https://www.mdu.se/

mdu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Analyzing a wind turbine system: From simulation to formal verification
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
ABB Corporate Research, Sweden.
Volvo Construction Equipment, Sweden.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. ABB Corporate Research, Sweden.ORCID iD: 0000-0001-6954-8339
Show 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
Available from: 2016-12-08 Created: 2016-12-08 Last updated: 2020-11-06Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Seceleanu, Cristina CerschiSapienza, GaetanaSeceleanu, TiberiuPettersson, Paul
By organisation
Embedded Systems
In the same journal
Science of Computer Programming
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 140 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf