Building effective formal models to prove time properties of networked automation systems

This paper proposes a method to build formal models of networked automation systems, in the form of sets of communicating timed automata, which are reduced enough to avoid (or limit) combinatory explosion, but accurate enough to provide meaningful proof results, when they are checked. This method starts from a detailed initial model, which includes all behaviours of all components of the system, and comprises two steps. First, given a property to prove, the structure of the model is simplified so as to keep only the components models which impact directly this proof. Then the formal models of the remaining components are modified to take the previous simplification into account; the resulting models are worst-case models which guarantee trustworthy results. Experiments show the effectiveness of this modeling.