Paper Info
Title
Formal Verification of Software-Intensive Systems Architectures Described with Piping and Instrumentation Diagrams.
Abstract
Socio-technical systems are increasingly becoming software-intensive. The challenge now is to design the architecture of such software-intensive systems for guaranteeing not only its correctness, but also the correctness of its implementation. In social-technical systems, the architecture (including software and physical elements) is described in terms of Piping and Instrumentation Diagrams (P&ID). The design of these P&ID is still considered an art for which no rigorous design support exists. In order to detect and eliminate architectural design flaws, this paper proposes a formal-based automated approach for the verification of the essential architecture "total correctness" properties, i.e. compatibility, completeness, consistency, and correctness. This approach is based on the definition of an architectural style for P&ID design in Alloy. We use MDE to automatically generate Alloy models from a P&ID and check their compatibility with the style and its completeness, consistency, and correctness properties. Our approach is presented through an industrial case study: the system of storage and production of freshwater for a ship.
Year
DOI
Venue
2016
10.1007/978-3-319-48992-6_16
Lecture Notes in Computer Science
Keywords
Field
DocType
System architectures,Software-intensive systems,Architectural style,Formal verification,Alloy,P&ID
Architecture,Programming language,Compatibility (mechanics),Computer science,Correctness,Real-time computing,Software,Piping,Completeness (statistics),Architectural style,Formal verification
Conference
Volume
ISSN
Citations 
9839
0302-9743
1
PageRank 
References 
Authors
0.36
8
6
Name
Order
Citations
PageRank
Soraya Mesli-Kesraoui110.36
Djamal Kesraoui210.36
Flávio Oquendo336387.03
Alain Bignon463.27
Armand Toguyéni5366.59
Pascal Berruet6209.27