A proof system for communicating shared resources
- 1 January 1990
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 288-299
- https://doi.org/10.1109/real.1990.128760
Abstract
The authors introduce a proof system for CCSR, a process algebra based on the CSR model. CCSR allows the algebraic specifications of timeouts, interrupts, periodic behaviors and exceptions. A rigorous treatment of preemption, which is based not only on priority but also on resource utilization and inter-resource synchronization, is provided. The theory of preemption leads to a term equivalence based on strong bisimulation, which yields a set of laws forming the proof system. As an illustration, a resource-sharing, producer-consumer problem is presented and the authors use their laws to prove its correctness.Keywords
This publication has 10 references indexed in Scilit:
- Concurrency and automata on infinite sequencesPublished by Springer Nature ,2005
- CCSR: A calculus for communicating shared resourcesPublished by Springer Nature ,2005
- Communicating shared resources: a model for distributed real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Priorities in process algebrasInformation and Computation, 1990
- Compositional semantics for real-time distributed computingInformation and Computation, 1988
- A linear-history semantics for languages for distributed programmingTheoretical Computer Science, 1984
- Calculi for synchrony and asynchronyTheoretical Computer Science, 1983
- On the algorithmic properties of concurrent programsPublished by Springer Nature ,1981
- A Calculus of Communicating SystemsLecture Notes in Computer Science, 1980
- Communicating sequential processesCommunications of the ACM, 1978