liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • 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
Model-Based Verification of Dynamic System Behavior against Requirements: Method, Language, and Tool
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
2013 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Modeling and simulation of complex systems is at the heart of any modern engineering activity. Engineers strive to predict the behavior of the system under development in order to get answers to particular questions long before physical prototypes or the actual system are built and can be tested in real life.

An important question is whether a particular system design fulfills or violates requirements that are imposed on the system under development. When developing complex systems, such as spacecraft, aircraft, cars, power plants, or any subsystem of such a system, this question becomes hard to answer simply because the systems are too complex for engineers to be able to create mental models of them. Nowadays it is common to use computer-supported modeling languages to describe complex physical and cyber-physical systems. The situation is different when it comes to describing requirements. Requirements are typically written in natural language. Unfortunately, natural languages fail at being unambiguous, in terms of both syntax and semantics. Automated processing of naturallanguage requirements is a challenging task which still is too difficult to accomplish via computer for this approach to be of significant use in requirements engineering or verification.

This dissertation proposes a new approach to design verification using simulation models that include formalized requirements. The main contributions are a new method that is supported by a new language and tool, along with case studies. The method enables verification of system dynamic behavior designs against requirements using simulation models. In particular, it shows how natural-language requirements and scenarios are formalized. Moreover, it presents a framework for automating the composition of simulation models that are used for design verification, evaluation of verification results, and sharing of new knowledge inferred in verification sessions.

A new language called ModelicaML was developed to support the new method. It enables requirement formalization and integrates UML and Modelica. The language and the developed algorithms for automation are implemented in a prototype that is based on Eclipse Papyrus UML, Acceleo, and Xtext for modeling, and OpenModelica tools for simulation. The prototype is used to illustrate the applicability of the new method to examples from industry. The case studies presented start with sets of natural-language requirements and show how they are translated into models. Then, designs and verification scenarios are modeled, and simulation models are composed and simulated automatically. The simulation results produced are then used to draw conclusions on requirement violations; this knowledge is shared using semantic web technology.

This approach supports the development and dynamic verification of cyber-physical systems, including both hardware and software components. ModelicaML facilitates a holistic view of the system by enabling engineers to model and verify multi-domain system behavior using mathematical models and state-of-the-art simulation capabilities. Using this approach, requirement inconsistencies, incorrectness, or infeasibilities, as well as design errors, can be detected and avoided early on in system development. The artifacts created can be reused for product verification in later development stages.

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 2013. , 235 p.
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1547
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:liu:diva-98107DOI: 10.3384/diss.diva-98107ISBN: 978-91-7519-505-6 (print)OAI: oai:DiVA.org:liu-98107DiVA: diva2:654890
Public defence
2013-11-12, Visionen, hus B, Campus Valla, Linköpings universitet, Linköping, 10:15 (English)
Opponent
Supervisors
Funder
Vinnova
Available from: 2013-10-09 Created: 2013-09-30 Last updated: 2014-10-08Bibliographically approved

Open Access in DiVA

Model-Based Verification of Dynamic System Behavior against Requirements: Method, Language, and Tool(8644 kB)3119 downloads
File information
File name FULLTEXT01.pdfFile size 8644 kBChecksum SHA-512
f6c6685c7eee8754e03efb3c39d3fe35e8c06312d27d51b2c99a842be38231e27e255ae4d939532f5f09a8a917dfa65ed43a70b87969f14aec5c6b90c9ed6444
Type fulltextMimetype application/pdf
omslag(2728 kB)50 downloads
File information
File name COVER01.pdfFile size 2728 kBChecksum SHA-512
af1fe8d5176ede7cfe8de956259a7d39a12246e487912812b14ae0f67ce4b8b1a30393f53e301757932bc3c2faf601780caa2fb2752dc69e4672ebda0afb87a8
Type coverMimetype application/pdf

Other links

Publisher's full text
By organisation
Department of Computer and Information ScienceThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 3119 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • 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