Analyzing a wind turbine system: From simulation to formal verificationShow others and affiliations
2017 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 133, p. 216-242Article in journal (Refereed) Published
Abstract [en]
Many industrial systems are hybrid by nature, most often being made of a discrete controller that senses and regulates the execution of a plant characterized by continuous dynamics. Examples of such systems include wind turbines that convert wind energy into electrical energy. Designing industrial control systems is challenging, due to the mixed nature of requirements (functional, timing, etc.) as well as due to the complexity stemming from the interaction of the controller with the plant. Model-based techniques help in tackling the design challenges, whereas methods such as simulation with tools like MATLAB/Simulink can be employed for analysis. Although practical, these methods alone cannot ensure full predictability, due to the fact that they cannot guarantee system properties for all possible executions of the system model. In order to ensure that the system will behave as expected under any operational circumstance, formal verification and validation procedures need to be added to the actual development process. In this paper, we propose an extension of the iFEST (industrial Framework for Embedded Systems Tools) process and platform for embedded systems design with model-based testing using MaTeLo, and model checking time-dependent requirements with the UPPAAL tool, as means of increasing the confidence in the system's behavior. To show the feasibility of the techniques on industrially-sized systems, we analyze a wind turbine industrial prototype model against functional and timing requirements. We capture the execution semantics of the plant and controller components of the wind turbine via logical clocks and constraints expressed in the clock constraint specification language (CCSL) of UML MARTE, after which we construct real-time models amenable to model checking, by mapping the timed behavior (expressed in CCSL) of the real-time components of the wind turbine, onto timed automata. Our work is a first application on an industrial wind turbine system of complementary methods for formal analysis, that is, model-based testing, and model checking a mathematically tractable system abstraction based on data obtained by simulating the system with MATLAB/Simulink. We also discuss relevant modeling and verification challenges encountered during our experiences with the wind turbine system.
Place, publisher, year, edition, pages
2017. Vol. 133, p. 216-242
Keywords [en]
MaTeLo, Model checking, Model-based testing, UPPAAL, Wind turbine system, Clocks, Controllers, Embedded software, Embedded systems, Formal verification, MATLAB, Semantics, Specification languages, Wind power, Wind turbines, Industrial control systems, Model based techniques, Model based testing, Modeling and verifications, Verification-and-validation, Wind turbine systems
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:mdh:diva-34042DOI: 10.1016/j.scico.2016.09.007ISI: 000390072300007Scopus ID: 2-s2.0-84997417525OAI: oai:DiVA.org:mdh-34042DiVA, id: diva2:1053222
2016-12-082016-12-082020-11-06Bibliographically approved