Specification of realtime systems using ASTRAL

Author

Coen-Porisini, Alberto ; Ghezzi, Carlo ; Kemmerer, Richard A.

Author_Institution

Dipartimento di Elettronica, Politecnico di Milano, Italy

Volume

23

Issue

9

fYear

1997

fDate

9/1/1997 12:00:00 AM

Firstpage

572

Lastpage

598

Abstract

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A real-time system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the rationale of ASTRAL´s design. ASTRAL´s specification style is illustrated by discussing a telephony example. Composability of one or more ASTRAL system specifications is also discussed by the introduction of a composition section, which provides the needed information to combine two or more ASTRAL system specifications

Keywords

finite state machines; formal specification; program verification; real-time systems; specification languages; telecommunication computing; telephony; temporal logic; ASTRAL; complex systems; formal software development; formal specification language; global specification; modularized specifications; program verification; real-time systems specification; state machine specifications; structuring mechanisms; telephony; temporal logic; Aerospace electronics; Aircraft; Application software; Formal specifications; Logic; Programming; Specification languages; Telephony; Testing; Timing;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.629494

Filename

629494