Quantity and intricacy of features implemented in vehicle have expanded rapidly over a past few years. Currently vision of autonomous vehicle is no longer a dream or SF movie, but instead a coming reality. In order to reach the better quality and high safety, advanced verification techniques are required. Simulink Design Verifier is a model checking tool based on formal verification, which can be effectively used to solve problems concerning error detection and testing at earlier stages of project. The transformation of requirements written in traditional form into Simulink Design Verifier objectives can be time consuming as well as requiring knowledge of system model and the verification tools. In order to reduce time consumption and to guide a user through the system model and the verification tool, the semi-automated framework has been developed. An implementation of restricted English grammar patterns into Simulink objects supports description of patterns to engineers and reduces time consumption. The developed framework is flexible and intuitive hence can be a solution for other branches of industry, but further tests and verification would be required. This thesis highlights the whole process of transformation system requirements written in natural language into Simulink Design Verifier objectives. The Fuel Level Display System model currently used by almost all Scania’s vehicles is analysed. Limitations and errors encountered during development process like a flexibility of Simulink Design Verifier to capture requirements and the patterns behaviour or ambiguity of system requirements are analysed and described in this thesis.

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.

Automated Test Generation (ATG) has been successfully applied in many domains. For the modeling and simulation language Simulink, there has been research on developing tools for ATG with promising results. However, most tools developed as part of academic research and are not publicly available, or severely limited in their ability to be integrated into an industrial workflow. There are commercial ATG tools for Simulink, with Simulink Design Verifier (SLDV) as the de-facto standard tool. For this thesis, we perform an empirical comparison of manual tests to those generated by SLDV. For the comparison, we used 180 components from the propulsion control software developed by our industry partner. All except two components are compatible for test generation to some extent. The majority of components are partially compatible, requiring block replacement or stubbing. Approximation of floating-point numbers is the primary reason for block replacement, which can be performed automatically by SLDV. Two components were incompatible, and 14 required full stubbing of blocks. Using a pre-processing step, the generated tests achieve similar coverage as the manual tests. We performed a Mann–Whitney U test with the hypothesis that the generated tests achieve higher coverage than the manual tests. There are no statistically significant differences for either decision coverage (0.0719), or condition coverage (0.8357). However, for Modified Condition/Decision Coverage, the generated tests achieve higher coverage, and the difference is significant (0.0027). The limitations of ATG were explored by looking at the cases where the generated tests achieved lower coverage than the manual test. We found that the use of floating-point arithmetic and temporal logic increases the time required for test generation, and causes the analysis to hit the time limit. The test generation does not support all custom S-functions and perform stubbing of these blocks. This made the tool unable to reason about persistent storage. Configuration constants have limited support, which was the reason for the coverage difference in three cases. We have concluded that while much effort is required for custom tooling and initial setup, ATG can prove useful for early fault detection in an industrial workflow. ATG would prove especially useful in an automated continuous integration workflow for integration-level conformance testing.