APPLYING UNIFYING THEORIES OF PROGRAMMING TO REAL-TIME PROGRAMMING

Issue title: Applications of formal methods

Article type: Research Article

Authors: Arenas, Alvaro E. | Bicarregui, Juan C.

Affiliations: E-Science Centre, CCLRC Rutherford Appleton Laboratory, Chilton, Oxfordshire, UK

Abstract: This paper introduces an approach to verify the correctness of the implementation of real-time languages. We apply the techniques presented in Hoare and He's "Unifying Theories of Programming" to reason about the correctness of compilers and schedulers for real-time languages, using high-level abstractions such as algebraic laws. In the compilation process, the existence of unique fixed-points is exploited to verify the implementation of crucial real-time operators such as asynchronous input, delay and timeout. It is developed an abstract model for scheduling real-time programs into a uniprocessor machine. The applicability of the model is shown by instancing it with two types of schedulers: a round-robin scheduler, employed when the participating parallel processes do not include deadline constraints, and a priority-based scheduler, used when each participating process is periodic and possesses an associated deadline.

Keywords: unifying theories of programming, real-time programming, compiler specification, scheduling

Journal: Journal of Integrated Design & Process Science, vol. 10, no. 4, pp. 69-88, 2006