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 »

Objectives:

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:

• To detect and/or prevent the errors related to parallelism and concurrency,

• To estimate the performance of various architectural solutions in order to contribute to the guiding of the design process towards the optimal solution.

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:

• Analysis of the execution and communication models

• Contribution to the definition of design patterns for expressing the parallelism and the concurrency. These patterns will rely on the mechanisms proposed by the standard parallelization APIs (MT-API, OpenMP, etc.).

• Formal specification of the properties related to parallelism and concurrency

• Formal modeling and verification of the design patterns

• Application of these patterns to one or several case studies

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:

• Writing of project deliverables

• Publications and/or presentations in the conferences of the domain

• Sharing of knowledge

Required skills and profile:

• Education: PhD in computer science on one of the subjects covered by the activity (model checking, performance modeling, concurrent architectures, etc.)

• Knowledge of formal modeling for verification (specification of properties, description of behaviour)

• Knowledge of verification techniques by model checking

• Knowledge of performance modeling (probabilistic modeling, stochastic modeling, etc.)

• Knowledge of concurrent architectures, languages and/or parallel programming APIs (OpenMP, MTAPI, etc.)

• Usage of tools for specification and model checking (CADP, Tina, Romeo, Uppaal, etc.)

• Interest in the concrete implementation of technologies, software development and experimenting

• Fluent in English, French is a plus

• Proven communication and interpersonal relationships skills, attention to detail, methodical approach, curiosity, autonomy, team player

Contacts:

If you are interested in this offer, please send your application file to recrutement@irt-saintexupery.com with the reference 17PD-SE-CAPH-01.

Application content:

• Letter of application

• Curriculum vitæ including the list of publications

• References or letters of recommendation, if any