Ontology-based Analysis and Scalable Model Checking of Embedded Systems Models

Currently, there is a lack of effective and scalable methods to specify and analyze requirements, and formally analyze the behavioral models of embedded systems. Most embedded systems requirements are expressed in natural language, which is flexible and intuitive but frequently ambiguous, vague and incomprehensive. Besides natural language, template-based requirements specification methods are used to specify requirements (esp. in safety-critical applications), which reduce ambiguity and improve the comprehensibility of the specifications. However, the template-based methods are usually rigid due to the fixed structures of the templates. They also lack meta-models for extensibility, and template selection is challenging. In this thesis, we propose a domain specific language for embedded systems, ReSA, which is a constrained natural language but flexible enough to allow engineers to use different constructs to specify requirements. The language has formal semantics in propositional logic, and also in description logic, which enables non-trivial and rigorous analysis of requirements specifications, e.g., consistency checking, completeness of specifications, etc. We show how to carry out consistency checking of requirements formalized in boolean logic, but also at deeper semantic levels, within the ReSA ontology. Moreover, we propose a method for the scalable formal analysis of Simulink models, as Simulink is the de facto modeling and simulation environment of embedded systems in industry. Simulink models are also used to generate code automatically for various hardware platforms. Therefore, it is essential to be able to formally analyze Simulink models, to get insight into the behavior of the embedded system, and also prevent potential errors from propagating into the implementation. We validate our approaches on industrial use cases from the automotive industry, that is, the Adjustable Speed Limiter (ASL) and the Brake-By-Wire (BBW) systems from Volvo Group Trucks Technology, Sweden.