This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
RT-ASLAN: A specification language for real-time systems
Sept. 1986 (vol. 12 no. 9)
pp. 879-889
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.
Index Terms:
Real-time systems,Specification languages,Semantics,Abstracts,Software,Clocks,temporal logic,Data abstraction,formal specification,formal verification,real-time system specification,real-time validation
Citation:
Brent Auernheimer, Richard A. Kemmerer, "RT-ASLAN: A specification language for real-time systems," IEEE Transactions on Software Engineering, vol. 12, no. 9, pp. 879-889, Sept. 1986, doi:10.1109/TSE.1986.6313044
Usage of this product signifies your acceptance of the Terms of Use.