摘要
We present an effective approach to perform formal verification of properties of interest of production systems whose behavior is modeled through Stateflow diagrams. The approach hinges on a semantics of Stateflow diagrams given in terms of formulae of a metric temporal logic. The semantics has been implemented in a fully automated tool through which users can define a wide range of properties of interest and then check if they hold for the system. We illustrate the approach and the use of the tool through a realistic case study. The verification technique allowed us to uncover a previously undetected error in the design of the system.
- 出版日期2014-10