Skip to main content

Über dieses Buch

Concurrent systems abound in human experience but their fully adequate conceptualization as yet eludes our most able thinkers. The COSY (ConcurrentSystem) notation and theory was developed in the last decade as one of a number of mathematical approaches for conceptualizing and analyzing concurrent and reactive systems. The COSY approach extends theconventional notions of grammar and automaton from formal language and automata theory to collections of "synchronized" grammars and automata, permitting system specification and analysis of "true" concurrency without reduction to non-determinism. COSY theory is developed to a great level of detail and constitutes the first uniform and self-contained presentationof all results about COSY published in the past, as well as including many new results. COSY theory is used to analyze a sufficient number of typical problems involving concurrency, synchronization and scheduling, to allow the reader to apply the techniques presented tosimilar problems. The COSY model is also related to many alternative models of concurrency, particularly Petri Nets, Communicating Sequential Processes and the Calculus of Communicating Systems.



Chapter 1. What COSY Is and What It Is For

Concurrent systems abound in human experience but their fully adequate conceptualization as yet eludes our most able thinkers. Even the concurrent systems we construct on the basis of modern computer and communication technology continue to elude adequate conceptual analysis in general. However, our increasing dependence on ever more complex concurrent systems in the management and control of human affairs and activities increases the urgency for developing more adequate concepts to maintain reliable control over systems we have created.
Ryszard Janicki, Peter E. Lauer

Chapter 2. Formal Theory of Basic COSY

A basic COSY path program is a collection of paths in program and endprogram parentheses. A path is an expression, similar to a regular expression (see Appendix B.3), built from event names, semicolons, commas, conventional parentheses and Kleene stars, enclosed by path and end parentheses. For instance:
$${{\Pr }_{1}} = \left\{ \begin{gathered} {\text{ }}\underline {program} \hfill \\ P(1):\underline {path} {\text{ }}a;b;c{\text{ }}\underline {end} \hfill \\ P(2):\underline {path} {\text{ }}(d;e)*;b{\text{ }}\underline {end} \hfill \\ {\text{ }}\underline {endprogram} \hfill \\ \end{gathered} \right.{\text{ }}$$
In every expression as described above, the semicolon specifies sequential occurrences of the events named or subexpressions, and comma specifies a mutually exclusive occurrence of one of the events named or subexpressions. The comma binds more strongly than the semicolon, so that the expression “a;b, c” means “first event a must occur, after which exclusively either event b or event c must occur”. An expression may be enclosed in conventional parentheses with Kleene star appended, as for instance “(d, e)*” which means that the enclosed specification applies zero or more times. In other words, an expression between path and end may be understood as an ordinary regular expression. The only difference is that “∪” is replaced by “,”, concatenation is replaced by “;”, and mutually exclusive choice binds more strongly than concatenation1. Thus for instance “a; b, c” is equivalent to “a(bc)” in the traditional notation for regular expressions. Moreover, by definition, the parentheses path and end correspond to “(” and “)*” respectively, so that a single path specifies repeated (or cyclic) sequences of event occurrences.
Ryszard Janicki, Peter E. Lauer

Chapter 3. High-level COSY Programs and System Design

Throughout Chap. 2 we have encountered two types of basic COSY programs. First, uninterpreted programs, which involve a (usually small) number of uninterpreted events to permit the illustration of notation, to support the definition of concepts arising in the context of concurrency theory, and to support the formulation and proof of important laws relating these concepts. Second, interpreted programs, which involve a (usually much larger) number of interpreted events which permit the application of the results of concurrency theory to develop verified solutions to problems arising in the area of concurrent system design and specification.
Ryszard Janicki, Peter E. Lauer

Chapter 4. COSY Applications

This chapter is devoted to various applications of the COSY theory and techniques. In general we can find two classes of applications. The first kind is the application of COSY, its theory and techniques to specify and/or prove properties of some realistic non-sequential systems or their parts. In fact, we already used COSY in Chap. 2 and 3 to analyse specifications of a linereader-lineprinter system, a specification mechanism for controlling access to a critical section, a mechanism regulating the use of a critical section by processes with differing priorities, and a reader-writer system.
Ryszard Janicki, Peter E. Lauer

Chapter 5. Comparison of COSY with Other Models

In this chapter we compare COSY with other models of non-sequential systems. Besides Petri Nets, the Calculus of Communicating Systems (CCS) and Communicating Sequential Processes (CSP) have been developed to a great extent and sophistication. We devote the first two sections of this chapter to the analysis of the relationship between COSY and, respectively, CCS and CSP. In the third section we show how the process notation and the concept of priority can be modelled by appropriate classes of Petri nets. The fourth section shows the equivalence between vector sequences and Mazurkiewicz traces. The last section is an analysis of the relationship between COSY and Synchronized Behaviours.
Ryszard Janicki, Peter E. Lauer

Chapter 6. Historical Perspective

This historical perspective of the development of the COSY approach was written particularly to compensate for omissions we have had to make to obtain a text of reasonable size. There are several kinds of omissions we have had to make:
Omission of results in COSY theory which exist in the published literature, but which are based on different techniques which would have to be explained to make the book self contained. Their inclusion would have lengthened the present text considerably.
Omission of discussion of other important formal approaches to concurrency.
Omission of discussion of other important path notations based on different models of concurrency.
Omission of discussion of path or COSY like models which have largely appeared independently of knowledge of the similarity with our approach.
Ryszard Janicki, Peter E. Lauer


Weitere Informationen