عنوان

Specification and analysis of concurrent systems :

3642773370

9783642773372

b573651

Specification and analysis of concurrent systems :

[Book]

the cosy approach.

Ryszard Janicki

[Place of publication not identified]

Springer

2012

1 What COSY Is and What It Is For.- 1.1 Introduction.- 1.2 Concepts, Objectives and Design Decisions.- 1.3 Structure of Bookevevr.- 1.4 Acknowledgements.- 2 Formal Theory of Basic COSY.- 2.1 Basic COSY Syntax and Semantics.- 2.2 VFS Semantics of COSY.- 2.2.1 Simple Properties of Vector Sequences.- 2.2.2 Vector Sequences and Partial Orders.- 2.2.3 Vector Sequences of Path Programs.- 2.2.4 Concurrent Product of Regular Expressions.- 2.3. Petri Net Semantics of COSY.- 2.3.1 Elements of Net Theory.- 2.3.2 VFS semantics of SMD nets.- 2.3.3 Semantics of Labelled Petri Nets.- 2.3.4 Labelled Petri Nets defined by Path Programs.- 2.3.5 Uniquely Named and Labelled Uniquely Named Regular Expressions.- 2.3.6 Labelled Nets and Products of Regular Expressions.- 2.3.7 Labelled Nets and COSY Path Programs.- 2.3.8 Other Constructions.- 2.4 Adequacy Properties of Path Programs.- 2.4.1 Syntactically Conflict-Free Path Programs.- 2.4.2 Checking Adequacy of SCF-Path Programs.- 2.4.3 Adequacy-Preserving Transformations.- Insertions Preserving Adequacy.- Deletions Preserving Adequacy.- Applications of Adequacy-Preserving Transformations.- 2.4.4 Free-Choice Path Programs.- 2.5 Execution Semantics for COSY.- 2.5.1 Execution Strategies.- 2.5.2 Maximally Concurrent Strategies.- 2.6 Semantics of COSY with Priorities.- 2.6.1 Observations and Multiple Sequences.- 2.6.2 MFS Semantics for Priority COSY.- 2.6.3 Starvation Problem.- 2.6.4 Infinite MFS and Formal Definition of Starvation.- 2.6.5 Simulation of Dynamic Priorities.- 2.6.6 VFS Semantics for Priority COSY.- 2.7 Bibliographic Notes.- 3 High-level COSY Programs and System Design.- 3.1 High-level COSY Syntax and Semantics.- 3.2 The Process Notation.- 3.3 Macro Generators for COSY Notation.- 3.3.1 The Macro Program.- 3.3.2 The Collectivisors.- 3.3.3 The Body-Replicators.- 3.3.4 Macro Paths and Macro Processes.- 3.3.5 Sequence Replicators.- 3.3.6 Left and Right Sequence Replicators.- 3.3.7 The Distributors.- 3.3.8 Expansion of Macro COSY Programs.- The Expansion of Replicators.- The Expansion of Distributors.- Expansion Theorem.- 3.4 The Semantics of Macro COSY Programs.- 3.5 The COSY Environment.- 3.5.1 The Architecture of BCS.- The BCS Analysis Mechanism.- The BCS Semantic Transformation Mechanism.- The BCS Interface.- 3.5.2 The Macro COSY Environment.- 3.6 The COSY System Dossier.- 3.7 Bibliographical Notes.- 4 COSY Applications.- 4.1 Two-Way Channel with Disconnect.- 4.1.1 Bibliographic Notes.- 4.2 The Hyperfast Banker.- 4.2.1 The Bank Director.- 4.2.2 The Vault.- 4.2.3 The Doors.- 4.2.4 The Fair Doormen.- 4.2.5 The Counters.- 4.2.6 The Clerks.- 4.2.7 The Fair Reimbursers.- 4.2.8 The Customers.- 4.2.9 Priority Constraints.- 4.2.10 Final Comment and Bibliographical Notes.- 4.3 Cigarette Smokers.- Bibliographic Notes.- 4.4 Merlin-Randell Problem of Train Journeys.- 4.4.1 Movement Graphs and Minimal Critical Patterns.- 4.4.2 COSY Specification of the Synchronization.- 4.4.3 Final Comment and Bibliographic Notes.- 4.5 Transforming Sequential Systems into Concurrent Systems.- 4.5.1 e-Paths and e-Path Programs.- 4.5.2 Concurrent e-Paths and Proper Concurrent e-Paths.- 4.5.3 Synchronized e-Path Programs.- 4.5.4 Final Comment and Bibliographic Notes.- 4.6 Modelling N-Modular Redundancy.- 4.6.1 Replicated Computation in Networks of Computing Nodes.- 4.6.2 Formal Specification.- 4.6.3 Bibliographical Notes.- 5 Comparison of COSY with Other Models.- 5.1 COSY and CCS.- 5.2 COSY and CSP.- Full COSY and Petri Nets.- 5.3.1 Uniquely Named Comma&Star-free Programs and Asymmetric Choice Nets.- 5.3.2 Priority Path Programs, Priority Nets and Inhibitor Net.- 5.4 Vector Sequences and Mazurkiewicz Traces.- 5.5 COSY and Synchronized Behaviours.- 6 Historical Perspective.- 6.1 Introduction.- 6.2 Conceptual and Methodological Framework of COSY Approach.- Appendices.- A Algebra of Relations.- B Automata and Formal Language Theory.- B.1 Strings.- B.2 Languages.- B.3 Regular Expressions and Languages.- B.4 Finite State Automata and Grammars.- C Elements of Graph Theory.- D Proofs of Theorems 2.25, 2.26 and 2.28.- E Proofs of Theorems 2.37 and 2.38.- F Proof of Theorem 2.29.- G Proof of Theorem 4.3.- H Basic COSY Notations and Macro COSY Notation.- List of Figures.- List of Algorithms.- List of Definitions.- List of Theorems.- List of Corollaries.- List of Lemmas.

Ryszard Janicki

Ryszard Janicki

[Book]

Y