Formal Verification of Lack of Existence of Illegal Scenarios in the Requirements of Distributed Systems

M. Moshirpour and B.H. Far (Canada)


Distributed systems, Emergent behaviour, Scenariobased specifications, Message sequence charts.


The lack of central control in distributed systems makes the analysis and design of such systems a challenging task. In fact many faults are introduced into the system at this stage of the software development life cycle. Therefore design validation of distributed software systems prior to the implementation phase is greatly desirable as it results in huge savings in time and cost. An effective and efficient approach to describing the requirements of distributed systems is using scenarios. Scenarios are commonly represented using message sequence charts or sequence diagrams. Although scenario-based specifications provide a powerful medium to present information, they are also prone to subtle deficiencies such as incompleteness and potential contradictions among scenarios. Moreover for the development of larger distributed systems, it is often desirable to ensure certain scenarios do not emerge in the system's behaviour. This research proposes systematic and automated methodologies to ensure the lack of emergent behaviour in distributed systems using scenario based specifications. These methodologies are demonstrated using a case study of a common online commerce system.

Important Links:

Go Back