Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Semi-Automated Formalization and Verification of Automotive Requirements using Simulink Design Verifier
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.).
2015 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

The complexity of embedded software in the automotive domain is ever-increasing due to increase in the no. of features aimed at providing more advanced solutions. This has greatly favored the incorporation of Model Based Design workflow in the software development lifecycle to handle complexities in different development phases. Simulation based testing is widely used in automotive domain to identify design errors in models. However, formal verification as opposed to simulation based testing has an inherent advantage of traversing the entire design space systematically and proving mathematically that the system satisfies the requirements. Lack of knowledge in formal methods and system requirements in their present form in natural text, form the biggest hindrances in making formal verification a reality in the automotive domain. Specification Patterns through their constrained English grammar have shown some promise in requirements specification by avoiding the diverse language structure of the natural language. Simulink Design Verifier (SLDV), a verification tool integrated with MATLAB/Simulink alleviates the need of a separate formal model and leverages on Simulink’s capability to model requirements. This thesis investigates various challenges with regard to formal verification with Simulink Design Verifier and Specification Patterns with possibilities of semi-automating the process. Fuel Level Display System, a case study from Scania is specifically dealt with as a real industry example, to investigate the expressivity of Simulink Design Verifier for modelling requirements, its efficiency as a verification tool, usability of Specification Patterns and insufficiencies of requirements in natural text. The investigation recommends formal verification to be carried out by system engineers/developers with help of Specification Patterns and SLDV, provided that complex behavior is specified within a proposition/non-literal term of Pattern. This complex behavior can be modelled with Simulink and SLDV blocks. The modelling framework of patterns in SLDV can be used to verify the requirements. The limitations posed by SLDV in modelling some aspects of requirements can be dealt with by making suitable changes to system model by system developers.

Abstract [sv]

Komplexiteten för de inbyggda system som utnyttjas inom fordonsindustrin är alltjämt ökande då behovet av alltmer avancerade lösningar kräver fler funktioner. Detta har vart till stor fördel vid införandet av Model Based Design i arbetsflödet för mjukvaruutvecklingen vilket gett medel för att hantera komplexitet vid olika faser i utvecklingen. Simulation based testing är vidsträckt använt inom fordonsindustrin för att identifiera designfel i modellerna, dock har formal verification i motsats till Simulation based testing en nedärvd fördel att kunna granska hela designen systematiskt och matematiskt bevisa att systemet uppfyller kraven. De största hindren för att kunna utnyttja formal verification till fullo inom fordonsindustrin idag är brist på kunskap inom formella metoder samt systemkrav i naturlig textform. Specification Patterns i begränsad grammatisk engelska har visat vissa lovande resultat inom kravspecifikation genom att undvika den stora mångfalden i språkstrukturen i det naturliga språket. Simulink Design Verifier (SLDV) är ett verifikationsverktyg integrerat i MATLAB/Simulink som minskar behovet av en separat formell modell samt begränsningarna i Simulink’s kapacitet att modellera krav. Detta examensarbete undersöker olika utmaningar angående formal verification med Simulink Design Verifier och Specification Patterns för möjligheten att göra processen semi-automatiserad. Fuel Level Display System, en fallstudie vid Scania är specifikt framtagen som ett reellt industriellt exempel för att undersöka möjligheten att utnyttja Simulink Design Verifier för modell krav, dess effektivitet som verifikationsverktyg, användningsmöjligheter för Specification Patterns samt bristerna för kraven i naturlig text. Undersökningen rekommenderar att formal verification ska genomföras av system-ingenjörer/utvecklare genom Specification Patterns och SLDV, förutsatt att komplext beteende är specificerad inom en proposition/icke-bokstavlig form av Pattern. Detta komplexa beteende kan modelleras med hjälp av Simulink och SLDV block. Verifikation av krav är möjligt genom modellstrukturen i SLDV. De begränsningar som tillkommer genom användning av SLDV för att modellera vissa aspekter av kraven kan åtgärdas genom lämpliga förändringar i systemmodellen, detta utförs av systemutvecklare.

Place, publisher, year, edition, pages
2015. , 73 p.
Series
MMK 2015:71 MES 012
National Category
Mechanical Engineering
Identifiers
URN: urn:nbn:se:kth:diva-182644OAI: oai:DiVA.org:kth-182644DiVA: diva2:905250
External cooperation
Scania
Supervisors
Examiners
Available from: 2016-03-07 Created: 2016-02-22 Last updated: 2016-03-07Bibliographically approved

Open Access in DiVA

fulltext(3240 kB)431 downloads
File information
File name FULLTEXT01.pdfFile size 3240 kBChecksum SHA-512
f50301bca28f4ef658d6769fa8ff502e1b05aebed9106af56961594986a344c968583458cc2ebbd3850f835527051add5a31bf35d30254c29ea2e122028fa1c4
Type fulltextMimetype application/pdf

By organisation
Machine Design (Dept.)
Mechanical Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 431 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: 882 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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