Verificação paralela de sistemas dinâmicos com configurações ricas
| Autor: | Pessoa, Eduardo José Dias |
|---|---|
| Přispěvatelé: | Macedo, Nuno Filipe Moreira, Cunha, Alcino, Universidade do Minho |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Verificação de modelos
Verificação paralela Electrum TLA Linguagem de especificação formal Model-Checking Formal specification language Engenharia Eletrotécnica Eletrónica e Informática [Engenharia e Tecnologia] Sistemas dinâmicos Dynamic systems Parallel verification Alloy Rich configurations Configurações ricas Engenharia e Tecnologia::Engenharia Eletrotécnica Eletrónica e Informática |
| Zdroj: | Repositório Científico de Acesso Aberto de Portugal Repositório Científico de Acesso Aberto de Portugal (RCAAP) instacron:RCAAP |
| Popis: | Dissertação de mestrado em Engenharia Informática (área de especialização em Informática) Model checking is a technique used to automatically verify a model which represents the specification of some system. To ensure the correctness of the system the verification of both static and dynamic properties is often needed. The specification of a system is made through modeling languages, while the respective verification is made by its model-checker. Most modeling frameworks are not ready to verify models rich in both kind of properties thereby limiting the verification of dynamic systems with rich configurations. Electrum is a modeling language which mixes the best of the Alloy and TLA specification languages, with the capability of handling the problem mentioned above. This language is supported by two model-checking techniques – one bounded and one unbounded. Nonetheless, the Electrum’s bounded model-checker has limitations, thus, this dissertation aims to overcome them with the purpose of improving the analysis procedure of Electrum models, in particular, the definition of a new Electrum’s semantics through a translation into Kodkod as well as the creation of a novel procedure of verifying Electrum models in parallel. Hence, in order to achieve these goals, a temporal extension to the Kodkod constraint solver was implemented. Model-checking é uma técnica utilizada para verificar automaticamente modelos que representam uma determinada especificação de um sistema. Para assegurar a correção de um sistema, e necessário verificar dois tipos de propriedades – dinâmicas e estáticas. A especificação de um sistema é realizada através das linguagens de modelação, enquanto que a verificação do mesmo é feita pelo seu respectivo model-checker. A maior parte das frameworks de modelação não se encontram preparadas para verificar os dois tipos de propriedades, limitando assim a verificação de sistemas dinâmicos com configurações ricas. O Electrum é uma linguagem de modelação que conjuga o melhor de Alloy e TLA, com a capacidade de contornar o problema acima enunciado. Esta linguagem tem associadas duas técnicas de model-checking, uma bounded e outra unbounded. No entanto, o bounded model-checker do Electrum apresenta limitações, portanto, esta dissertação tem como objectivo resolver tais limitações a fim de melhorar o procedimento de análise dos modelos Electrum. Concretamente, a definição de uma nova semântica para o Electrum através de uma tradução para Kodkod, bem como a criação de um novo processo de verificação de modelos Electrum em paralelo. Consequentemente, estes dois últimos objectivos são alcançados através da construção de uma extensão temporal para o Kodkod. This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnológica, within project POCI-01-0145-FEDER-016826. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|