Formal proofs for the analysis of real-time systems in Coq

Abstract

Real-time systems are systems that must satisfy timing requirements such as response time bounds (i.e., bounds on the maximum time a task may take to complete its execution). There exists by now a large body of research on analysis methods for such systems. However, the underlying proofs for all these analyses are too often informal or difficult to understand, check, adapt and reuse. Given that safety assurance requirements are constantly evolving, this lack of certification is likely to become a major issue with substantial implications in the embedded systems industry.

It is our belief that a strong formal basis for the analysis of real-time systems is needed. The goal of the thesis is to contribute to a formal framework for the analysis of real-time systems using the Coq proof assistant. A first objective is to certify well-established response-time analyses so as to better understand the role played by standard assumptions. This will allow for new results to emerge by lifting unnecessary assumptions. A second objective is to formally prove recent research results such as those related to Typical Worst-Case Analysis [1]. Particular care will be taken to ensure a modular structure of the proof framework, relying on concepts such as critical instant and busy window which are usually defined in a specific context (e.g. for a specific scheduler). Another promising research direction is the use of Coq to formally bridge the gap between existing analysis techniques, e.g. between Real-Time Calculus [1] and Compositional Performance Analysis [2]. The proofs developed in the thesis will be integrated into Prosa [2], see http://prosa.mpi-sws.org/.

Keywords: certified proofs, real-time systems, schedulability, Coq proof assistant, response-time analysis

Starting date: September 2016 (a later date can be discussed)

Context

The thesis will take place in the INRIA SPADES team, in Grenoble, France in collaboration with Verimag (http://www-verimag.imag.fr). The PhD thesis will be funded by PERSYVAL-Lab (https://persyval-lab.org) as part of a project-team involving three research labs of the Grenoble area. In addition, the PhD candidate will benefit from active collaborations with the Max-Planck Institute (mpi-sws.org) and Onera (onera.fr).

Requirements

A strong background in formal methods is expected and knowledge in embedded systems technology would be a plus. Good written and oral communication skills in English are required (French is not necessary).

Candidates are invited to send their application via email to Sophie Quinton (sophie.quinton@inria.fr), Pascal Fradet (pascal.fradet@inria.fr) and Jean-François Monin (jean-francois.monin@imag.fr). Please include a CV, a motivation letter and contact information for 2 referees.

Bibliography

[1] Wenbo Xu, Zain Alabedin Haj Hammadeh, Alexander Kröller, Rolf Ernst, and Sophie Quinton. Improved Deadline Miss Models for Real-Time Systems Using Typical Worst-Case Analysis. In Euromicro Conference on Real-Time Systems (ECRTS), 2015.

[2] Felipe Cerqueira, Felix Stutz, and Björn Brandenburg. Prosa: A Case for Readable Mechanized Schedulability Analysis. In Euromicro Conference on Real-Time Systems (ECRTS), to appear, 2016.

[3] Samarjit Chakraborty, Simon Künzli, and Lothar Thiele. A general framework for analysing system properties in platform-based embedded system designs. In Design, Automation and Test in Europe Conference and Exposition (DATE), 2003.

[4] Rafik Henia, Arne Hamann, Marek Jersak, Razvan Racu, Kai Richter, and Rolf Ernst. System level performance analysis – the SymTA/S approach. In IEE Proceedings Computers and Digital Techniques, 2005.