×

zbMATH — the first resource for mathematics

Automated analysis of mutual exclusion algorithms using CCS. (English) Zbl 0696.68039
Summary: A number of mutual exclusion algorithms are studied by representing them as agents in the Calculus of Communicating Systems and using an automated tool embodying some of the theory of the Calculus to analyse the representations. It is determined whether or not each of the algorithms preserves mutual exclusion and is live.

MSC:
68N25 Theory of operating systems
68W99 Algorithms in computer science
Software:
CESAR
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baeten, J.:Procesalgebra, Kluwer programmatuurkunde, 1986.
[2] Baeten, J., Bergstra, J. and Klop, J. W.: Decidability of Bisimulation Equivalence for Processes Generating Context-free Languages, in Springer LNCS 299, 1987. · Zbl 0635.68014
[3] Clarke, E. and Emerson, E. A.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, in Springer LNCS 131, 1981. · Zbl 0546.68014
[4] Clarke, E. and Grümberg, O.: Research on Automatic Verification of Finite-State Concurrent Systems.Ann. Rev. Comput. Sci., 2 1987.
[5] Cleaveland, R., Parrow, J. and Steffen, B.: The Concurrency Workbench, to appear in [Gre89].
[6] Cleaveland, R., Parrow, J. and Steffen, B.: A Semantics based Verification Tool for Finite State Systems, to appear inProc. Ninth Int. Symp. on Protocol Specification, Testing and Verification, North Holland, 1989.
[7] Dijkstra, E. W.: Solution of a Problem in Concurrent Programming Control. Comm. ACM, 8/9 1965.
[8] Emerson, E. A. and Lei, C-L.: Modalities for Model Checking: Branching Time Strikes Back. Sci. Comput. Prog., 6 1987. · Zbl 0615.68019
[9] Emerson, E. A. and Srinivasan, J.: Branching time temporal logic, in Springer LNCS 354, 1989. · Zbl 0683.68013
[10] Francez, N.:Fairness, Springer, 1986.
[11] Proceedings of Workshop on Automatic Verification Methods for Finite State Systems, Grenoble 1989, to appear in Springer LNCS series.
[12] Hoare, C. A. R.:Communicating Sequential Processes, Prentice-Hall 1985. · Zbl 0637.68007
[13] Hyman, H.: Comments on a Problem in Concurrent Programming Control.Comm. ACM, 9/1 1966.
[14] Jonsson, B. and Parrow, J.: Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs, in Springer LNCS 349, 1989. · Zbl 0799.68133
[15] Knuth, D. E.: Additional Comments on a Problem in Concurrent Programming Control. Comm. ACM, 9/5 1966.
[16] Kozen, D.: Results on the Prepositional\(\mu\)-Calculus. Theoretical Computer Science, 27 1983. · Zbl 0553.03007
[17] Lamport, L.: The Mutual Exclusion Problem Part II – Statement and Solutions. JACM, 33/2 1986. · Zbl 0627.68018
[18] Larsen, K.: Proof Systems for Hennessy-Milner Logic with Recursion to appear inInformation and Computation 1989.
[19] Manna, Z. and Pneuli A.: The Anchored Version of the Temporal Framework, in Springer LNCS 354, 1989. · Zbl 0683.68031
[20] Milner, R.:A Calculus of Communicating Systems, Springer-Verlag, 1980; available as University of Edinburgh report ECS-LFCS-87-7. · Zbl 0452.68027
[21] Milner, R.: Calculi for Synchrony and Asynchrony.Theoretical Computer Science, 25 1983. · Zbl 0512.68026
[22] Milner, R.:Communication and Concurrency, Prentice-Hall, 1989. · Zbl 0683.68008
[23] Parrow, J.: Verifying a CSMA/CD-Protocol with CCS, University of Edinburgh report ECS-LFCS-87-18, 1987.
[24] Peterson, J. L. and Silberschatz, A.:Operating System Concepts, 2nd ed., Addison Wesley, 1985. · Zbl 0758.68023
[25] Pratt, V., A Decidable Mu-Calculus, in Proc. 22nd ACM FOCS, 1981.
[26] Queille J., and Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR, in Springer LNCS 137, 1981. · Zbl 0482.68028
[27] Stirling, C.: Temporal Logics for CCS, in Springer LNCS 354, 1989. · Zbl 0683.68016
[28] Stirling, C.: Modal and Temporal Logics, chapter to appear inHandbook of Logic in Computer Science, OUP, 1989.
[29] Stirling, C. and Walker, D.: Local Model Checking in the Modal Mu-Calculus, in Springer LNCS 351, 1989. · Zbl 0745.03027
[30] Stirling, C. and Walker, D.: CCS, Liveness, and Local Model Checking in the Linear Time Mu-Calculus, to appear in [Gre89]. · Zbl 0745.03027
[31] Walker, D.: Introduction to a Calculus of Communicating Systems, University of Edinburgh report, ECS-LFCS-87-22, 1987.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.