Basic-REAL: Integrated approach for design, specification and verification of distributed systems

Abstract

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 modelchecking. 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.