Publication
Parallel verification of dynamic systems with rich configurations
| Summary: | 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. |
|---|---|
| Main Authors: | Pessoa, Eduardo José Dias |
| Subject: | Alloy 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 Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática |
| Year: | 2016 |
| Country: | Portugal |
| Document type: | master thesis |
| Access type: | open access |
| Associated institution: | Universidade do Minho |
| Language: | English |
| Origin: | RepositóriUM - Universidade do Minho |
| Summary: | 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. |
|---|
Funded activities
No funded projects found.