Integrating formal methods with industrial standards in the development of flexible manufacturing systems

This thesis presents a complete, innovative, formal verification approach to model certain class of manufacturing systems, the Flexible Manufacturing Systems (FMS). The thesis is the final product of a collaboration project between a group of automatic control engineers of the "Istituto di Tecnologie Industriali ed Automazione" (ITIA) of the CNR of Milano and a group of informatics engineers of the "Dipartimento di Elettronica, Informazione e Bioingegneria" (DEIB) of the Politecnico di Milano. A complete, integrated Model-Driven environment is the final target of the project; this environment should support the designer from the modelling phase to the formal verification, to obtain an agile, flexible development process. To overcome the difficulties in the use of formal languages, the approach is based on widely-used, graphical but semi-formal high level modelling languages. The most part of these languages have Model-driven environments to help system designers in the development process and have simple and familiar notations, but lack of a rigorous semantics. We chose one of the typical languages adopted in such environments supporting the development of FMS, namely Stateflow, and we encoded it in terms of formulae of the metric temporal logic TRIO; by this way we provided a rigorous, compositional, run-to-completion semantics for Stateflow, based on concepts of micro- and macro-steps. The formal model and the axiomatization of the semantics allow the formal verification of a set of real-time qualitative or quantitative user-defined properties, using a fully automatic model checker, Zot, which has been developed internally by the group of the DEIB. The approach is general enough to allow the use of different modelling languages, logical formalisms or model checking tools. The approach is illustrated and validated through a realistic case study. In the evolution of the work, a new metric temporal logic, X-TRIO, has been developed as an extension to TRIO, to overcome the limitations of the time model of TRIO. In effect, many formal semantics of high level graphical languages, such as the one of Stateflow, adopt the abstraction of "zero- time transitions", which does not consume time. These however have several drawbacks in terms of naturalness and logic consistency, as a system may be modelled to be in different states at the same time. X-TRIO exploits concepts from non-standard analysis to model micro and macro-steps. In the thesis, the expressiveness and decidability properties of the new metric temporal logic have been studied and analysed. Also, a plugin for Zot is presented to allow the use of the new logical formalism.

Questa tesi presenta un completo ed innovativo approccio alla verifica formale e alla modellazione di una ben specifica classe di sistemi di produzione, i sistemi manifatturieri flessibili o Flexible Manufacturing Systems (FMS). La tesi è il prodotto finale di un progetto di collaborazione tra un gruppo di ingegneri automatici del controllo dell’ "Istituto di Tecnologie Industriali Ed Automazione" (ITIA) del CNR di Milano e un gruppo di ingegneri informatici del "Dipartimento di Elettronica, Informazione e Bioingegneria" (DEIB) del Politecnico di Milano. L’obiettivo finale del progetto è un ambiente completamente integrato di modellazione, basato su un approccio orientato al modello; questo ambiente dovrebbe supportare il progettista dalla fase di modellazione a quella della verifica formale, per ottenere un processo di sviluppo agile e flessibile . Per superare le difficoltà nell’utilizzo dei linguaggi formali, l’approccio è basato su linguaggi ampiamente diffusi di modellazione di alto livello, possibilemnte grafici, ma purtroppo soltanto semi-formali. La maggior parte di questi linguaggi hanno sia ambienti integrati adatti ad aiutare i progettisti di sistemi nel processo di sviluppo, sia notazioni semplici e familiari, ma mancano di una semantica rigorosa. Per questa tesi, abbiamo scelto uno dei linguaggi più usati per la modellazione di FMS, Stateflow, e lo abbiamo codificato usando formule della logica metrica temporale TRIO; per ottenere ciò, abbiamo sviluppato una semantica per Stateflow rigorosa e composizionale, di tipo run-to-completion, basata sul concetto di micro- e macro- steps . Il modello e la rigorosa formalizzazione della semantica permettono la verifica formale di un insieme di proprietà in tempo reale, sia qualitative che quantitative, definite dall’utente, utilizzando un bounded model checker, Zot, che è stato sviluppato internamente dal gruppo del DEIB. L’approccio è sufficientemente generale da consentire l’uso di diversi linguaggi di modellazione, formalismi logici o strumenti di model checking. L’approccio è illustrato e validato attraverso un caso di studio realistico. In una successiva evoluzione del lavoro, una nuova logica metrica temporale, X-TRIO, è stata sviluppata come estensione di TRIO, per superare i limiti del suo approccio temporale. Infatti, molte semantiche formali per linguaggi grafici di modellazione ad alto livello, come ad esempio quella di Stateflow, adottano l’astrazione delle "transizioni a tempo zero", che non consumano tempo reale. Queste però presentano alcuni inconvenienti in termini di naturalezza e coerenza logica, in quanto un sistema può essere modellato in modo da essere in diversi stati nello stesso istante temporale. X-TRIO sfrutta i concetti dell’Analisi Non-Standard per modellare micro e macro-steps. Nella tesi, sono state studiate e analizzate le proprietà di espressività e decidibilità della nuova logica temporale metrica. Inoltre, è stato sviluppato un plugin per Zot per consentire l’utilizzo pratico del nuovo formalismo logico.