Title :
Formal Description of Time Management in Real-Time Operating Systems
Author :
Rusu-Banu, Fabricio ; Wang, Yingxu
Author_Institution :
Dept. of Electr. & Comput. Eng., Calgary Univ., Alta.
Abstract :
This paper describes the formal specification of the time management subsystem of a real-time operating system. Real-time process algebra (RTPA) is adopted to formally specify the system. The architecture, static behaviors, and dynamic behaviors of a CPU time manager are systematically specified that form an abstract model of the system. The formal specifications are implemented in C, on which the system performance can be tested and verified
Keywords :
formal specification; operating systems (computers); process algebra; abstract model; formal specification; real-time operating system; real-time process algebra; time management; Clocks; Computer architecture; Delay; Engineering management; Operating systems; Processor scheduling; Real time systems; Software engineering; Time factors; Timing; RTPA; Software engineering; architecture specifications; dynamic behavior; real-time operating systems; static behavior; time management;
Conference_Titel :
Electrical and Computer Engineering, 2006. CCECE '06. Canadian Conference on
Conference_Location :
Ottawa, Ont.
Print_ISBN :
1-4244-0038-4
Electronic_ISBN :
1-4244-0038-4
DOI :
10.1109/CCECE.2006.277604
