Enriching SysML-based software architecture descriptions: a model-driven approach
The critical nature of many complex software-intensive systems requires formal architecture descriptions for supporting automated architectural analysis regarding correctness properties. Due to the challenges of adopting formal approaches, many architects have preferred using notations such as UML,...
Na minha lista:
| Autor principal: | |
|---|---|
| Outros Autores: | |
| Formato: | doctoralThesis |
| Idioma: | pt_BR |
| Publicado em: |
Universidade Federal do Rio Grande do Norte
|
| Assuntos: | |
| Endereço do item: | https://repositorio.ufrn.br/handle/123456789/53351 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
| Resumo: | The critical nature of many complex software-intensive systems requires formal architecture descriptions for supporting automated architectural analysis regarding correctness
properties. Due to the challenges of adopting formal approaches, many architects have preferred using notations such as UML, SysML, and their derivatives to describe the structure
and behavior of software architectures. However, these semi-formal notations have limitations regarding the support for architectural analysis, particularly formal verification.
This work investigates how to formally support SysML-based architecture descriptions
to enable the formal verification of software architectures. As a result of this research,
the main contribution is proposing a model-driven approach (MDD) that provides formal semantics to a SysML-based architectural language, SysADL, through a seamless
transformation of SysADL architecture descriptions to the corresponding formal specifications in p-ADL, a well-founded theoretically language based on the higher-order typed
p-calculus. The proposal implementation involves the execution of a four-phase process: (i)
Model-to-Model (M2M) transformation of SysADL models into p-ADL model; (ii) Modelto-text (M2T) transformation of p-ADL models into p-ADL source; (iii) corresponding
executable architecture generation, and architecture validation; and (iv) property verification. The work has other associated contributions to support the 4-phase process: (i) a
denotational semantics to SysADL in p-ADL; (ii) a definition of a process to support the
automated transformation of SysADL models into p-ADL models; (iii) The validation of
the p-ADL architecture generated by the MDD transformation to demonstrate that it is
in accordance with the original SysADL architecture; and (iv) the verification of formal
architectural properties analyzing execution traces. The proposal was implemented and
validated using a Flood Monitoring System architecture. |
|---|