Formal Methods for Timing and Schedlability Analysis of Embedded Systems

Presented by Insup Lee, Anna Philippou, and Oleg Sokolsky

April 13, 2002, morning

Abstract :

This tutorial describes a process-algebraic approach to a variety of problems commonly encountered in the design of embedded systems. A family of real-time process algebras, ACSR, PACSR and ACSR-VP, is considered. ACSR is a resource-bound real-time process algebra that supports synchronous timed actions and asynchronous instantaneous events as well as the notions of resource, priority, exception, and interrupt. PACSR is a probabilistic extension of ACSR with resources that can fail and associated failure probabilities. ACSR-VP extends ACSR with value passing between processes and parameterized process definitions. This tutorial also provides simple real-time system examples to illustrate the expressive power and analysis technique of each process algebra.