Abstract
Specification of Realtime Systems Using ASTRAL
by: Alberto Coen-Porisini, Carlo Ghezzi, and Richard A. Kemmerer
Abstract:
ASTRAL is a formal specification language for realtime systems. It is intendedto support formal software development and, therefore, has been formallydefined. The structuring mechanisms in ASTRAL allow one to build modularizedspecifications of complex systems with layering. A realtime system is modeledby a collection of state machine specifications and a single globalspecification. 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 bythe introduction of a composition section, which provides the neededinformation to combine two or more ASTRAL system specifications into a singlenew one. Finally, this paper discusses the current status of the ASTRALsoftware development environment.
Keywords:
Formal methods, Formal specification and verification, Assertions,Temporal logic, Realtime systems, Timing requirements, SoftwareTools, State machines, Composability, ASLAN, TRIO.
Date:
July 1996
Document: 1996-30
