Title :
Practical formal development of real-time systems
Author :
Bradley, S.P. ; Henderson, W.D. ; Kendall, D. ; Robson, A.P.
Author_Institution :
Dept. of Comput., Northumbria Univ., Newcastle-upon-Tyne, UK
Abstract :
The complexities of real-time systems are such that it is often thought necessary to give a formal justification of their correctness especially if they are to be used in a safety-critical environment. We describe our work on a formally based design method for real-time systems which allows the timing aspects of a concurrent system to be mathematically described and verified, as well as semi-automatically implemented. Our design language, AORTA, is a timed process algebra, with features to ensure that all designs can be implemented. A predictable real-time kernel is also described, which is used in the construction of a system from an AORTA design, and which allows the timing of the implementation to be verified
Keywords :
multiprocessing systems; program verification; real-time systems; software engineering; systems analysis; AORTA; concurrent system; correctness; design language; formal development; formal justification; formally based design method; mathematical description; predictable real-time kernel; real-time systems; safety-critical environment; semi-automatically implemented; system construction; system verification; timed process algebra; timing; timing aspects; Algebra; Costs; Design methodology; Formal specifications; Formal verification; Kernel; Mars; Real time systems; Time factors; Timing;
Conference_Titel :
Real-Time Operating Systems and Software, 1994. RTOSS '94, Proceedings., 11th IEEE Workshop on
Conference_Location :
Seattle, WA
Print_ISBN :
0-8186-5710-3
DOI :
10.1109/RTOSS.1994.292563
