Title :
Real time in a TLA-based theory of reactive systems
Author :
Kurki-Suonio, Reino ; Katara, Mika
Author_Institution :
Software Syst. Lab., Tampere Univ. of Technol., Finland
Abstract :
A practical theory for operational specification of reactive systems is described. Reasoning on temporal properties is made possible by it already at high levels of abstraction, and rigorous refinement towards implementation is supported. The paper discusses how the underlying logic, execution model, and refinement methods fit together, and how object-orientation, distribution, and real time are supported. A closer look is taken on the specification of real-time properties by illustrating the approach by a logically layered specification of simple mobile robot control software
Keywords :
formal specification; execution model; logic; logically layered specification; mobile robot control; operational specification; reactive systems; refinement methods; Design methodology; Electrical capacitance tomography; Encapsulation; Laboratories; Logic; Real time systems; Safety; Software engineering; Software systems; Specification languages;
Conference_Titel :
Object-Oriented Real-time Distributed Computing, 1998. (ISORC 98) Proceedings. 1998 First International Symposium on
Conference_Location :
Kyoto
Print_ISBN :
0-8186-8430-5
DOI :
10.1109/ISORC.1998.666788
