Formally Verifying Sequence Diagrams for Safety Critical Systems - Archive ouverte HAL Access content directly
Conference Papers Year :

Formally Verifying Sequence Diagrams for Safety Critical Systems

(1) , (2, 3, 4, 5) , (1)
1
2
3
4
5

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.
Fichier principal
Vignette du fichier
Tase2020.pdf (623.33 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03121933 , version 1 (26-01-2021)

Identifiers

  • HAL Id : hal-03121933 , version 1

Cite

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⟩
82 View
279 Download

Share

Gmail Facebook Twitter LinkedIn More