PhD Alumni

Spoletini Paola

Present position: Assistant Professor

Thesis title:  Verification of Temporal Logic Specifications via Model Checking
Advisor:  Pierluigi San Pietro
Research area:  Advanced Software, Architectures and Methodologies
Thesis abstract:  
Critical systems, especially in case of real-time characteristics, require specification, design, and verification methods with high thoroughness, supported by proper tools. Recent progress in the automatic verification techniques find use in this area, but still require further research and design of applications in order to be exploited in common engineering tasks, in particular when time comes into play with its different granularities.
The aim of this thesis is to extend the existing verification techniques, typically built on traditional finite state automata, to treat complex critical systems with time constraints. Such techniques must be based on appropriate formalisms, whose power must be accurately balanced between real systems description capability and possibility of efficient automatization of the verification process.
The TRIO specification language [1], which is a typed first order logic that supports a linear notion of time with both past and future operators (TRIO-in the-small), and can be extended with the typical object oriented programming constructs [2], is an excellent specification language for such systems. But, in
general, TRIO is undecidable; therefore, in order to obtain an entirely automatic verification method, it is necessary to limit TRIO to a decidable subset, disallowing variables, considering the natural numbers as time domain and limiting all the other domains to finite domains. During this research work, we focused on a decidable subset of TRIO, and introduced a new model checking technique based on automata, which allows us to take advantage of TRIO modular aspects. The proposed approach allows the automatic verification of TRIO specification through the Spin model checker. Note that the problem we are dealing with slightly differs from the classical model-checking problem, seeing that, instead of considering an operational model, we use a purely descriptive specification; hence a technique for the verification of models defined both in the past and in the future has been developed. Shortly, the proposed approach is based on an initial separation of the past and future components, always possible by the Gabbay separation theorem. The two components are then differently translated, considering that the past component refers to finite words, since we are considering the natural numbers as temporal domain, and the future component refers to infinite words. Therefore, we propose a translation of the past component to deterministic Büchi automata [4], and of the future component to alternating automata [3], which allow non determinism and parallelism. Both the considered automata are enriched with a set of finite counters, in order to keep track of the quantitative aspect of time, which is part of TRIO. The two components are then merged through the composition of the two automata [4], and the resulting automaton is then translated to Promela, which is Spin input language. Let us notice that the automaton obtained with the composition of the past and future components is still an alternating automaton, while Spin uses Büchi automata. Anyway, an alternating automaton can always be transformed into a Büchi automaton with an exponential explosion in the number of the states; in order to avoid such explosion in the translation to Promela, the automaton obtained with the composition is directly simulated in Promela. The proposed techniques have been implemented in the TRIO2Promela translator, a plug-in for Trident, a platform for the specification and verification of TRIO models, based on Eclipse. With the usage of the translator it has been possible to experimentally validate the proposed technique.
[1] C. Ghezzi, D. Mandrioli, and A. Morzenti. Trio: A logic language for executable specifications of real-time systems. The Journal of Systems and Software, 12(2):107–123, May 1990.
[2] A. Morzenti and P. San Pietro. Object-oriented logic specifications of time
critical systems. ACM Transactions on Software Engineering and Methodologies, 3(1):56–98, January 1994.
[3] A. Morzenti, M. Pradella, P. San Pietro, and P. Spoletini. Model checking of trio specifications in Spin. Proc. 12th International FME Symposium, LNCS,
volume 2805, Sep 2003.
[4] M. Pradella, P. San Pietro, P. Spoletini, and A. Morzenti. Practical model checking of LTL with past. Proc. 1st International Workshop on Automated Technology for Verification and Analysis, December 2003.