Title :
Platform-independent verification of real-time programs
Author :
Hooman, Jozef ; Van Roosmalen, Onno
Author_Institution :
Dept. of Comput. Sci., Eindhoven Univ. of Technol., Netherlands
Abstract :
To include the specification of timing properties in distributed programs, we propose a method to extend existing programming languages with timing annotations. These annotations provide a similar abstraction from the execution platform as is normal for non-real-time languages. Hence they enable the construction of (hard) real-time programs which can be proved correct independently of any underlying execution platform. The realization of programs on a particular platform is considered as a separate phase where, e.g., scheduling is important. We illustrate the method by means of a simple programming language which is extended with timing annotations. A formal, axiomatic, semantics of the language constructs is defined. It is used to prove the correctness of a small example program
Keywords :
formal specification; object-oriented languages; parallel languages; parallel programming; program verification; programming theory; real-time systems; scheduling; Deal; distributed programs; formal semantics; object oriented language; platform-independent program verification; programming languages; real-time languages; real-time program verification; scheduling; specification; timing annotations; timing properties; Computer languages; Control systems; Functional programming; Multitasking; Object oriented programming; Operating systems; Real time systems; Timing;
Conference_Titel :
Parallel and Distributed Real-Time Systems, 1997. Proceedings of the Joint Workshop on
Conference_Location :
Geneva
Print_ISBN :
0-8186-8096-2
DOI :
10.1109/WPDRTS.1997.637978