Utilize este identificador para referenciar este registo: http://hdl.handle.net/1822/47746

TítuloParallel verification of dynamic systems with rich configurations
Outro(s) título(s)Verificação paralela de sistemas dinâmicos com configurações ricas
Autor(es)Pessoa, Eduardo José Dias
Orientador(es)Macedo, Nuno Filipe Moreira
Cunha, Alcino
Palavras-chaveAlloy
Electrum
TLA
Formal specification language
Dynamic systems
Rich configurations
Model-Checking
Parallel verification
Linguagem de especificação formal
Sistemas dinâmicos
Configurações ricas
Verificação de modelos
Verificação paralela
Data10-Dez-2016
Resumo(s)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.
TipomasterThesis
DescriçãoDissertação de mestrado em Engenharia Informática (área de especialização em Informática)
URIhttp://hdl.handle.net/1822/47746
AcessoopenAccess
Aparece nas coleções:DI - Dissertações de Mestrado
BUM - Dissertações de Mestrado

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
Eduardo José Dias Pessoa.pdfTese1,06 MBAdobe PDFVer/Abrir

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu Currículo DeGóis