Real-Time Concurrent Processes

Discrete event concurrent process models are widely used to model control flow within and interactions between concurrent activities. Classical discrete event concurrent process models do not deal with resource allocation and scheduling or data variables, which limits their usefulness for real-time systems and makes it awkward to model some implementation details. Classical preemptive scheduling models do not deal with complex task sequencing and interaction, which limits their usefulness for describing distributed systems and implementation details. Discrete time models have been developed for real-time scheduling of concurrent processes 10, 5, 4. 11, and some work has been done on dense time real-time process algebras 3, 6. This report describes the use of dense time linear hybrid automata models to perform schedulability analysis and to verify implementation code.