Title :
Building effective formal models to prove time properties of networked automation systems
Author :
Ruel, Silvain ; De Smet, Olivier ; Faure, Jean-Marc
Author_Institution :
LURPA, ENS Cachan, Cachan
Abstract :
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.
Keywords :
local area networks; combinatory explosion; communicating timed automata; effective formal models; networked automation systems; time properties; worst-case models; Automata; Automatic control; Automation; Chemical industry; Communication system control; Ethernet networks; Explosions; Power system modeling; Programmable control; Protocols;
Conference_Titel :
Discrete Event Systems, 2008. WODES 2008. 9th International Workshop on
Conference_Location :
Goteborg
Print_ISBN :
978-1-4244-2592-1
Electronic_ISBN :
978-1-4244-2593-8
DOI :
10.1109/WODES.2008.4605968