Nowadays, model checking is a wellestablished formal technique for verifying safetycritical systems. However, one of its main disadvantages is the socalled statespace explosion, as it is necessary to examine every possible configuration reached by the execution of the (possibly parallel) system. This issue is of exponential order and still remains a fundamental challenge in model checking research. It is therefore crucial to find methods that can either manipulate large sets of configurations (states) at a single time (symbolic methods), or let us forget the problem of checking all the possible parallel interleavings by reducing the amount of states to check without losing any significance (reduction methods). The majority of the existing statereducing methods are mostly based on Partial Order Reduction (POR) and Transaction Reduction (TR). Both reduction methods rely on the concept of (in)dependence between the execution order of certain statements. If the order of execution of two statements does not matter then they reach the same state. If so, it is not necessary to check every possible intermediate state the parallel system may witness. POR algorithms generally perform a selective statespace search by exploring a only a subset of the reachable states, whereas TR algorithms merge multiple sequential statements and disregard the states reached in between. This thesis focuses on finding new methods for tackling the statespace explosion and assessing their effectiveness. To this purpose, the first contribution is the systematic presentation of different POR and TR techniques in a single formal setting in order to ease their understanding. The main innovative contribution consists in a novel dynamic TR method based on a concept of independence that is called weakly conditional. The new method is presented, implemented and successively tested against other existing methods to see what degree of improvement is made.
Nowadays, model checking is a wellestablished formal technique for verifying safetycritical systems. However, one of its main disadvantages is the socalled statespace explosion, as it is necessary to examine every possible configuration reached by the execution of the (possibly parallel) system. This issue is of exponential order and still remains a fundamental challenge in model checking research. It is therefore crucial to find methods that can either manipulate large sets of configurations (states) at a single time (symbolic methods), or let us forget the problem of checking all the possible parallel interleavings by reducing the amount of states to check without losing any significance (reduction methods). The majority of the existing statereducing methods are mostly based on Partial Order Reduction (POR) and Transaction Reduction (TR). Both reduction methods rely on the concept of (in)dependence between the execution order of certain statements. If the order of execution of two statements does not matter then they reach the same state. If so, it is not necessary to check every possible intermediate state the parallel system may witness. POR algorithms generally perform a selective statespace search by exploring a only a subset of the reachable states, whereas TR algorithms merge multiple sequential statements and disregard the states reached in between. This thesis focuses on finding new methods for tackling the statespace explosion and assessing their effectiveness. To this purpose, the first contribution is the systematic presentation of different POR and TR techniques in a single formal setting in order to ease their understanding. The main innovative contribution consists in a novel dynamic TR method based on a concept of independence that is called weakly conditional. The new method is presented, implemented and successively tested against other existing methods to see what degree of improvement is made.
A Dynamic Transaction Reduction Theorem based on Weak Conditional Independence
BRIAN, FEDERICO
2022/2023
Abstract
Nowadays, model checking is a wellestablished formal technique for verifying safetycritical systems. However, one of its main disadvantages is the socalled statespace explosion, as it is necessary to examine every possible configuration reached by the execution of the (possibly parallel) system. This issue is of exponential order and still remains a fundamental challenge in model checking research. It is therefore crucial to find methods that can either manipulate large sets of configurations (states) at a single time (symbolic methods), or let us forget the problem of checking all the possible parallel interleavings by reducing the amount of states to check without losing any significance (reduction methods). The majority of the existing statereducing methods are mostly based on Partial Order Reduction (POR) and Transaction Reduction (TR). Both reduction methods rely on the concept of (in)dependence between the execution order of certain statements. If the order of execution of two statements does not matter then they reach the same state. If so, it is not necessary to check every possible intermediate state the parallel system may witness. POR algorithms generally perform a selective statespace search by exploring a only a subset of the reachable states, whereas TR algorithms merge multiple sequential statements and disregard the states reached in between. This thesis focuses on finding new methods for tackling the statespace explosion and assessing their effectiveness. To this purpose, the first contribution is the systematic presentation of different POR and TR techniques in a single formal setting in order to ease their understanding. The main innovative contribution consists in a novel dynamic TR method based on a concept of independence that is called weakly conditional. The new method is presented, implemented and successively tested against other existing methods to see what degree of improvement is made.File  Dimensione  Formato  

Brian_Federico.pdf
accesso riservato
Dimensione
1.08 MB
Formato
Adobe PDF

1.08 MB  Adobe PDF 
The text of this website © Università degli studi di Padova. Full Text are published under a nonexclusive license. Metadata are under a CC0 License
https://hdl.handle.net/20.500.12608/52340