Specification and analysis of concurrent systems. The COSY approach
compositional specificationconcurrent systemsCOSY languagePetri netssemanticsvector firing sequences
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
This book gives a comprehensive account of a compositional specification method for concurrent and reactive systems, COSY, based on extensions of notions of formal language and automata theory, in which true concurrency (as opposed to interleaving concurrency) and causal dependencies of subsystems can be represented. After the introduction of the COSY language (Chapter 1), in Chapter 2 two different semantics of the language is given, one by means of vector firing sequences and one based on Petri nets. The latter is suited for ambiguous specifications, whereas the former is not. The chapter further discusses adequacy preserving transformations of specifications and various execution semantics for COSY such as interleaving, full, maximally concurrent and optimal semantics. Also COSY with priorities is treated extensively. Chapter 3 presents higher-level features of COSY such as process notation and several kinds of macro generators. In Chapter 4 several non-trivial applications involving concurrency, synchronization and scheduling are elaborated in COSY. It is also indicated how COSY's theory may be used in other theoretical issues like efficiency and reliability. Chapter 5 contains comparisons of COSY with other well-known models such as CCS, CSP and Mazurkiewicz traces. A historical perspective is offered in Chapter 6, in which the choice of material is justified, in particular the omissions that the authors had to make. The book is concluded with an extensive bibliography, 8 appendices with introductory treatments of the algebra of relations, automata and formal language theory and graph theory, proofs of the more difficult theorems and basic COSY notations, several lists of figures, algorithms, etc, and, finally, an index. The book contains a lot of (formal) detail, which enables the reader to get a good impression of the way COSY works and to value its assets.
- scientific article; zbMATH DE number 4018373
- scientific article; zbMATH DE number 4043257
- Concurrency theory. Calculi and automata for modelling untimed and timed cocurrent systems.
- scientific article; zbMATH DE number 3956419
- The analysis of concurrent systems. Cambridge, September 12-16, 1983. Proceedings
- A formal semantics for concurrent systems with a priority relation
- The box algebra = Petri nets + process expressions
- scientific article; zbMATH DE number 4018373 (Why is no real title available?)
- Specifying and Analysing SOC Applications with COWS
- scientific article; zbMATH DE number 3956419 (Why is no real title available?)
- scientific article; zbMATH DE number 4043257 (Why is no real title available?)
- Solving recursive net equations
- The 4C Spectrum of Fundamental Behavioral Relations for Concurrent Systems
- Cyclic vector languages
- Transition systems of Elementary Net Systems with inhibitor arcs
- Modelling concurrency with comtraces and generalized comtraces
- Interval traces with mutex relation
- A formal system for specification analysis of concurrent programs
- Relational structures model of concurrency
This page was built for publication: Specification and analysis of concurrent systems. The COSY approach
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4023058)