Basic protocols, message sequence charts, and the verification of requirements specifications

Message sequence charts are a widely used notation to express requirements specifications of multi-agent systems. The semantics of message sequence charts can be defined algebraically in the theory of interaction of agents and environments. Using this algebra, one can split message sequence chart scenarios into sets of Hoare triples consisting of precondition, the specification of a finite process, and a postcondition. We refer to such triples as “basic protocols”. In this paper, we discuss tools to prove properties of systems described as basic protocols, such as the completeness (at each of its stages the system behavior has a possible continuation) and consistency (at each stage the system behavior is deterministic) of the specification, or the correspondence of the specified behavior to given scenarios. Together, these tools constitute a powerful environment for the formal verification of requirements specifications expressed through message sequence charts.