Dealing with incompleteness in automata based model checking

The software development process concerns a sequence of design decisions that transforms the initial, high-level model of the system into a fully detailed and verified implementation. This process is based on an iterative decomposition of the model of the system into smaller functionalities. At each iteration, the developer may leave the system deliberately incomplete. Incompleteness arises when the design of some functionalities is postponed to a later development stage or when they are left unspecified (e.g., if they will be developed by third parties). The final, fully specified, model of the system is obtained by refining the incomplete parts. The development process concerns the iterative substitution of the postponed functionalities with sub-modules (replacements) and, eventually, executable code. During this process alternative replacements are often explored to evaluate their tradeoffs. It can also happen that replacements of postponed functionalities are only detected at run time, as in the case of adaptive systems. Formal verification has now become mature. Several techniques allow the designer to check whether the model of the system under development possesses the properties of interest. Formal verification has already been used in practice in several application domains and has also been adopted in many industrial settings. However, there is still a gap between the model checking techniques and the currently used software development lifecycles. Model checking is a technique that found a prominent role in formal verification. Given a model of the system and a formal property, model checking exhaustively analyzes the model of the system to ensure that all of its behaviors satisfy the property of interest. If the property is not satisfied a counterexample is also returned. Mainstream model checking techniques assume that the model of the system and the properties against which it should be verified are completely defined when the verification takes place. However, this assumption is not always valid during the software development process, as we discussed earlier, since models are often incomplete. To support continuous verification during the development process, we should be able to verify incomplete models. By checking incomplete models even initial, incomplete, and high-level descriptions of the system can be verified against their properties, supporting an early error detection. Furthermore, when an incomplete part is refined by designing the corresponding replacement, it is desirable to check only the modified part and do not perform the whole verification process from scratch. This approach may distribute the verification effort more uniformly over development and enable also run-time verification, as required by adaptive systems, where certain functionalities only become available while the system is running. In this case, it necessary to check if the functionalities possess certain properties before linking them to the running system. This thesis aims to provide techniques that support the analysis of incomplete models designed in the software development. First, it proposes Incomplete Büchi Automata (IBAs) a novel modeling formalism that natively supports incompleteness as in the case of top-down development. IBAs extend the well known Büchi automata (BAs) with unspecified states, called black box states, which encapsulate unspecified functionalities. Black box states can be (recursively) refined into other (Incomplete) Büchi automata. In order to analyze IBAs, we propose an automata-based model checking technique to verify if an IBA M satisfies a property ϕ, written in Linear Temporal Logic (LTL). Due to the presence of black box states, the model checking procedure is modified to produce three different values: yes, if the model of the system satisfies its property; no (plus a counterexample), if it does not; unknown, when the property is possibly satisfied, i.e., its satisfaction depends on the replacements, still to be designed, associated to the black box states. Whenever the property is possibly satisfied, a constraint synthesis procedure, which is presented in this thesis, allows the computation of a constraint for the unspecified parts. A constraint concerns a set of sub-properties that must eventually be satisfied by the automata fragments (replacements) that will replace the black box states in the refinement process. The developer may use these sub-properties as guidelines in the replacement design. Finally, the thesis presents a replacement checking procedure able to verify a replacement against the previously generated constraint. In this way, at each development step, only the new increment is considered in the verification activity. The approach presented in this thesis has been implemented in the CHIA (CHecker for Incompete Automata) framework. CHIA is a prototype tool which supports the designer in the system development and its verification and it has been used to evaluate the approach over two practical examples. The first is a classical computer science example and concerns the well known mutual exclusion system. The second concerns the evolution of a Pick and Place Unit (PPU). The PPU example is used to compare tools that analyze the evolution of automation systems. It is a limited size example, but it provides a valuable trade-off between complexity and evaluation effort. Finally, to analyze the scalability of the approach, in absence of a realistic benchmark suite, the thesis considers a set of random models with increasing size. The evaluation compares the difference in terms of time and space between checking the replacement against the previously generated constraint (the corresponding sub-property) and the effort required to verify the refined model (the original model in which the new component is injected) against the original property.

Il processo di sviluppo del software è costituito da un insieme di scelte progettuali medianti le quali il modello iniziale del sistema viene iterativamente modificato fino ad ottenere l'implementazione finale. Ad ogni raffinamento lo sviluppatore può lasciare parti del sistema non specificati. In questi casi la specifica viene definita incompleta. L'incompletezza sorge quando il raffinamento di alcune funzionalità viene posticipato ad una successiva fase dello sviluppo, o quando i componenti vengono sviluppati da terze parti. Il modello finale del sistema viene ottenuto mediante una sequenza di raffinamenti successivi attraverso i quali le funzionalità identificate vengono iterativamente raffinate in sottomoduli, ed infine rimpiazzate dal corrispettivo codice eseguibile. Durante questo processo varie funzionalità vengono analizzate e confrontate per valutare le loro proprietà. A volte alcune funzionalità possono anche essere aggiunte a run-time, come nel caso dei sistemi adattativi. Le tecniche di verifica formale sviluppate negli ultimi anni consentono di verificare se il sistema sviluppato possiede un insieme di proprietà definite dallo sviluppatore. La verifica formale è utilizzata in pratica in vari domini applicativi e viene utilizzata in diversi contesti industriali. Tuttavia, la verifica formale, ed in particolare le tecniche di model checking, non sono completamente integrate nei processi di sviluppo software correntemente utilizzati. Le tecniche di model checking, dato un modello del sistema e una proprietà di interesse, analizzano esaustivamente tale modello per garantire che tutte le sue esecuzioni soddisfino la proprietà. Se la proprietà non è soddisfatta viene generato un contro esempio. Nelle tecniche di model checking convenzionali il modello del sistema e le proprietà di interesse sono completamente specificate al momento dell'esecuzione della procedura di verifica. Tuttavia, questa assunzione non è sempre valida, infatti, come discusso in precedenza, i modelli considerati sono spesso incompleti. Per consentire una verifica continua durante il processo di sviluppo del software è necessario fornire delle tecniche capaci di supportare dei modelli incompleti. La verifica di modelli incompleti permette di considerare descrizioni di alto livello del sistema, e di rilevare in anticipo eventuali errori. Inoltre, quando le parti incomplete vengono raffinate e rimpiazzate dai rispettivi componenti, è auspicabile la verifica della sola parte modificata, in modo da evitare l'esecuzione della procedura di verifica sull'intero modello. Questo approccio consente di distribuire la verifica in maniera più uniforme nel corso del processo di sviluppo software, riducendo significativamente i tempi di verifica e supportando la verifica a run-time. Nella verifica a run-time, richiesta per esempio nel contesto dei sistemi adattativi, è necessario verificare le proprietà delle funzionalità rilevate prima di inserirle nel sistema in esecuzione. Questa tesi si pone come obbiettivo di fornire tecniche e strumenti atti a supportare specifiche incomplete nel processo di sviluppo software. La tesi propone un formalismo che supporta nativamente l'incompletezza chiamato Incomplete Büchi Automata (IBAs). Gli IBAs estendono i Büchi Automata (BAs) con degli stati non specificati, chiamati black box che incapsulano funzionalità ancora da definire. I black box possono essere ricorsivamente raffinati in altri (Incomplete) Büchi automata. Al fine di analizzare gli IBAs proponiamo una tecnica di verifica basata su automi che consente di verificare se un IBA M soddisfi una proprietà ϕ, specificata in Linear Temporal Logic (LTL). A causa della presenza degli stati black box, la procedura produce tre differenti valori, ``si" se la proprietà è soddisfatta dal modello, ``no" (e un contro esempio) se non è soddisfatta, ``forse" se la validità della proprietà dipende nel raffinamento degli stati black box. In questo ultimo caso, viene proposta una tecnica di sintesi capace di computare un vincolo per le parti del modello non specificate. Il vincolo è un insieme di sottoproprietà che devono essere soddisfatte dagli automi che rimpiazzeranno gli stati black box nel processo di raffinamento. Tali automi vengono chiamati replacements. Le sottoproprietà possono essere utilizzate per guidare lo sviluppatore nel processo di raffinamento. Infine, questa tesi propone una tecnica di verifica capace di considerare il raffinamento associato a un black box in riferimento al corrispondente vincolo. Questa procedura evita la verifica del modello originale ogni volta che un raffinamento è proposto, rendendo l'analisi del modello incrementale. L'approccio presentato in questa tesi è stato implementato nel framework CHIA (CHecker for Incompete Automata). CHIA è un tool in versione prototipale che supporta il progettista nello sviluppo del software e nella sua verifica. Il tool è stato utilizzato per valutare l'approccio su due esempi pratici. Il primo è un esempio classico nel campo dell'informatica e riguarda un sistema di mutua esclusione. Il secondo si riferisce all'evoluzione di un sistema di spostamento pezzi-``Pick and Place Unit"-all'interno di una catena di montaggio. Infine, per valutare la scalabilità dell'approccio, sono stati considerati un insieme di modelli randomici di dimensione crescente. È stata analizzata la differenza di prestazioni, in termini di tempo e spazio, tra la verifica del replacement associato a un black box in riferimento al vincolo corrispondente e la verifica del raffinamento (il modello originale nel quale il replacement del black box viene inserito) in riferimento alla proprietà originale. Infine, per valutare la scalabilità dell'approccio, sono stati considerati un insieme di modelli randomici di dimensione crescente. È stata analizzata la differenza di prestazioni, in termini di tempo e spazio, tra la verifica del replacement associato a un black box in riferimento al vincolo corrispondente e la verifica del raffinamento (il modello originale nel quale il replacement del black box viene inserito) in riferimento alla proprietà originale.