The public defense of Nesredin Mahmud's doctoral thesis in Computer Science and Engineering

Doctoral thesis and Licentiate seminars

Datum: 2019-06-13
Tid: 13.15
Plats: room Gamma, MDH Västerås.

The public defense of Nesredin Mahmud's doctoral thesis in Computer Science and Engineering will take place at Mälardalen University, room Gamma, MDH Västerås, at 13.15 on June 13, 2019.

Title: “Design of Assured and Efficient Safety-critical Systems”.

Serial number: 291

The faculty examiner is Professor Joost-Pieter Katoen, RWTH Aachen University, and the examining committee consists of Professor Peter Csaba Ölveczky, University of Oslo, Professor Wolfgang Ahrendt, Chalmers University of Technology, associate Professor Raffaela Mirandola, Politecnico di Milano.

Reserve; Professor Björn Lisper, Mälardalen University


Safety-critical systems need to be analyzed rigorously to remove software/specifications errors, that is, their requirements specifications should be unambiguous, comprehensible and consistent, and the software design should conform to the specifications, hence avoiding undesirable system failures. 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 and incomprehensible. Besides natural language, template-based requirements specification methods are used frequently to specify requirements (esp. in safety-critical applications). Although, the latter reduce ambiguity and improve the comprehensibility of the specifications, they are usually rigid due to the constrained syntax of the templates, and template selection is challenging. Industrial systems are frequently developed by using modeling and simulation environments such as Simulink, which is 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. Analyzing the timing behavior of safety-critical software that is refined by multi-rate periodic tasks with data age constraints across the end-to-end software functionality is not trivial. This is due to the undersampling and oversampling effects caused by the data propagation from higher to lower rates and vice versa, respectively. Furthermore, when such systems are deployed on a distributed architecture, e.g., electrical/electronic vehicular system, besides assuring the timeliness, the reliability of the distributed software should be maximized to counter the higher risk of failures in the distributed computing setting, hence improving the overall predictability of the safety-critical system. However, designing for reliability usually requires additional critical system resources such as power and energy. Hence, to accommodate the growing complexity of software functionality, the design of the safety-critical systems should consider the efficient use of critical system resources such as the power source, while meeting the timing and reliability requirements.

To address the above needs, in this thesis, we propose formal-methods-based approaches and optimization techniques to assure improved quality of requirements specifications and software designs, and to efficiently map software functionality to hardware. The contributions of the thesis are: (i) ReSA - a domain-specific requirements specification language tailored to embedded systems, based on constrained natural language; (ii) a formal approach to check consistency of ReSA  specifications via Boolean satisfiability problem (SAT) and ontology; (iii) a framework based on statistical model checking to analyze Simulink models via automated transformation into networks of stochastic timed automata; and (iv) a resource-efficient allocation of fault-tolerant software with end-to-end timing and reliability constraints via integer linear programming and hybrid particle-swarm optimization. Our proposed solutions are validated and evaluated on automotive use cases such as the Adjustable Speed Limiter (ASL) and the Brake-by-Wire (BBW) systems from Volvo Group Trucks Technology (VGTT), and on an Engine Management (EM) system benchmark from Bosch.