Title :

Formal Verification of Software-Intensive Systems Architectures Described with Piping and Instrumentation Diagrams

Author(s) :

Mesli, Soraya [Auteur]
ArchWare
Kesraoui, Djamal [Auteur]
Oquendo, Flavio [Auteur]
ArchWare
Bignon, Alain [Auteur]
Toguyéni, Armand [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Berruet, Pascal [Auteur]
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) [Lab-STICC]

Conference title :

Proceedings of the 10th European Conference on Software Architecture (ECSA 2016)

City :

Copenhagen

Country :

Danemark

Start date of the conference :

2016-11-28

Publisher :

Springer

English keyword(s) :

System architectures
Software-intensive systems
Architectural style
Formal verification
Alloy
P&ID

HAL domain(s) :

Informatique [cs]/Génie logiciel [cs.SE]

English abstract : [en]

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 ...
Show more >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.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL