Building deductive proofs of LTL properties for iteratively refined systems

Modern software development processes are evolving from sequential to increasingly agile and incremental paradigms. Verification, unavoidable step of a correct software production, cannot get left behind by this new quickly changing practice. Advances in verification techniques have been considerable in the past years, and feasibility has been achieved on always greater systems. Nevertheless, we believe that verification and modern development processes are still not going at the same pace in terms of incrementality. Classical verification algorithms are applied when a complete specification of the model to verify is available, and several development costs and efforts have been already spent. Today more than ever, the description of a system changes continuously during the phase of analysis, asking for periodical adjustments in its specifications. Various parts are often only sketched waiting for further enrichment, which is sometimes delegated to third parties. The classical scenario is, therefore, not applicable anymore: it becomes essential coming up with light iterative methods formal verification methods, that can be applied also to incomplete models at each stage of the design and development phases, contributing more incisively to developers choices. With particular focus on two main verification techniques, model checking and deductive verification, we study a way to integrate them into this incremental context. The idea is to supply each step of the design phase with a way to prove behaviors of incomplete systems or only single components. Step-wise model checking can be augmented by a simple incremental deductive system generator that justifies why the system actually meets some requested temporal specification (if this is the case). This kind of infrastructure can bring a useful contribution in cases and refinements where matters of safety, starvation or liveness are critical, and, in general, guide the choices of the developer that faces different designs. The main idea is to combine two approaches presented in literature: on one side we would like to exploit a procedure of model checking that supports systems that are not completely specified, on the other side we study a mechanism to build deductive proofs using information gathered during model checking. This thesis deals with the construction of these incremental deductive proofs of linear temporal logic properties in incomplete systems that are completed progressively when the system gets refined.

I processi di sviluppo del software, un tempo sequenziali, si stanno ora evolvendo verso paradigmi sempre più agili ed incrementali. La verifica formale, fase fondamentale del processo di produzione del software, deve dunque adattarsi a queste pratiche in continuo cambiamento. I progressi nelle tecniche di verifica sono stati considerevoli negli ultimi anni, soprattutto grazie alla loro attuabilità su sistemi di sempre maggiori dimensioni. Ciò nonostante, notiamo ancora un disallineamento tra le tecniche di verifica ed i processi di sviluppo moderni, in termini di metodologie incrementali. Gli algoritmi di verifica classici vengono applicati in fasi già conclusive, quando le specifiche fornite sono pressoché complete e diversi costi di sviluppo sono già stati sostenuti. Oggigiorno, però, la descrizione di un sistema durante la fase di analisi è in continua evoluzione e richiede dunque frequenti modifiche alle specifiche. Infatti, diversi moduli vengono spesso solo abbozzati in attesa di un successivo arricchimento o direttamente affidati a terze parti. Lo scenario classico non è dunque più attuale: diventa essenziale elaborare metodi di verifica più leggeri ed iterativi, applicabili anche a modellizzazioni incomplete del software durante qualsiasi fase della pianificazione e dello sviluppo, in modo da contribuire in maniera più incisiva alle scelte degli sviluppatori. Incentrando la nostra ricerca sulle tecniche di model checking e verifica deduttiva, valutiamo una soluzione per integrarle nel contesto incrementale. L'obbiettivo è quello di affiancare ad ogni fase del design una procedura che prova i comportamenti di interi sistemi incompleti e di loro singoli moduli, fornendo supporto per integrare le informazioni ottenute in modo frammentato. Mostriamo come il model checking incrementale può essere arricchito da un semplice generatore di prove deduttive che, quando il sistema in analisi rispetta un dato requisito, ne giustifica il perché. Questo tipo di supporto può fornire un contributo utile in ambiti in cui proprietà di safety, starvation e liveness sono critiche, e in generale guidare lo sviluppatore software che affronta qualsiasi tipo di design. In questa tesi combiniamo insieme due diversi approcci provenienti dalla letteratura: da una parte utilizziamo una procedura di model checking che supporta sistemi specificati in modo incompleto [#MSG15], dall'altra studiamo il meccanismo di costruzione di prove deduttive sfruttando direttamente le informazioni generate dalla procedura di model checking [#PZ01, #PPZ01]. Dopo aver introdotto il nostro lavoro nel panorama della verifica formale, presentiamo gli approcci che hanno ispirato il nostro lavoro; poi introduciamo il nostro contributo, una tecnica di verifica ibrida applicabile in maniera flessibile a specifiche parziali confrontate con requisiti espressi in logica temporale, e risolviamo la problematica di comporre insieme prove deduttive ottenute a diversi livelli di dettaglio. Successivamente, presentiamo la validazione della nostra tecnica ottenuta tramite il tool ChIPS. Infine, chiariamo il nostro approccio tramite un case study che descrive un sistema di invio di messaggi e concludiamo descrivendo lo stato dell'arte ed i futuri sviluppi di questo lavoro.