[SMT-LIB] PHD thesis proposal

[Rémi Delmas]

PhD Thesis proposal.

"Formal verification of interactive applications embedded in 
new-generation cockpits."

* Subject

Over the last 30 years, the aeronautics industry has promoted sound
and rigorous formal methods for specifying, developing and formally
verifying safety critical, high assurance software, such as flight
control systems, engine control systems, fuel management systems,
etc. Over the same period, the software driving the interface between
the pilot and the system has not benefited from the enriched
methodologies and accompanying formal techniques. However, most of
these interactive interface software have grown in size and their will
certainly, if not already, become prevalent in current and future
generations cockpits, with the introduction of touchscreens,
etc. These software-driven interfaces will take over traditional
hardware interface elements such as buttons, switches, rotary
encoders, status lights, ... and will inherit their high assurance
requirements.

(For instance, the BEA report (see note 1) on the Rio-Paris AF-447
crash indicates a malfunction of the flight director: right before the
accident, the flight director indicated the pilot to increase the
incidence of the aircraft whereas the aircraft was already
stalled. These indications should never have been shown to the pilot
considering the current physical state of the aircraft.)

The issue is that the design methods, specification and implementation
languages and V&V processes designed for systems such as flight
control systems are not well suited for systems with strong graphical
content and human interaction. Current design, development and V&V
processes for interactive systems are rather primitive, where software
is usually coded "from scratch" without prior specification, or by
cut&paste reuse of older software itself lacking explicit formal
requirements, and validation is mainly carried out through extensive
testing without any reference formal requirement to compare test
outcomes against.

In an attempt to overcome these issue, DTIM, in a previous project and
PhD thesis, elaborated a language LIDL (LIDL stands for LIDL is an
Interaction Definition Language, see note 2). This
language is rooted in the family of synchronous reactive data flow
languages, provides the notion of Interactor which operates over input
flows to produce output flows, the language also offers constructs to
specify compositions of interactors to achieve elaborate interactive
applications. A code generator for LIDL has also been developed, which
is able to translate a LIDL specification into lower-level code
forming the core of an interactive application, compatible with the
ARINC661 norm applicable for cockpit applications.

The goal of the proposed PhD thesis is to design and implement a
collection of processes, techniques and tools allowing to perform the
formal verification of critical properties (mostly safety and bounded
liveness properties) of LIDL specifications. The operational semantics
of LIDL is already available and constitutes a sound foundation for
building formal verification methods based on formal transition
systems, using methods such as bounded model checking, k-induction,
IC3/PDR, predicate abstraction, etc. Such techniques could be used to
establish critical properties of specifications, as well as to
generate tests that would in turn be used to validate the actual
implementation running on the target hardware.

- Note 1: 
http://www.bea.aero/fr/enquetes/vol.af.447/rapport.final.fr.php - pages 
194-197
- Note 2: 
https://www.researchgate.net/publication/281627447_The_LIDL_Interaction_Description_Language

* Funding

The PhD thesis is co-funded by ONERA and the Région Midi-Pyrennées.

* Applicant profile

   - MSc in computer science, interest and background in:
     - language and compiler design,
     - formal logic (first order logic, temporal logics, etc)
     - formal semantics and model theory
     - Boolean Satisfiability and Satisfiability Modulo Theories.
   - Speaking English is a must if French is not possible.
   - Experience with functional programming languages (OCAML, Scala) is
     a plus but is not necessary.

* Location

The work will be conducted in Toulouse, France, in the Department of
Information Processing and Modelling of ONERA (the French National
Office of Aerospace Research), under the supervision of:

Advisor: Bruno D'Ausbourg
- Tel: +33 5 62 25 26 48
- email: Bruno.d.Ausbourg at onera.fr

Co-Advisor: Rémi Delmas
- tel: +33 5 62 25 26 54
- email: Remi.Delmas at onera.fr

Collaboration with external academic or industrial entities:
- IRIT (https://www.irit.fr/?lang=en)
- LORIA (http://www.loria.fr/en/loria/)
- IRT Saint-Exupéry (http://www.irt-saintexupery.com/)


* Application and Contact information

Applicants can send their resumes, motivation letters, grade records and
recommendation letters to the Advisor's email address given above.



-- 
Rémi Delmas
Research engineer, DTIM, ONERA Midi-Pyréennées.
Tél: +33562252654