Semi-Automated Formalization and Verification of Automotive Requirements using Simulink Design Verifier

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.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