Formal semantics and verification of distributed systems presented by Basic-REAL specifications

The specification language Basic-REAL consists of executional and logical specification sublanguages. The first one is based on SDL and differs from it by multiple clock concept, time intervals associated with actions, non-determinism, and rich collection of channel structures. The second one is based on temporal and dynamic logics extended by time intervals. The language includes fairness conditions. The structural operational semantics of Basic-REAL is given by means of transition systems. Throughout the paper an example “Passenger and Slot-Machine” is considered. Our approach to verification of Basic-REAL specifications is based on inductive proof principles supported by model-checking and exploits refinement, fairness conditions, and time constraints.