The Coq mailing list

[Stephan Merz <Stephan.Merz AT loria.fr>]

Project
"Computer-assisted checking of schedulability and resource access of 
concurrent Java using timed automata"

funded by Fondation EADS

We seek two post-doctoral researchers in computer science who have experience 
in at least one of the following areas:

        • Formal verification using model checking and/or SMT solving
        • Timed automata
        • Interactive theorem proving
        • Concurrent Java programming

The first position will be at Université Paul Sabatier Toulouse (IRIT) and 
lasts 24 months. The second position will be at INRIA Nancy and lasts 12 
months (possibly extensible).

The positions will be remunerated according to French salary scale for 
post-doctoral researchers at approximately 2600 euros monthly.

The project holders are Jan-Georg Smaus 
(http://www.irit.fr/~Jan-Georg.Smaus/) at IRIT and Stephan Merz 
(http://www.loria.fr/~merz/) at INRIA. Informal inquiries should be sent to 
smaus AT irit.fr
 or 
Stephan.Merz AT loria.fr.

The working language of the project is English.

Female candidates are particularly encouraged to apply.


Information on the project:

In safety critical systems, concurrent programs are becoming more widespread, 
even though their correctness is particularly difficult to ascertain. In 
particular, system failures due to timing problems are hard to detect with 
traditional quality assurance methods like tests. Untimely or badly 
synchronized access to resources may lead to data corruption, with 
catastrophic consequences.

This project aims at investigating analysis and verification techniques for 
concurrent programs in a real-time setting, and at relating program analyses 
and proof methods in a demonstrably sound way. We address a major problem of 
concurrent programming, namely the access to shared resources by several 
program threads. Uncoordinated access may lead, among others, to data 
inconsistencies and loss of updates, and is therefore not acceptable. The 
standard solution is to use critical regions, access monitors or locks to 
prevent two threads from modifying the same resource at the same time. 
Unfortunately, this solution has major drawbacks: deadlocks may stall the 
entire program, unfair strategies may permanently exclude single threads from 
executing, and the execution times of threads may be difficult to predict, 
which is fatal for a hard real-time system.

Programming frameworks for real-time systems propose instead to grant access 
to a resource based on temporal coordination, and not as a consequence of 
locking. Thus, each thread of a set of concurrent threads is equipped with a 
specification of when it intends to access a given set of resources. In this 
project, we will more specifically work with Safety Critical Java (SCJ), a 
real-time dialect of the Java programming language targeted at 
safety-critical systems. We intend to verify that the temporal annotations 
(minimal and maximal execution times and scheduling dates) in an SCJ program 
ensure that no two threads can simultaneously access a resource. The basic 
idea is to map timing information to timed automata and apply real-time model 
checking in order to prove the absence of errors. More fine-grained analysis 
will require the use of advanced program analysis in order to construct an 
appropriate timed automaton.

As a methodological contribution, we are also interested in providing a 
formal model (in the proof assistant Isabelle) of Safety Critical Java and of 
timed automata and in proving the correctness of the TA abstraction of SCJ 
programs.