The talk will present 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.

Syntax and semantics of bREAL will be described in formal and informal levels. Some meta-properties of this language will be discussed (namely, stuttering invariance and interleaving concurrency). Deductive proof-principles and model-checking will be presented for verification of progress properties. All features of the approach will be illustrated by an example (Passenger and Vending Machine).

DATE: November 27, 2002, Wednesday @ 15:40
PLACE: EA-409