A formal approach for reactive mode handling

The purpose of this study is the formal verification and validation of a model used for the reconfiguration process of a production system. This process is ensured by a function within the control framework named mode handling. For the needs of reactivity of this function, a synchronous approach using the formal specification formalism safe state machine (SSM) is adopted. We explain firstly what the required properties are, the methods used to check them are presented, and then we propose the specifications in SSM, which guarantee their verification and their validation. This study is mainly concerned with safety properties ensuring mode coherence.