Please use this identifier to cite or link to this item: https://hdl.handle.net/1822/47746

Full metadata record
DC FieldValueLanguage
dc.contributor.advisorMacedo, Nuno Filipe Moreirapor
dc.contributor.advisorCunha, Alcinopor
dc.contributor.authorPessoa, Eduardo José Diaspor
dc.date.accessioned2017-11-24T11:19:22Z-
dc.date.available2017-11-24T11:19:22Z-
dc.date.issued2016-12-10-
dc.date.submitted2016-10-21-
dc.identifier.urihttps://hdl.handle.net/1822/47746-
dc.descriptionDissertação de mestrado em Engenharia Informática (área de especialização em Informática)por
dc.description.abstractModel 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.abstractModel-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.sponsorshipThis 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.isoengpor
dc.rightsopenAccesspor
dc.subjectAlloypor
dc.subjectElectrumpor
dc.subjectTLApor
dc.subjectFormal specification languagepor
dc.subjectDynamic systemspor
dc.subjectRich configurationspor
dc.subjectModel-Checkingpor
dc.subjectParallel verificationpor
dc.subjectLinguagem de especificação formalpor
dc.subjectSistemas dinâmicospor
dc.subjectConfigurações ricaspor
dc.subjectVerificação de modelospor
dc.subjectVerificação paralelapor
dc.titleParallel verification of dynamic systems with rich configurationspor
dc.title.alternativeVerificação paralela de sistemas dinâmicos com configurações ricaspor
dc.typemasterThesiseng
dc.identifier.tid201615711por
thesis.degree.grantorUniversidade do Minhopor
sdum.degree.grade16 valorespor
sdum.uoeiEscola de Engenhariapor
dc.subject.fosEngenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informáticapor
Appears in Collections:BUM - Dissertações de Mestrado
DI - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Eduardo José Dias Pessoa.pdfTese1,06 MBAdobe PDFView/Open

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 ORCID