Issue No. 09 - Sept. (1986 vol. 12)
Brent Auernheimer , Department of Computer Science, University of California, Santa Barbara, CA 93106
Richard A. Kemmerer , Department of Computer Science, University of California, Santa Barbara, CA 93106
RT-ASLAN is a formal language for specifying real-time systems. It is an extension of the ASLAN specification language for sequential systems. Some of the features of the ASLAN language, such as constructs for writing procedural semantics in a nonprocedural logical language, are highlighted. The RT-ASLAN language supports specification of parallel real-time processes through arbitrary levels of abstraction; processes do not have to be specified to the same level of detail. Communicating processes use an interface process as an abstract data type representing shared information. From RT-ASLAN specifications, performance correctness conjectures are generated. These conjectures are logic statements whose proof guarantees the specification meets critical time bounds. A detailed example as well as a discussion of the advantages and disadvantages of formal specification and verification are included.
Real-time systems, Specification languages, Semantics, Abstracts, Software, Clocks, temporal logic, Data abstraction, formal specification, formal verification, real-time system specification, real-time validation
B. Auernheimer and R. A. Kemmerer, "RT-ASLAN: A specification language for real-time systems," in IEEE Transactions on Software Engineering, vol. 12, no. , pp. 879-889, 1986.