POMC. Toward a model checking tool for operator precedence languages

A significant contribution from the field of formal methods is providing software engineers with increasingly powerful and efficient tools to model, analyze and verify the properties and the behavior of computer programs. Recently a promising line of research has stemmed from Operator Precedence Languages (OPL), a family of formal languages introduced by Robert W. Floyd in the late sixties. In particular, it has been shown how OPL, despite enjoying considerable expressive power, are characterized by algebraic and logic properties that make them particularly suitable for formal verification techniques. A major step in this direction has been taken with the introduction of temporal logics based on OPL, such as POTL (Precedence Oriented Temporal Logic). Procedural programs can be accurately modeled as OPL, and POTL can then be used to formulate specifications on structural elements like procedure calls, exceptions, handlers, etc. We made a first attempt to reap the practical benefits of this approach with the creation of POMC, a newly born verification tool built in the Haskell programming language. The tool is currently capable of performing runtime verification of POTL formulas on finite strings. In this dissertation, we review the work done to develop POMC up to the latest version, illustrating the main design and architectural choices taken. We also present some concrete usage examples, and discuss the performance of POMC in light of empirical results. We finally suggest how POMC can be extended to implement OPL-based model checking.

Un importante contributo da parte del campo dei metodi formali è quello di fornire agli ingegneri del software strumenti sempre più potenti ed efficienti per modellare, analizzare e verificare le proprietà ed il comportamento dei programmi. Un promettente filone di ricerca si è ultimamente incentrato sugli Operator Precedence Languages (OPL), una famiglia di linguaggi formali introdotta da Robert W. Floyd sul finire degli anni sessanta. In particolare, è stato mostrato come gli OPL, nonostante il loro considerevole potere espressivo, siano caratterizzati da proprietà algebrico-logiche che li rendono particolarmente adatti per le tecniche di verifica formale. Un deciso passo avanti in questa direzione è stato effettuato con l'introduzione di logiche temporali basate sugli OPL, come ad esempio POTL (Precedence Oriented Temporal Logic). I programmi procedurali possono essere fedelmente modellati come OPL, e POTL può poi essere utilizzata per formulare specifiche elaborate su elementi strutturali come chiamate a procedure, eccezioni, handlers, ecc. Un primo tentativo di sfruttare i benefici pratici di questo approccio si è concretizzato nella creazione di POMC, un tool di verifica di recente concezione scritto nel linguaggio di programmazione Haskell. Al momento il software è in grado di effettuare la runtime verification di formule POTL su stringhe finite. Questa tesi si propone di esporre il lavoro fatto per sviluppare POMC fino alla versione corrente, illustrando le principali scelte progettuali e architetturali fatte. Sono inoltre presentati degli esempi d'uso concreti, e viene discusso il livello di performance raggiunto alla luce di una serie di risultati empirici. Si suggerisce infine come POMC possa essere esteso per implementare funzionalità di model checking basate sugli OPL.