Navegando por Autor "Dias, Fagner Morais"
Agora exibindo 1 - 2 de 2
- Resultados por página
- Opções de Ordenação
Dissertação FormAr: software architecture formalization for critical applications(Universidade Federal do Rio Grande do Norte, 2022-02-11) Dias, Fagner Morais; Oliveira, Marcel Vinicius Medeiros; http://lattes.cnpq.br/1756952696097255; http://lattes.cnpq.br/9457736660395718; Batista, Thais Vasconcelos; https://orcid.org/0000-0003-3558-1450; http://lattes.cnpq.br/5521922960404236; Oquendo, FlavioErros durante o desenvolvimento do software podem originar falhas no sis- tema que podem causar danos importantes. Uma das etapas mais importantes no processo de desenvolvimento de software é a modelagem da arquitetura do sistema, possivelmente usando linguagens de descrição de arquitetura de software (ADLs). As ADLs atualmente adotadas pela indústria para sistemas intensivos de software são em sua maioria semiformais e essencialmente base- adas em SysML e perfis especializados. Essas ADLs permitem descrever a estrutura e o comportamento do sistema. Além disso, é possível gerar modelos executáveis ou gerar código em uma linguagem de programação alvo e simular seu comportamento. Isso, no entanto, não constitui prova de que o sistema está correto ou seguro. Este trabalho propõe uma nova abordagem para capacitar ADLs baseadas em SysML com verificação formal suportada por verificação de modelo. Ele apresenta uma semântica baseada em CSP para modelos SysADL. Além disso, este trabalho apresenta como as propriedades de correção podem ser formalmente especificadas usando CSP, e como o verificador de refinamento de modelos FDR4 pode verificar essas propriedades de correção. Finalmente, apresentamos a nova extensão do SysADL studio que permite a transformação automatizada de descrições de arquitetura SysADL para processos CSP e a verificação de propriedades importantes de correção do sistema. Toda a abordagem é ilustrada por meio de um estudo de caso, que também faz parte deste documento. Este estudo de caso demonstra a utilidade de nossa abordagem na prática.TCC Towards software architecture formalization(Universidade Federal do Rio Grande do Norte, 2023-06-13) Dias, Fagner Morais; Oliveira, Marcel Vinicius Medeiros; 0000-0002-3023-2748; http://lattes.cnpq.br/1756952696097255; 0000-0001-7398-8628; http://lattes.cnpq.br/9457736660395718; Batista, Thais Vasconcelos; 0000-0003-3558-1450; http://lattes.cnpq.br/5521922960404236; Leite, Jair Cavalcanti; http://lattes.cnpq.br/8133660776746187Errors 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.