Specification and verification of concurrent systems in CESAR
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.
KeywordsTemporal Logic Propositional Variable Execution Sequence High Level Language Algorithmic Description
Unable to display preview. Download preview PDF.
- [Bartlett 69]K.A. BARTLETT, R.A. SCANTLEBURY and P.T. WILKINSON "A note on reliable full-duplex transmission over half-duplex links" CACM, Vol. 12, No5, May 1969, pp. 260–261.Google Scholar
- [Ben-Ari 81]M. BEN-ARI, Z. MANNA and A. PNUELI "The temporal logic of branching time" Proc. 8th Annual ACM Symp. on Principles of Programming Languages, Jan. 1981, pp. 164–176.Google Scholar
- [Bremer 79]J. BREMER and O. DROBNIK "A new approach to protocol design and validation" IBM research report RC 8018, IBM Yorktown Heights, Dec. 1979Google Scholar
- [Brinch Hansen 78]P. BRINCH HANSEN "Distributed Processes: A concurrent programming concept" CAM, Vol. 21, No5, Nov. 1978, pp. 934–941.Google Scholar
- [Clarke 80]E.M. CLARKE Jr. "Synthesis of resource invariants for concurrent programs" ACM Trans. on Progr. Languages and Systems, Vol. 2, No3, July 1980, pp. 338–358.Google Scholar
- [Cousot 78]P. COUSOT and N. HALBWACHS "Automatic discovery of linear restraints among variables of a program" Proc. 5th ACM. Symp. on Principles of Programming Languages, Tucson, Ariz., 1978, pp. 84–96.Google Scholar
- [Gabbay 80]D. GABBAY, A. PNUELLI, S. SHELAH and J. STAVI "On the temporal analysis of fairness" Conference Record of the 7th Annual ACM Symposium on Principles of Programming Languages, Jan. 1980, pp. 163–173.Google Scholar
- [Hoare 78]C.A.R. HOARE "Communicating Sequential Processes" Comm. ACM 21–8, August 1978, pp. 666–667.Google Scholar
- [Jensen 79]K. JENSEN, M. KYNG and O.L. MADSEN "A Petri net definition of a system description language" Semantics of Concurrent Computation in LNCS, Springer Verlag, July 1979, pp. 348–368.Google Scholar
- [Keller 76]R.M. KELLER "Formal verification of parallel programs" Comm. ACM 19, 7 (July 1976), pp. 371–384.Google Scholar
- [Lamport 80]L. LAMPORT ""Sometime" is sometimes "not never" — On the temporal logic of programs" Proc. of the 7th Annual ACM Symp. on Principles of Programming Languages, Las Vegas, Janv. 1980, pp. 174–185.Google Scholar
- [Lauer 75]P.E. LAUER and R.H. CAMPBELL "Formal semantics of a class of high level primitives for coordinating concurrent processes" Acta Informatica 5, pp. 297–332 (1975).Google Scholar
- [Manna 81]Z. MANNA and A. PNUELI "Verification of concurrent programs: The temporal framework" Intern. Summer School, Theoretical Foundations of Programming Methodology, Munich, July 1981.Google Scholar
- [Queille 81]J.P. QUEILLE "The CESAR system: An aided design and certification system for distributed applications" Proc. 2nd Int. Conf. on Distributed Computing Systems, April 1981, pp. 149–161.Google Scholar
- [Rescher 71]N. RESCHER and A. URQUHART "Temporal Logic" Springer Verlag, Vienna, 1971.Google Scholar
- [Schwartz 81]R.L. SCHWARTZ and P.M. MELLIAR-SMITH "Temporal logic specification of distributed systems" Proc. 2nd Int. Conf. on Distributed Computing Systems, April 1981, pp. 46–454.Google Scholar
- [Sifakis 79]J. SIFAKIS "A unified approach for studying the properties of transition systems" Research Report RR No 179, IMAG December 1979 (Revised December 1980), to appear in TCS January 1982.Google Scholar
- [SIGPN 81]Special Interest Group: Petri nets and related system models. Newsletter No 7, Feb. 1981, p-. 17–20.Google Scholar