Email Gateway (Aug 19 2022 at 10:16): Email Gateway (Aug 19 2022 at 10:16):From: Stephan Merz <Stephan.Merz@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@irit.fr or Stephan.Merz@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.
Last updated: May 06 2024 at 16:21 UTC