Change search
CiteExportLink to record
Permanent link

Direct link
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Wind Turbine System: An Industrial Case Study in Formal Modeling and Verification
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Formal Modelling and Analysis of Embedded Systems))
ABB Corporate Research, Norway.ORCID iD: 0000-0001-6954-8339
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded systems))ORCID iD: 0000-0003-2870-2680
ABB Corporate Research, Norway. (IS (Embedded systems))ORCID iD: 0000-0003-1996-1234
Show others and affiliations
2014 (English)In: Communications in Computer and Information Science, Volume 419 CCIS, 2014, 229-245 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.
Keyword [en]
Formal Modeling, Case Study
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Computer Science
URN: urn:nbn:se:mdh:diva-22326DOI: 10.1007/978-3-319-05416-2_15Scopus ID: 2-s2.0-84904627849ISBN: 9783319054155 (print)OAI: diva2:661160
2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013; Queenstown; New Zealand; 29 October 2013 through 30 October 2013
Available from: 2013-11-01 Created: 2013-11-01 Last updated: 2015-02-05Bibliographically approved
In thesis
1. Model Based Development of Embedded Systems using Logical Clock Constraints and Timed Automata
Open this publication in new window or tab >>Model Based Development of Embedded Systems using Logical Clock Constraints and Timed Automata
2013 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

In modern times, human life is intrinsically depending on real-time embedded systems (RTES) with increasingly safety-critical and mission-critical features, for instance, in domains such as automotive and avionics. These systems are characterized by stringent functional requirements and require predictable timing behavior. However, the complexity of RTES has been ever increasing requiring systematic development methods. To address these concerns, model-based frameworks and component-based design methodologies have emerged as a feasible solution. Further, system artifacts such as requirements/specifications, architectural designs as well as behavioral models like statemachine views are integrated within the development process. However, several challenges remain to be addressed, out of which two are especially important: expressiveness, to represent the real-time and causality behavior, and analyzability, to support verification of functional and timing behavior.

As the main research contribution, this thesis presents design and verification techniques for model-based development of RTES, addressing expressiveness and analyzability for architectural and behavioral models. To begin with, we have proposed a systematic design process to support component-based development. Next, we have provided a real-time semantic basis, in order to support expressiveness and verification for structural and behavioral models. This is achieved by defining an intuitive formal semantics for real-time component models, using ProCom, a component model developed at our research centre, and also using the CCSL (Clock Constraint Specification Language), an expressive language for specification of timed causality behavior. This paves the way for formal verification of both architectural and behavioral models, using model checking, as we show in this work, by transforming the models into timed automata and performing verification using UPPAAL, a model checking tool based on timed automata. Finally, the research contributions are validated using representative examples of RTES as well as an industrial case-study.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2013
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 146
Embedded Systems, Model-based development, Model-Checking, Architectural Modeling, CCSL, Timed Automata
National Category
Embedded Systems
urn:nbn:se:mdh:diva-22328 (URN)978-91-7485-123-6 (ISBN)
Public defence
2013-12-09, Kappa, Mälardalen University, Västerås, 13:15 (English)
Swedish Research Council, 2270 430 16243
Available from: 2013-11-01 Created: 2013-11-01 Last updated: 2013-11-18Bibliographically approved

Open Access in DiVA

FTSCS2013(616 kB)