Towards model checking electrum specifications with LTSmin

Abstract

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.