bachelorThesis
Towards software architecture formalization
Towards software architecture formalization
Registro en:
DIAS, Fagner Morais. Towards software architecture formalization. Orientador: Marcel Vinicius Medeiros Oliveira. 2023. 75 f. Trabalho de Conclusão de Curso (Graduação em Engenharia de Software) - Departamento de Informática e Matemática Aplicada, Universidade Federal do Rio Grande do Norte, Natal, 2023.
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. 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.