Concurrent and Real-time Systems

The CSP Approach

AvSteve Schneider

Häftad, Engelska, 1999

Del i serien Worldwide Series in Computer Science

874 kr

Beställningsvara. Skickas inom 5-8 vardagar. Fri frakt över 249 kr.

Beskrivning

The CSP approach has been widely used in the specification, analysis and verification of concurrent and real-time systems, and for understanding the particular issues that can arise when concurrency is present. It provides a language which enables specifications and designs to be clearly expressed and understood, together with a supporting theory which allows them to be analyzed and shown to be correct. This book supports advanced level courses on concurrency covering timed and untimed CSP. The first half introduces the language of CSP, the primary semantic models (traces, failures, divergences and infinite traces), and their use in the modelling, analysis and verification of concurrent systems. The second half of the book introduces time into the language, brings in the timed semantic model (timed failures) and finally presents the theory of timewise refinement which links the two halves together. Accompanying website: http://www.cs.rhbnc.ac.uk/books/concurrency Containing the following: -Exercises and solutions -Instructors resources - Example CSP programs to run on FDR and ProBe -Links to useful sites Partial Contents: Part I: The Language of CSP; Sequential Processes; Concurrency; Abstraction and Control Flow; Part II: Analyzing Processes; Traces; Specification and Verification with Traces; Stable Failures; Specification and Verification with Failures; Failures, Divergences, and Infinite Traces; Part III: Introducing Time; The Timed Language; Timed transition systems; Part IV: Timed Analysis; Semantics of Timed CSP; Timed Specification and Verification; Timewise Refinement; Appendix A: Event-based Time; A.1 Standard CSP and $tock$; A.2 Translating from Timed CSP; A.3 Notes; Appendix B: Model-checking with FDR; B.1 Interacting with FDR; B.2 How FDR Checks Refinement; B.3 Machine readable CSP; Index of Processes.

Produktinformation

Utgivningsdatum:1999-09-15
Mått:187 x 235 x 29 mm
Vikt:907 g
Format:Häftad
Språk:Engelska
Serie:Worldwide Series in Computer Science
Antal sidor:528
Förlag:John Wiley & Sons Inc
ISBN:9780471623731

Utforska kategorier

Systemvetenskap och AI inom Data och IT
Programmeringsböcker inom Data och IT

Mer om författaren

Steve Schneider is the author of Concurrent and Real-time Systems: The CSP Approach, published by Wiley.

Innehållsförteckning

Preface ixAcknowledgements xvPart 1 The language of CSP1 Sequential processes 31.1 Events and processes 31.2 Performing events 81.3 Recursion 131.4 Choice 202 Concurrency 312.1 Alphabetized parallel 312.2 Interleaving 442.3 Interface parallel 503 Abstraction and control flow 553.1 Hiding 553.2 Event renaming 623.3 Sequential composition 693.4 Interrupt 723.5 Notes 74Part II Analysing processes4 Traces 874.1 Sequences 874.2 Trace semantics 914.3 Recursion 1174.4 Testing 1334.5 Congruence 1365 Specification and verification with traces 1415.1 Property-oriented Specification 1415.2 Verification 1435.3 Recursion induction 1555.4 Case study: Distributed sum 1605.5 Process-oriented specification 1686 Stable failures 1736.1 Observing processes 1746.2 Process semantics 1786.3 Recursion 1887 Specification and verification with failures 1957.1 Property-oriented specification 1957.2 Verification 1977.3 Recursion induction 2067.4 Process-oriented specification 2097.5 Case study: Distributed sum 2128 Failures, divergences, and infinite traces 2218.1 Observing processes 2218.2 Process semantics 2298.3 Recursion 2428.4 Specification and verification 2488.5 Recursion induction 2538.6 Case study: Distributed sum 2568.7 Must testing and FDI equivalence 2578.8 Notes 258Part III Introducing time9 The timed language 2679.1 Timed computational model 2689.2 Transitions 2699.3 Performing events 2709.4 Choice 2759.5 Recursion 2869.6 Concurrency 2909.7 Abstraction 2979.8 Flow of control 30410 Timed transition systems 31310.1 Evolution 31310.2 Executions 31510.3 Well-timed processes 32710.4 Notes 329Part IV Timed analysis11 Semantics of timed CSP 33511.1 Timed observations 33611.2 Timed failures semantics 34711.3 Recursion 35811.4 Testing and timed failures equivalence 36312 Timed specification and verification 36912.1 Specification 36912.2 Verification 37512.3 Recursion induction 38512.4 Ill-timed processes 38812.5 Case study: Fischer’s protocol 39013 Timewise refinement 39913.1 Trace timewise refinement 40013.2 Failures timewise refinement 41013.3 Refinement and parallel composition 41313.4 Case study: a railway crossing 43113.5 FDI timewise refinement 43613.6 Testing and timewise refinement 43913.7 Notes 442Appendix A: Event-based time 447A.1 Standard CSP and took 448A.2 Translating from timed CSP 454A.3 Notes 465Appendix B: Model-checking with FDR 469B.1 Interacting with FDR 470B.2 How FDR checks refinement 473B.3 Machine readable CSP 478References 485Notation 493Index 498Index of Processes 507

Mer från samma författare

11th Hour Audio Productions Audio Anthology, Vol. 1

John Ballentine, Jeremy Hennessy, Neil Gustin, Richard H. Brooks, Scott Phillips, Jonathan Patrick Russell, Shane Harris, MJ Cogburn, Matthew McLean, Justin Mullane, Steve Schneider, James Comtois