Temporal logic and model checking for operator precedence languages: theory and applications

The growing ubiquity of computer systems in every industrial sector has posed increasingly demanding challenges, one of the most crucial being the verification of adherence of mission- and safety-critical systems to their requirements. One of the most successful and popular techniques that have been developed for this objective is model checking. It consists of the formal specification of the system’s requirements by means of a logic formalism, in the generation of a model of the system in exam by using an operational or denotational formalism, and in the subsequent automatic and exhaustive verification of the adherence of the latter to the former. The capabilities of this process depend on the choice of such formalisms. The most classical thereof are Linear Temporal Logic (LTL), Computation Tree Logic (CTL) and CTL*. In particular, LTL maintains the same expressive power as First-Order Logic (FOL), while providing a model-checking procedure which is only exponential in specification size, and not non-elementary as FOL. However, LTL only allows to express properties in the realm of regular languages. Recently, the literature has seen considerable efforts in the direction of extending the expressive power of temporal logic towards larger language classes. The most notable of them is the work on temporal logics based on Visibly Pushdown Languages (VPLs), which led to the introduction of the logic CaRet, and of the First-Order complete NWTL. VPL are a subclass of Deterministic Context-Free Languages (DCFLs), and they are only slightly more expressive than parenthesis languages. The main motivation of this line of research is the verification of procedural programs: the one-to-one correspondence between function calls and returns can only be modeled by a context-free language. This thesis develops a model-checking framework based on Operator Precedence Languages (OPLs). OPLs, another subclass of DCFLs, are significantly more expressive than VPLs and, consequently, regular languages. Being suitable for describing the syntax of real-world programming languages, they could dramatically extend the properties expressible in system specifications. In particular, they enable verification of programs with exceptions, which VPL-based formalisms could not do. In this thesis, we present two temporal logic formalisms capable of expressing OPL properties. The first one, OPTL, is a first attempt at this task, for which we develop a model-checking procedure. Unfortunately, OPTL is strictly less expressive than FOL. Thus, we introduce a better logic, POTL, for which we prove equivalence to FOL, and develop and implement an automata-theoretic model-checking procedure. We demonstrate the applicability of the resulting tool through case studies, showing promising results.

La crescente diffusione dei calcolatori elettronici in tutti i settori industriali pone sfide sempre più impegnative. Una delle più cruciali è la verifica dell'aderenza di sistemi mission- e safety-critical ai propri requisiti. Una delle tecniche più di successo che sono state sviluppate con questo scopo è il model checking. Esso consiste nella specifica formale dei requisiti del sistema con un formalismo logico, nella generazione di un modello del sistema in esame usando un formalismo operazionale o denotazionale, e nella successiva verifica automatica ed esaustiva dell'aderenza del secondo al primo. Le potenzialità di questo processo dipendono dalla scelta di tali formalismi. I più classici di essi sono Linear Temporal Logic (LTL), Computation Tree Logic (CTL) e CTL*. In particolare, LTL mantiene la stessa potenza espressiva della logica del prim'ordine, ma permette una procedura di model checking che è soltanto esponenziale nelle dimensioni della specifica, mentre quella della logica del prim'ordine è non-elementare. Tuttavia, LTL permette di esprimere proprietà ristrette ai soli linguaggi regolari. Recentemente, la letteratura scientifica ha visto sforzi considerevoli volti all'estensione della potenza espressiva delle logiche temporali verso classi di linguaggi più ampie. Il più notevole di essi è il lavoro sulle logiche temporali basate sui Visibly Pushdown Languages (VPL), che ha portato all'introduzione della logica CaRet, e di NWTL, completa rispetto alla logica del prim'ordine. I VPL sono una sotto-classe dei Linguaggi Liberi dal Contesto Deterministici (LLCD), e sono solo leggermente più espressivi dei linguaggi a parentesi. La motivazione principale di questa linea di ricerca è la verifica dei programmi procedurali: la corrispondenza uno-a-uno tra le chiamate di funzione e i loro "ritorni" può essere modellata soltanto con un linguaggio libero dal contesto. Questa tesi sviluppa una tecnica per il model checking basata sugli Operator Precedence Languages (OPL). Gli OPL, un'altra sotto-classe degli LLCD, sono significativamente più espressivi dei VPL e, di conseguenza, dei linguaggi regolari. Essendo adatti a descrivere la sintassi di linguaggi di programmazione veri e propri, possono estendere significativamente le proprietà esprimibili nelle specifiche di sistema. In particolare, permettono la verifica dei programmi con le eccezioni, cosa che i formalismi basati su VPL non possono fare. In questa tesi, presentiamo due logiche temporali in grado di esprimere proprietà OPL. Il primo, OPTL, è un tentativo iniziale, per cui sviluppiamo una procedura di model checking. Sfortunatamente, OPTL è strettamente meno espressiva della logica del prim'ordine. Quindi, introduciamo una logica migliore, POTL, per la quale dimostriamo l'equivalenza con la logica del prim'ordine, e sviluppiamo ed implementiamo una procedura di model checking basata su automi. Mostriamo l'applicabilità dello strumento risultante grazie a dei casi di studio, che mostrano risultati promettenti.