Skip to Main content Skip to Navigation
Conference papers

Formally Verifying Sequence Diagrams for Safety Critical Systems

Abstract : 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 formal safety requirements for safety critical systems in an incremental way, where the scenarios are progressively refined after checking the consistency of the requirements. As before, the semantics of these scenarios are expressed by transforming them into an intermediate semantic model amenable to formal verification. We rely on the Clock Constraint Specification Language (CCSL) as the intermediate semantic language. An SMT-based analysis tool called MyCCSL is used to check consistency of the sequence diagrams. We compare these requirements against actual execution traces to prove the validity of our transformation. 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. Finally, the whole process is illustrated on partial requirements for a railway transit system.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-03121933
Contributor : Frédéric Mallet <>
Submitted on : Tuesday, January 26, 2021 - 4:56:24 PM
Last modification on : Monday, March 1, 2021 - 9:49:17 AM

File

Tase2020.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03121933, version 1

Collections

Citation

Xiaohong Chen, Frédéric Mallet, Xiaoshan Liu. Formally Verifying Sequence Diagrams for Safety Critical Systems. TASE 2020 - 14th International Symposium on Theoretical Aspects of Software Engineering, Dec 2020, Hangzhou, China. ⟨hal-03121933⟩

Share

Metrics

Record views

31

Files downloads

90