Implementing temporal logic queries with PyNuSMV

Details

Supervisors

Pecheur, Charles

Faculty

Ecole polytechnique de Louvain

Degree label

Master [120] en sciences informatiques

Abstract

In recent years, the use of efficient methods that ensure reliable hardware and software systems has been critical, and it will become even more in the future. Indeed, we interact with more and more computing devices in our daily lives, our confidence in these is therefore essential. Model checking is a popular technique to achieve this goal of reliability in hardware and software systems. It is used to verify, in an automatic way, that a given system satisfies or not given properties. This technique is successfully applied in practice on various systems to verify their correctness. However, model checking does not appear to be effective in the process of understanding systems behaviors when their design is opaque. Indeed, while such a process is still possible with model checking, it takes the form of an inefficient trial-and-error approach. Temporal logic query solving was therefore proposed by William Chan at CAV 2000 to fill this gap. This technique is an extension of model checking whose main aim is to understand a model as opposed to merely verifying its correctness. A temporal logic query basically consists of a temporal logic formula where some subformulas are replaced by the special symbol ? representing a "hole" in the formula. The query solving problem then consists of finding the right subformula to fill the hole(s) and make the initial formula satisfied in the considered system. His researches have been well-received in the model checking community, and important developments have been initiated by his paper. Among them, Samer and Veith systematically investigated temporal logic queries, and corrected and extended Chan's work. For the time being, no public implementation of temporal logic queries - as defined by Chan and Samer and Veith - is known. This thesis therefore proposes a first implementation of such queries, in the form of a new Python package, called PyTLQ. In order to fit the needs of this practical implementation in Python, we present adaptations to Chan's and Samer and Veith's algorithms, and we use PyNuSMV - a Python library that gives access to the rich BDD-based functionalities of the well-known model checker NuSMV. Initial experiments demonstrate the applicability of PyTLQ with concrete systems, and show how it can be used to better apprehend systems design and correct potential faulty behaviors.