A RESOURCE-BASED PRIORITIZED BISIMULATION FOR REAL-TIME SYSTEMS

The behavior of concurrent, real-time systems can be specified using a process algebra called CCSR. The underlying computation model of CCSR is a resource-based one in which multiple resources execute synchrono usly, while processes assigned to the same resource are interleaved ac cording to their priorities. CCSR allows the algebraic specification o f timeouts, interrupts, periodic behaviors, and exceptions. This paper develops a natural treatment of preemption, which is based not only o n priority, but also on resource utilization and inter-resource synchr onization. The preemption ordering leads to a term equivalence based o n strong bisimulation, which is also a congruence with respect to the operators. Consequently the equivalence yields a compositional proof s ystem, which is illustrated in the verification of a resource-sharing, producer-consumer problem. (C) 1994 Press, Inc.