Abstract
The aim of this paper is to illustrate by an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications.
CESAR allows the progressive validation of the algorithmic description of a system of communicating sequential processes with respect to a given set of specifications. The algorithmic description is done in a high level language inspired from CSP and specifications are a set of formulas of a branching time logic, the temporal operators of which can be computed iteratively as fixed points of monotonic predicate transformers. The verification of a system consists in obtaining by automatic translation of its description program an Interpreted Petri Net representing it and evaluating each formula of the specifications.
Originally published in: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 337-351. Springer, Heidelberg (1982).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. CACM 12(5), 260–261 (1969)
Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. In: Proc. 8th Annual ACM Symp. on Principles of Programming Languages, January 1981, pp. 164–176 (1981)
Bremer, J., Drobnik, O.: A new approach to protocol design and validation IBM research report RC 8018. IBM Yorktown Heights (December 1979)
Brinch Hansen, P.: Distributed Processes: A concurrent programming concept. CACM 21(5), 934–941 (1978)
Clarke Jr., E.M.: Synthesis of resource invariants for concurrent programs. ACM Trans. on Progr. Languages and Systems 2(3), 338–358 (1980)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. 5th ACM. Symp. on Principles of Programming Languages, Tucson, Ariz, pp. 84–96 (1978)
Gabbay, D., Pnuelli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Conference Record of the 7th Annual ACM Symposium on Principles of Programming Languages, January 1980, pp. 163–173 (1980)
Hoare, C.A.R.: Communicating Sequential Processes. Comm., ACM 21(8), 666–667 (1978)
Jensen, K., Kyng, M., Madsen, O.L.: A Petri net definition of a system description language. In: Semantics of Concurrent Computation. LNCS. pp. 348–368. Springer (July 1979)
Keller, R.M.: Formal verification of parallel programs. Comm. ACM 19(7), 371–384 (1976)
Lamport, L.: ""Sometime" is sometimes "not never" - On the temporal logic of programs. In: Las Vegas, January 1980, pp. 174–185 (1980)
Lauer, P.E., Campbell, R.H.: Formal semantics of a class of high level primitives for coordinating concurrent processes. Acta Informatica 5, 297–332 (1975)
Manna, Z., Pnueli, A.: Verification of concurrent programs: The temporal framework. Intern. Summer School, Theoretical Foundations of Programming Methodology, Munich (July 1981)
Queille, J.P.: The Cesar system: An aided design and certification system for distributed applications. In: Proc. 2nd Int. Conf. on Distributed Computing Systems, April 1981, pp. 149–161 (1981)
Rescher, N., Urquhart, A.: Temporal Logic. Springer, Vienna (1971)
Schwartz, R.L., Melliar-Smith, P.M.: Temporal logic specification of distributed systems. In: Proc. 2nd Int. Conf. on Distributed Computing Systems, April 1981, pp. 46–454 (1981)
Sifakis, J.: A unified approach for studying the properties of transition systems. Research Report RR 179, IMAG December 1979 (Revised December 1980) to appear in TCS January 1982
Special Interest Group: Petri nets and related system models. Newsletter, 17–20 (February 1981)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Queille, J.P., Sifakis, J. (2008). SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR. In: Grumberg, O., Veith, H. (eds) 25 Years of Model Checking. Lecture Notes in Computer Science, vol 5000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69850-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-69850-0_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69849-4
Online ISBN: 978-3-540-69850-0
eBook Packages: Computer ScienceComputer Science (R0)