IRT Saint-Exupéry and the CONVECS team of Inria and LIG
are recruiting a post-doc fellowship
Start date: September 1st, 2017
Type of contract: Fixed term contract (CDD) for 18 months.
Location: This post-doctoral fellowship will be carried out at the IRT Saint-Exupéry located in Toulouse, France.
Subject: « Evaluation and formal verification of concurrent architectures »
The Institute for Technological Research IRT Saint-Exupéry is a world-class excellence center in Aeronautics, Space and Embedded Systems. It aims at enforcing the competitiveness of research and industry of the Midi Pyrénées and Aquitaine regions in the areas of aeronautics, space, and embedded systems. With a funding of 50% from the public sector and 50% from the private sector, the IRT gathers the large industrial companies of the region acting in the aforementioned areas, as well as public institutions and their laboratories, to join forces on three strategic technological domains: multifunctional high-performance materials, more electrical aircrafts, and embedded systems.
The CAPHCA project (Critical Applications on Predictable High-Performance Computing Architectures) carried on at IRT Saint Exupéry aims at defining and building a process and its associated tool chain making possible the safe exploitation of modern multi-core hardware architectures / coprocessors, whilst maintaining a high performance level. CAPHCA gathers several industrial companies from the avionics and automotive domains, providers of simulation technologies for hardware platforms, and research laboratories working on formal methods, languages, and analysis of real-time systems. For its research and development activities, the IRT is seeking a research engineer (post-doctorate level) who will work within the CAPHCA project.
The work will be carried out at IRT Saint Exupéry located in Toulouse, and will be co-supervised by the CONVECS project-team team of Inria and LIG. CONVECS is involved in several research directions: providing formal specification languages for describing asynchronous concurrent systems; enhancing temporal logics and verification tools; fighting state explosion; designing generic components for verification, test, and performance evaluation; and demonstrating the applicability of its methods and tools on real-life applications with academic and industrial partnership. The members of CONVECS have been developing for about 20 years the CADP verification toolbox dedicated to the design, analysis, and verification of asynchronous systems consisting of concurrent processes interacting via message passing. Within CAPHCA, CONVECS will bring its support and its scientific and technical expertise on the usage of formal methods and tools.
Work proposed and expected results:
In this context, the research engineer will be in charge of defining and building the methodological and technical means allowing:
The application domain is that of critical avionics and automotive applications deployed on recent multi-core execution platforms (PowerPC, ARM, AURIX, etc.).
These activities will be guided by the case studies developed in the CAPHCA project (typical applications from the avionics and automotive domains). The results will be evaluated on a subset of these case studies.
The solutions will rely on the application of models and verification techniques stemming, if possible, from the software and/or hardware design modeling frameworks (AADL, HOOD, UML, etc.). The research engineer will contribute to the selection of the design formalism(s) in order to facilitate this transition. The formal model will exploit the languages and tools of the CADP toolbox developed at Inria Grenoble.
The methodology will be applied and validated on all (or a part of) the case studies defined in the project.
The activities of the research engineer will be organized in two phases of approximately 9 months each.
Phase 1: Exploitation for the detection of concurrency errors
The objective of this phase is to propose a tool-supported methodology enabling to detect certains classes of errors on the basis of the design model. Two approaches will be studied, and possibly combined: (i) an approach based on the definition of interaction patterns, the formal verification of these patterns, and their exploitation for devising an application, and (ii) an approach based on the direct verification of the architectural model of the application. The architectural description formalisms will be defined during the project. The choice will be guided in particular by the verification capabilities. The AADL formalism of SAE is a possible candidate. For the families of applications considered in the project, the following activities will be carried out:
Phase 2: Exploitation of formalisms and model checking tools for performance estimation
The objective of this phase is to exploit some of the notations, tools, and possibly formal models used initially for verification (namely, during the first phase of the work) to the purpose of performance evaluation.
The activities will consider first purely functional models (e.g., for searching the sequence of interactions leading to the worst execution time, worst bus load, etc.), and then probabilistic and stochastic models. The work will exploit existing results regarding various modeling formalisms, such as the LNT language and IMCs (Interactive Markov Chains), as well as more classical models, such as DTMCs (Discrete-Time Markov Chains) extended with data.
Regarding the annotation of models with quantitative data, all available sources of information will be exploited, such as the measures obtained on the simulator or on the target architecture. This modelling and evaluation methodology is sought to be integrated in an archituectural exploration and optimization process.
Besides these specific activities, the research engineer will contribute to the achievement of the common objectives of the team:
Required skills and profile:
If you are interested in this offer, please send your application file to email@example.com with the reference 17PD-SE-CAPH-01.