Modular Automated Verificationof Flexible Manufacturing Systems with MetricTemporal Logic and Non-Standard Analysis

Industrial systems are made of interacting components, which evolve at very different speeds. This is often dealt with in notations used in the industrial practice, such as Stateflow, through the notion of “zero-time transitions”. These have several drawbacks, especially when building complex models from basic components, whose coordination is complicated by the fact that each element is modeled to be in different states at the same time. We exploit a temporal logic formalism based on non-standard analysis to provide a natural formal semantics to the composition of modules described as Stateflow diagrams. The semantics has been implemented in a fully automated formal verification tool, which we apply to the formal verification of an example of robotic cell.