Extensions and Generalization of the Saturation Algorithm in Model Checking

Formal verification is a collective name of techniques that aim to prove that a system design or implementation satisfies its required properties. Formally proving something is much more challenging than testing and simulation: the proof has to cover every possible case, not just selected executions of the system. This kind of rigorous analysis is often used in the development of safety-critical hardware and software systems, commonly found in the automotive, railway or aerospace industries. Model checking is an automated formal verification technique that evaluates the possible states and behaviors of a system design with regard to a formal specification. This is a challenging task because real-life systems usually have an enormous number of possible states, all (or most) of which has to be checked for violations of the specified properties. Symbolic model checking techniques, and in particular the saturation algorithm have been introduced to efficiently handle these large state spaces in many (common) cases. Research of the saturation algorithm has yielded different variants suitable for different problems, but the range of possible applications are still not fully covered. This dissertation presents further results in the fields of efficient analysis of models with prioritized transitions and the model checking of linear temporal logic properties, a class of specification logic that is prevalent but hard to analyze. Furthermore, investigation of different variants of saturation inspired an enhanced and more general version of the original algorithm, which is the culmination of this research. Thesis 1 presents an approach to efficiently analyze Generalized Stochastic Petri Nets, a formalism suitable for the modeling of extra-functional aspects of a system. These models have prioritized transitions, which is challenging for saturation. The presented approach decomposes the priority-related aspects from the effect of the transition and achieves better scaling compared to previous approaches, expanding the scope of models on which analysis is feasible. Thesis 2 is about the model checking of linear temporal logic properties, which is a complex algorithm only partially supported by saturation. It investigates how saturation can be used in different phases of the algorithm and introduce extensions accordingly. Furthermore, Thesis 2 introduces new algorithms for the different subtasks of this model checking problem, tailored to work with saturation and combining the best of previously known approaches. The combination of these building blocks provides a scalable, optimized symbolic model checking algorithm for linear temporal logic properties. Thesis 3 introduces an enhanced version of the saturation algorithm. By identifying the common ideas, the enhanced version generalizes previous variants in a single, more powerful algorithm that can directly tackle a wider range of problems. Enhancement can be observed on performance as well: in certain types of models, the enhanced version outperforms the original saturation algorithm by orders of magnitude, while it has the same performance in other cases.Successfully defended on February 18, 2020