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

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