×

Basic-REAL: Integrated approach for design, specification and verification of distributed systems. (English) Zbl 1057.68643

Butler, Michael (ed.) et al., Integrated formal methods. 3rd international conference, IFM 2002, Turku, Finland, May 15–18, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43703-7). Lect. Notes Comput. Sci. 2335, 69-88 (2002).
Summary: We suggest a three-level integrated approach to design, specification and verification of distributed system. The approach is based on a newly designed specification language Basic-REAL (bREAL) and comprises (I) translation of a high-level design of distributed systems to executional specifications of bREAL, (II) presentation of high-level properties of distributed systems as logical specifications of bREAL, (III) problem-oriented compositional deductive reasoning coupled with model-checking. The paper presents syntax and semantics of bREAL in formal and informal levels, some meta-properties of this language (namely, stuttering invariance and interleaving concurrency), proof-principles and model-checking for progress properties. An illustrative example (Passenger and Vending Machine) is also presented.
For the entire collection see [Zbl 0992.00052].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

REAL92
PDFBibTeX XMLCite
Full Text: Link