masterThesis
FormAr: software architecture formalization for critical applications
Fecha
2022-02-11Registro en:
DIAS, Fagner Morais. FormAr: software architecture formalization for critical applications. 2022. 124f. Dissertação (Mestrado em Sistemas e Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2022.
Autor
Dias, Fagner Morais
Resumen
Errors during the software development may give rise to flaws in the system
that can cause important damages. One of the most important stages in the
software development process is modelling the system architecture, possibly
using software architecture description languages (ADLs). The ADLs currently
adopted by industry for software-intensive systems are mostly semi-formal
and essentially based on SysML and specialized profiles. These ADLs allow
describing the structure and the behavior of the system. Besides, it is possible to
generate executable models or produce code in a target programming language
and simulate its behaviour. This, however, does not constitute a proof that the
system is correct or safe. This work proposes a novel approach for empowering
SysML-based ADLs with formal verification tools supported by model checking.
It presents a CSP-based semantics to SysADL models. Furthermore, this
work presents how correctness properties can be formally specified using CSP,
and how the FDR4 refinement model-checker can verify these correctness
properties. Finally, we present the new extension to SysADL studio that
allows the automated transformation from SysADL architecture descriptions to
CSP processes and the verification of important system correctness properties.
The whole approach is illustrated via a case study, which is also part of this
document. This case study demonstrates the usefulness of our approach in practice.