Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/79711
Título: | Towards model checking electrum specifications with LTSmin |
Autor(es): | Cancelinha, Bruno Miguel Sousa |
Orientador(es): | Cunha, Alcino Almeida, Paulo Sérgio |
Palavras-chave: | Alloy Electrum Model checking LTSmin Partial order reduction TLA+ |
Data: | 23-Dez-2019 |
Resumo(s): | Model checking é uma técnica comum de verificação; garante a consistência e integridade de
qualquer sistema fazendo uma exploração exaustiva de todos os possíveis estados. Devido à
grande quantidade de intercalações possíveis entre eventos, modelos de sistemas distribuídos
muitas vezes acabam por gerar um número de estados muito grande. Nesta dissertação
vamos explorar os efeitos de partial order reduction — uma técnica para mitigar os efeitos
da explosão de estados — implementando uma linguagem semelhante ao Electrum com
LTSmin. Vamos também propor um event layer por cima do Electrum e uma análise sintática
para extrair informação necessária para que esta técnica possa ser implementada. Model checking is a common verification technique to guarantee the consistency and integrity of any system by an exhaustive exploration of all possible states. Due to the large amount of interleavings, models on distributed systems often end up with a huge state-space. In this dissertation we will explore the effects of partial order reduction — a technique to mitigate the effects of this state-explosion problem — by implementing an electrum-like language with LTSmin. We will also propose an event layer over Electrum and a syntactic analysis to extract valuable information for this technique to be implemented. |
Tipo: | Dissertação de mestrado |
Descrição: | Dissertação de mestrado integrado em Engenharia Informática |
URI: | https://hdl.handle.net/1822/79711 |
Acesso: | Acesso aberto |
Aparece nas coleções: | BUM - Dissertações de Mestrado DI - Dissertações de Mestrado |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Bruno Miguel Sousa Cancelinha.pdf | Dissertação de Mestrado | 1,1 MB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons