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

fYear

1994

fDate

18-19 May 1994

Firstpage

44

Lastpage

48

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/RTOSS.1994.292563

Filename

292563