Department of Computer Science

Ph.D. defence by Andreas Engelbredt Dalsgaard

Andreas Engelbredt Dalsgaard will defend his thesis “Verification of Safety Critical Systems using Program Analysis and Model Checking” Thursday 27th of October 2016, 13:00, in room 0.2.13 at Selma Lagerlöfs Vej 300.

Last modified: 10.10.2016

Andreas Engelbredt Dalsgaard will defend his thesis:

Verification of Safety Critical Systems using Program Analysis and Model Checking 

The defence takes place on Thursday 27th of October 2016, 13:00, in room 0.2.13 at Selma Lagerlöfs Vej 300.
 
Abstract:    

Today embedded computer systems are increasingly an essential part in a wide range of products. That also include products where a failure of the system may injure or even endanger human life, such systems are generally known as safety critical systems. 

Unfortunately, developing software for safety critical systems is time- consuming and costly both due to that embedded systems are becoming increasingly complex and due to costs associated with testing and verification required by certification authorities. 

One source of errors for safety critical software is due to the use of unsafe languages. Two traditionally methods for remedying the use of unsafe languages and verifying the absences of errors in safety critical systems are static program analysis and model checking. For example, static program analysis can identify pointer arithmetic which may potentially lead to failures. Modern languages like Java disallow pointer arithmetic and can avoid such analyses. However,
Java is not designed for safety critical systems which often have real-time requirements. For example, deallocation of dynamically allocated data is problematic as it may interrupt the execution at any time. The Safety-Critical Java (SCJ) specification was designed to enable the use of Java for safety critical systems.

In this thesis aspects of the memory model of SCJ is examined. Unlike traditional Java, the memory model of SCJ is based on scoped memory areas to enable a predictable execution and reclamation of memory. However, the model may be unfamiliar to developers, who may inadvertently introduce dangling references. Additionally, SCJ require developers to annotate
worst-case memory bounds for scoped memory areas. These bounds must be strict upper bounds but should also not waste resources on resource constrained embedded systems. Two analyses for aiding SCJ developers with these issues were developed and implemented using static program analysis. 

In some cases of using these analyses it was found that analysing the entire SCJ software stack in full detail was not practical due to long run-times. The formalism of lattice model checking is
proposed as a way to formulate static program analyses as a model checking problem, potentially enabling an analysis to take advantage of future improvements in model checkers. Parallel timed automata reachability and model checking is studied as a way to speed up model checkers and a prototype toolchain is developed. Finally, distributed timed automata reachability is considered in order to enable verification of larger systems by taking advantage of the collective main memory of multiple machines.


Members of the assessment committee

Professor Brian Vinter, University of Copenhagen,
Denmark, Professor Wang Yi, Uppsala University, Sweden, and Associate Professor Bent
Thomsen, Aalborg University, Denmark. Associate Professor René Rydhof Hansen and Professor
Kim Guldstrand Larsen are supervisors. Moderator Associate Professor Brian Nielsen.

All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.

All news