Formally verifying consistency of sequence diagrams for safety critical systems

UML interactions, aka sequence diagrams, are frequently used by engineers to describe expected scenarios of good or bad behaviors of systems under design, as they provide allegedly a simple enough syntax to express a quite large variety of behaviors. This paper uses them to express safety requirements for safety critical systems in an incremental way, where the scenarios are progressively refined after checking the consistency of the requirements. The semantics of these scenarios are expressed by transforming them into an intermediate semantic model amenable to formal verification. In this paper, we rely on the Clock Constraint Specification Language (CCSL) as the intermediate semantic language. In some sense, sequence diagrams and CCSL constraints both express a family of acceptable infinite traces that must include the behaviors given by the finite set of finite execution traces against which we validate. We compare these requirements to actual execution traces to prove the validity of our transformation. As to check the consistency of the sequence diagrams, we present two verification methods based on SMT and clock graphs respectively. The SMT based method relies on our analysis tool called MyCCSL to analyze CCSL constraints. The clock graph based method transforms CCSL constraints into a clock graph, and does the analysis through traversing the clock graph. Finally, these two methods are evaluated against real cases from the railway transit systems. The results show that the SMT based method provides accurate but slow analysis, while the clock graph based method dramatically increases the verification efficiency aiming at two kinds of typical inconsistencies found by the SMT based method.