The open archive for STFC research publications

You may experience service outages on ePubs over the coming days due to work being carried out to enhance our network infrastructure. The service should be considered at risk from 23/11 - 03/12.

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