A Synthesis Rule for Concurrent Systems
- 1 January 1978
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 305-311
- https://doi.org/10.1109/dac.1978.1585190
Abstract
Concurrent (hardware and software) systems can become extremely complex due to the existence of multiple loci of control. Posteriori analysis of such systems is very difficult. This paper presents a systematic bottom-up modular approach to synthesis. The synthesis procedure at each stage yields all invariants (of a certain kind) of the system. These invariants can be used as an aid to proving certain properties of the system such as boundedness, conservativeness, mutual exclusion, absence of deadlock, etc. The use of the synthesis rule and the utility of the invariants are illustrated by examples.Keywords
This publication has 13 references indexed in Scilit:
- Petri NetsACM Computing Surveys, 1977
- Formal verification of parallel programsCommunications of the ACM, 1976
- A Methodology for the Design and Implementation of Communication ProtocolsIEEE Transactions on Communications, 1976
- MonitorsCommunications of the ACM, 1974
- Limitations of Dijkstra's Semaphore Primitives and Petri netsACM SIGOPS Operating Systems Review, 1973
- Comments on capabilities, limitations and “correctness” of Petri netsPublished by Association for Computing Machinery (ACM) ,1973
- Marked directed graphsJournal of Computer and System Sciences, 1971
- A Petri Net model of the CDC 6400Published by Association for Computing Machinery (ACM) ,1971
- A new approach to optimization of sequencing decisionsAnnual Review in Automatic Programming, 1970
- The correctness of nondeterministic programsArtificial Intelligence, 1970