摘要：AbstractSupremicais a tool for the modelling and analysis of discrete-event control functions based on state machine models of the uncontrolled plant and specification of the desired closed-loop behaviour. The modelling framework inSupremicais based on finite-state machines extended with variables, guard conditions, and action functions. In order to handle large-scale problems of industrially interesting size,Supremicauses advanced model checking techniques such as symbolic representations and compositional abstraction.Supremicahas been used in several industrial research projects to verify and synthesise control functions for embedded controllers, industrial robots, and flexible manufacturing systems, and to verify program code for autonomous vehicles. This paper gives an overview of the modelling features ofSupremica, shows the verification and synthesis facilities and their performance for large problems, and presents some of the industrial applications whereSupremicahas been used.
