Title :
Specification of realtime systems using ASTRAL
Author :
Coen-Porisini, Alberto ; Ghezzi, Carlo ; Kemmerer, Richard A.
Author_Institution :
Dipartimento di Elettronica, Politecnico di Milano, Italy
fDate :
9/1/1997 12:00:00 AM
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;
Journal_Title :
Software Engineering, IEEE Transactions on
