|Thesis abstract: |
This thesis presents a complete, innovative, formal veri?cation approach to model certain class of manufacturing systems, the Flexible Manufacturing Systems (FMS). The thesis is the ?nal 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 ?nal target of the project; this environment should support the designer from the modelling phase to the formal veri?cation, to obtain an agile, ?exible development process. To overcome the dif?culties 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 State?ow, 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 State?ow, based on concepts of micro- and macro-steps. The formal model and the axiomatization of the semantics allow the formal veri?cation of a set of real-time qualitative or quantitative user-de?ned 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 State?ow, 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.