Dealing with incompleteness in automata-based model checking
- Day - Time: 26 May 2016, h.15:00
- Place: Area della Ricerca CNR di Pisa - Room: C-29
Speakers
- Paola Spoletini (Professor at Kennesaw State University, GA, USA)
Referent
Abstract
A software specification is often the result of an iterative process that transforms an initial incomplete model through refinement decisions. A model is *incomplete* because decisions about certain functionalities are postponed to a later stage and perhaps even delegated to third parties. A delayed functionality may be later detailed, and alternative solutions are often explored to evaluate tradeoffs.
*Model checking* has been proposed as a technique to verify that the model of the system under development is compliant with its requirements. However, most classical model checking algorithms assume that a complete model and fully specified requirements are given: they do not support incompleteness. Furthermore, as changes are made, by either adding a part that was previously not specified or by revisiting a previous design decision, the whole model of the system must be verified from scratch. A verification- driven design process would instead benefit from the ability to apply formal verification at any stage, hence also to incomplete models. After any change, it is desirable that only a minimal part of the modelâ??the portion affected by the change, called replacementâ??is analyzed, thus reducing the verification effort.
In our work we propose an approach that extends the classical automata-based model checking procedure for LTL properties to deal with incompleteness. *The proposed model checking approach evaluates if* *a property holds or not for an incomplete model.* In addition, when satisfaction of the property depends on the incomplete partsâ??indicating delayed functionalitiesâ??it computes a constraint that must be satisfied by the replacement to ensure satisfaction of the property. The constraint is then verified on the replacement.