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

Direct link
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.
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1547
National Category
Engineering and Technology
URN: urn:nbn:se:liu:diva-98107DOI: 10.3384/diss.diva-98107ISBN: 978-91-7519-505-6OAI: diva2:654890
Public defence
2013-11-12, Visionen, hus B, Campus Valla, Linköpings universitet, Linköping, 10:15 (English)
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)1105 downloads
File information
File name FULLTEXT01.pdfFile size 8644 kBChecksum SHA-512
Type fulltextMimetype application/pdf
omslag(2728 kB)25 downloads
File information
File name COVER01.pdfFile size 2728 kBChecksum SHA-512
Type coverMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Schamai, Wladimir
By organisation
Department of Computer and Information ScienceThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 1105 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

Altmetric score

Total: 650 hits
ReferencesLink to record
Permanent link

Direct link