Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

1992 | Book

What COSY Is and What It Is For Read chapter Read first chapter

Specification and Analysis of Concurrent Systems

The COSY Approach

Authors: Prof. Dr. Ryszard Janicki, Prof. Dr. Peter E. Lauer

Publisher: Springer Berlin Heidelberg

Book Series : Monographs in Theoretical Computer Science. An EATCS Series

Included in: Professional Book Archive

Login to get access
insite
SEARCH

About this book

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.

Table of Contents

Frontmatter
Chapter 1. What COSY Is and What It Is For
Abstract
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
Abstract
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(b ∪ c)” 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
Abstract
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
Abstract
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
Abstract
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
Abstract
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:
1.
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.
 
2.
Omission of discussion of other important formal approaches to concurrency.
 
3.
Omission of discussion of other important path notations based on different models of concurrency.
 
4.
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
Backmatter
Metadata
Title
Specification and Analysis of Concurrent Systems
Authors
Prof. Dr. Ryszard Janicki
Prof. Dr. Peter E. Lauer
Copyright Year
1992
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-77337-2
Print ISBN
978-3-642-77339-6
DOI
https://doi.org/10.1007/978-3-642-77337-2