The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/35385
Record Status Checked
Record Id 35385
Title Applying Unifying Theories of Programming to Real-Time Programming
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.
Organisation CCLRC , ESC , ESC-IM
Keywords Engineering , Formal Methods , Unifying Theories of Programming , Real-Time Systems
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Journal Article Journal of Integrated Design and Process Science 10, no. 4 (2006): 69-88. realtime.pdf 2006
Paper In Conference Proceedings In Integrated Design and Process Technology Conference (IDPT-2006), San Diego, California, USA, 25th - 30th June 2006, (2006). 2006