[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
The positions may be of interest to readers of this list who have a background
in interactive theorem proving and in verification of real-world programming
languages.
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 [email protected] or [email protected].
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.
