Wind Turbine System: An Industrial Case Study in Formal Modeling and Verification
2014 (English)In: Communications in Computer and Information Science, Volume 419 CCIS, 2014, 229-245 p.Conference paper (Refereed)
In the development of embedded systems, the formal analysis of system artifacts, such as structural and behavioral models, helps the system engineers to understand the overall functional and timing behavior of the system. In this case study paper, we present our experience in applying formal verification and validation (V&V) techniques, we had earlier proposed, for an industrial wind turbine system (WTS). We demonstrate the complementary benefits of formal verification in the context of existing V&V practices largely based on simulation and testing. We also discuss some modeling trade-offs and challenges we have identified with the case-study, which are worth being emphasized. One issue is related, for instance, to the expressiveness of the system artifacts, in view of the known limitations of rigorous verification, e.g. model-checking, of industrial systems.
Place, publisher, year, edition, pages
2014. 229-245 p.
Formal Modeling, Case Study
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject Computer Science
IdentifiersURN: urn:nbn:se:mdh:diva-22326DOI: 10.1007/978-3-319-05416-2_15ScopusID: 2-s2.0-84904627849ISBN: 9783319054155OAI: oai:DiVA.org:mdh-22326DiVA: diva2:661160
2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013; Queenstown; New Zealand; 29 October 2013 through 30 October 2013