Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/47746
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.advisor | Macedo, Nuno Filipe Moreira | por |
dc.contributor.advisor | Cunha, Alcino | por |
dc.contributor.author | Pessoa, Eduardo José Dias | por |
dc.date.accessioned | 2017-11-24T11:19:22Z | - |
dc.date.available | 2017-11-24T11:19:22Z | - |
dc.date.issued | 2016-12-10 | - |
dc.date.submitted | 2016-10-21 | - |
dc.identifier.uri | https://hdl.handle.net/1822/47746 | - |
dc.description | Dissertação de mestrado em Engenharia Informática (área de especialização em Informática) | por |
dc.description.abstract | 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. | por |
dc.description.abstract | 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. | por |
dc.description.sponsorship | 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. | por |
dc.language.iso | eng | por |
dc.rights | openAccess | por |
dc.subject | Alloy | por |
dc.subject | Electrum | por |
dc.subject | TLA | por |
dc.subject | Formal specification language | por |
dc.subject | Dynamic systems | por |
dc.subject | Rich configurations | por |
dc.subject | Model-Checking | por |
dc.subject | Parallel verification | por |
dc.subject | Linguagem de especificação formal | por |
dc.subject | Sistemas dinâmicos | por |
dc.subject | Configurações ricas | por |
dc.subject | Verificação de modelos | por |
dc.subject | Verificação paralela | por |
dc.title | Parallel verification of dynamic systems with rich configurations | por |
dc.title.alternative | Verificação paralela de sistemas dinâmicos com configurações ricas | por |
dc.type | masterThesis | eng |
dc.identifier.tid | 201615711 | por |
thesis.degree.grantor | Universidade do Minho | por |
sdum.degree.grade | 16 valores | por |
sdum.uoei | Escola de Engenharia | por |
dc.subject.fos | Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática | por |
Aparece nas coleções: | BUM - Dissertações de Mestrado DI - Dissertações de Mestrado |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Eduardo José Dias Pessoa.pdf | Tese | 1,06 MB | Adobe PDF | Ver/Abrir |