Change search
ReferencesLink to record
Permanent link

Direct link
Verification of Requirements in Simulink Design Verifier and UPPAAL - an Industrial Case Study
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics. (Inbyggda kontrollsystem)
MDH.
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.
2016 (English)Report (Other academic)
Abstract [en]

Model checking has reached a state of maturity that allows its adoption for the verification of complex embedded systems, such as the ones found in vehicles. Little research has been carried out in order to determine how model checking can be integrated with the current design and verification practices at the industry. In this case study we take a real control subsystem of a Scania vehicle, specified as a Simulink model, and use two popular model checker (Simulink Design Verifier and Uppaal) for verifying its functional requirements according to the design specification. Our goal is to understand the real challenges faced by engineers performing model checking, and also to assess the possibilities and limitations of the available tools. The main difficulties encountered relate to the fact that most of the work still has to be performed manually, and depends significantly on the skills of the user. In particular, much effort has to be spent in formalizing the system requirements and in model-to-model transformation. This work shows that better tool support is required for these activities before model checking can be ready for widespread use in current development processes.

Place, publisher, year, edition, pages
KTH Royal Institute of Technology, 2016. , 2 p.
National Category
Mechanical Engineering Mathematical Analysis
Research subject
Machine Design
Identifiers
URN: urn:nbn:se:kth:diva-191110OAI: oai:DiVA.org:kth-191110DiVA: diva2:954829
Projects
ESPRESSO/VeriSpec
Note

QC 20160907

Available from: 2016-08-23 Created: 2016-08-23 Last updated: 2016-09-07Bibliographically approved

Open Access in DiVA

fulltext(179 kB)10 downloads
File information
File name FULLTEXT01.pdfFile size 179 kBChecksum SHA-512
816e5bff94ae3244f0f60d2e357ed2c0a7d59d35dbe4adc4e301870b75ba8808fc71dbc652174235b48f7ec49ba7af7e7203ab7ed79238b04273471b06d78458
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Westman, Jonas
By organisation
Mechatronics
Mechanical EngineeringMathematical Analysis

Search outside of DiVA

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

Total: 18 hits
ReferencesLink to record
Permanent link

Direct link