NOVALTIS

NOVel ALgorithms and VALidation Techniques for TIme-critical
and high Integrity Systems

Keywords: Distributed algorithms, distributed systems, fault-tolerance, redundancy & failure management, concurrency control, system-level specifications, system-level validation & proof obligations, requirement capture, proof-based system engineering, autonomous systems, embedded systems, mobile systems, space systems.

Topic: Com

Scientific Leader:

Gérard Le Lann, Research Director, INRIA

Research Scientists:

Jean-François Hermant, IE INRIA

Bernadette Charron-Bost, Researcher, LIX, CNRS

Assistant:

Stéphanie Aubin, INRIA

Scientific areas:

• (A1) System-level algorithms, specifications and proofs: Research on computational/system models and distributed algorithms for critical computing systems where combined safety, liveness, timeliness & dependability properties must be predicted
• (A2) System-level engineering methods: Research on proof-based system engineering (PBSE) methods directed at critical and/or complex computer-based applications and systems
• (A3) Analyses of causes of mishaps or failures: Diagnoses of real causes of difficulties experienced with projects (time/budget overruns, cancellations) and with deployed critical systems (failures or quasi-failures)

Major application domains (2005):

Defense (all forces), Aerospace (deep space exploration, earth orbiting vehicles, autonomous systems).

Established partnership with academia (2005):

• Vienna University of Technology, Austria
• Ecole Polytechnique Fédérale de Lausanne (EPFL), Switzerland
• Virginia Tech, USA

• DGA (French MoD)
• Members of the European Integrated Project ASSERT (Automated Proof-Based System & Software Engineering for Real-Time Systems, 2004-2007): ESA (European Space Agency), EADS-ST, Dassault Aviation, EADS-Astrium, Alcatel Space, Alenia, Axlog Ingénierie, CS
• Safran
• MITRE Corp., USA

NOVALTIS builds upon project REFLECS. New challenges are:

(A1) Models and Algorithms

• Safety and liveness: To explore most extreme asynchronous computational/system models, to specify and prove distributed algorithms in such models aimed at solving agreement problems in distributed fault-tolerant computing, while circumventing impossibility results (research on the Theta-model)
• Timeliness and asynchrony: To examine how to use purely asynchronous (time-free) algorithms or partially synchronous algorithms for solving problems in distributed real-time computing, where strict timeliness properties must be proven to hold (research on the design immersion principle)
• Timeliness and overloads: To investigate scheduling problems (algorithms, schedulability analyses, feasibility conditions) that arise with timeliness/scheduling attributes more complex than constant deadlines, assuming overloads are normal conditions (research on time utility function (TUF)-driven schedulers)
• Composed safety, liveness, timeliness and dependability: To devise, specify, and prove algorithms directed at endowing a distributed computing system with a specific combination of safety, liveness, timeliness, and dependability properties (research drawing from multiple disciplines, such as, e.g., Concurrency Control, Serializability theory, Distributed Algorithms, Scheduling theory)

• To address issues arising with the early phases in a project lifecycle (application requirement capture, system design and forward validation), for systems bound to meet specified properties very high coverage
• To investigate how to maintain a continuous chain of proofs, from application requirement capture to implementation of a validated system-solution
• To introduce system-level proof obligations in system engineering methods used for real projects, notably proofs of combined safety, liveness, dependability, and timeliness properties
• To blend together scientific rigor (proof obligations) and reality (proof assumptions, design assumptions, must be shown to be provably correctly implemented – not discarded as being “engineering/implementation details”)
• To contribute to the development of PBSE tools

• To examine documented cases of mishaps, quasi-failures or failures experienced with projects (before system deployment) and with deployed critical systems
• To identify causes of difficulties, with a special focus on system engineering faults
• Contributions to the safety-critical forum (moderated by York University, UK).