The de sign of safe industrial controllers is one of the most important domains related with Automation Systems research. For this purpose, there are used some important synthesis and analysis techniques. Among the analysis techniques two of the most important are Simulation and Formal Verification. In this paper these two techniques are used together in a complementary way. For the successful application of these mentioned techniques the plant modelling is crucial, so the understanding and modelling of the plant behaviour is essential for obtaining safe industrial systems controllers. A two step approach is presented: first, the use of Simulation and, second, the use of Formal Verification of Industrial Systems Specifications. The specification and plant models used for each technique are described. Simulation and Formal Verification results are presented and discussed. The approach presented in the paper makes it possible to deal with real industrial systems, and obtain safe controllers for hybrid plants. Modelica modelling language and Dymola simulation environment is used for Simulation purposes and Timed Automata formalism and UPPAAL real-time model-checker are used for Formal Verification purposes.
@article{MachadoSCSL:2011,
author = {J. Machado and E. Seabra and J.C. Campos and F. Soares and C. Lećo},
title = {Safe Controllers Design for Industrial Automation Systems},
journal = {Computers & Industrial Engineering},
note = {ISSN: 0360-8352},
abstract = {The de sign of safe industrial controllers is one of the most important domains related with Automation Systems research. For this purpose, there are used some important synthesis and analysis techniques. Among the analysis techniques two of the most important are Simulation and Formal Verification. In this paper these two techniques are used together in a complementary way. For the successful application of these mentioned techniques the plant modelling is crucial, so the understanding and modelling of the plant behaviour is essential for obtaining safe industrial systems controllers. A two step approach is presented: first, the use of Simulation and, second, the use of Formal Verification of Industrial Systems Specifications. The specification and plant models used for each technique are described. Simulation and Formal Verification results are presented and discussed. The approach presented in the paper makes it possible to deal with real industrial systems, and obtain safe controllers for hybrid plants. Modelica modelling language and Dymola simulation environment is used for Simulation purposes and Timed Automata formalism and UPPAAL real-time model-checker are used for Formal Verification purposes.},
pages = {635-653},
volume = {60},
number = {4},
month = {May},
year = {2011},
hdl = {1822/14887},
doi = {10.1016/j.cie.2010.12.020}
}Generated by mkBiblio 2.6.26