The public defense of Predrag Filipovikj's doctoral thesis in Computer Science and Engineering
Doctoral thesis and Licentiate seminars
The public defense of Predrag Filipovikj’s doctoral thesis in Computer Science and Engineering will take place at Mälardalen University, room Gamma (Västerås Campus) at 13.30 on June 17, 2019.
Title: “Automated Approaches for Formal Verification of Embedded System Artifacts”.
Serial number: 292
The faculty examiner is Professor Jim Woodcock, University of York, and the examining committee consists of Professor Kim Larsen, Aalborg University, Associate Professor Luigia Petre, Åbo Akademi University, Associate Professor Christian Berger, Chalmers University of Technology
Reserve; Professor Marjan Sirjani, Mälardalen University.
Using embedded software to perform highly complex functions has been enabled by the ever-increasing computational power and memory capacity of the embedded hardware. In the automotive industry, the embedded software has sparked the "-by-wire" trend, which focuses at replacing the traditional mechanical vehicular functions with software ones. Consequently, the software has become the major driver of innovation and an area where competitive edge is gained.
The vehicular embedded software has become so large and complex that creating and assuring the correctness of the related artifacts, including the system specifications and the design-time models, has become difficult to manage with the state-of-the-practice human-intensive techniques. One problem stems from the high number and intricacy of system requirements specifications (system specifications) that combine functional and possibly timing or other types of constraints, which makes them difficult for analysis in order to prevent propagation of specification and design errors into the production code. The predominant way of producing software is by using the model-based paradigm using Simulink as the de facto standard tool. Simulink models are thus important embedded software artifacts from which code can be generated, so their correctness needs to be ensured. A potential way to address such problems is to apply computer-aided and mathematically rigorous specification, analysis and verification techniques already at the requirements specification stage, but also further at later development stages. Despite the high degree of automation, exhaustiveness and rigor of the formal analysis and verification techniques, their integration with industrial practice remains a challenge.
To tackle the above-mentioned challenges, in this thesis, we propose a set of approaches for the formal specification and analysis of system requirements, as well as verification of design-time behavioral models of embedded software developed in Simulink. Our contributions are on several fronts, as follows. First, we assess the expressiveness of an existing pattern-based technique for the formal system specification on an operational industrial system. Based on the positive findings, we deem the technique expressive enough to capture the common systems' requirements in a systematic way and complement it with a tool, called PROPAS. The tool aims to enable practitioners to formally specify their systems. Next, we provide a consistency analysis approach applicable on the system specifications encoded as a set of temporal formulas. The proposed approach is fully automated and implemented in the PROPAS tool. It is suitable for the early phases of system development for debugging the specification. Our next two contributions concern the formal verification and analysis of Simulink models. To achieve this, we propose two formal approaches, one based on statistical model checking and the other on bounded model checking, which are tailored to deal with the size and complexity of industrial Simulink models. Both of the approaches are accompanied with an adequate tool support, namely SIMPPAAL and SYMC, respectively. For validation, all of the proposed approaches are applied on industrial systems provided by our industrial partners Scania and Volvo Group Trucks Technology.