Digitala Vetenskapliga Arkivet

Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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
Applying Model Checking for Verifying the Functional Requirements of a Scania’s Vehicle Control System
Mälardalen University, School of Innovation, Design and Engineering.
Mälardalen University, School of Innovation, Design and Engineering.
2012 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Model-based development is one of the most significant areas in recent research and development activities in the field of automotive industry. As the field of software engineering is evolving, model based development is gaining more and more importance in academia and industry. Therefore, it is desirable to have techniques that are able to identify anomalies in system models during the analysis and design phase instead of identifying them in development phase where it is difficult to detect them and a lot of time, effort and resources are required to fix them. Model checking is a formal verification technique that facilitates the identification of defects in system models during early stages of system development. There are a lot of tools in academia and industry that provide the automated support for model checking. 

In this master thesis a vehicle control system of Scania the Fuel Level Display System is modeled in two different model checking tools; Simulink Design Verifier and UPPAAL. The requirements that are to be satisfied by the system model are verified by both tools. After verifying the requirements against the system model and checking the model against general design errors, it is established that the model checking can be effectively used for detecting the design errors in early development phases and can help developing better systems. Both the tools are analyzed depending upon the features supported. Moreover, relevance of model checking is studied with respect to ISO 26262 standard.

Place, publisher, year, edition, pages
2012. , p. 77
Keywords [en]
Model checking, Verification, Functional Requirements, Scania, Vehicle Control System, Fuel Level Display system, Simulink Design Verifier, UPPAAL, ISO 26262.
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-15447OAI: oai:DiVA.org:mdh-15447DiVA, id: diva2:558435
External cooperation
Scania
Presentation
2012-09-07, Kappa, Mälardalens högskola, Mälardalen University, Västerås, 08:15 (English)
Uppsok
Technology
Supervisors
Examiners
Available from: 2012-10-04 Created: 2012-10-03 Last updated: 2012-10-04Bibliographically approved

Open Access in DiVA

Applying Model Checking for Verifying the Functional Requirements of a Scania's Vehicle Control System(3023 kB)1452 downloads
File information
File name FULLTEXT01.pdfFile size 3023 kBChecksum SHA-512
17fc9157aa16f2d2c779a58f4b6a110bd4ec2440f4108381c9ca0d9af7f2db65e7b21a429885f2c1906c54893d1fd0364e6ea6c0d4d421b172ee02c2012cf575
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Sulyman, MuhammadAli, Shahid
By organisation
School of Innovation, Design and Engineering
Computer Systems

Search outside of DiVA

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

urn-nbn

Altmetric score

urn-nbn
Total: 719 hits
CiteExportLink to record
Permanent link

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