2020-03007 - Software engineer for a timed model checker

Contract type : Fixed-term contract

Level of qualifications required : Graduate degree or equivalent

Other valued qualifications : Engineer degree

Fonction : Temporary scientific engineer

Level of experience : Recently graduated

Context

Main goal: significantly enhance the IMITATOR software input syntax.

IMITATOR (www.imitator.fr)  is a state-of-the-art software for formal verification of parametric timed models, with applications in the verification of real-time systems, as well as cybersecurity properties.

IMITATOR relies on the parametric timed automata formalism (an extension of finite-state automata), with some ad-hoc extensions such as shared rational variables. The goal is to significantly improve the set of types accepted by the tool, so as to allow a small programming language, including Booleans, integers, lists, arrays, user-defined functions, etc. A second direction will consist in allowing models parameterized by the number of components (e.g. a server with an arbitrary number of clients).

A more complete description of the subject is available at:

www.loria.science/andre/temp/subject-engineer-IMITATOR.pdf

Assignment

Missions:
Under the supervision of Étienne André (full professor at LORIA) and in collaboration with the SED (development and experimentation service) of LORIA and, from time to time, with Jaime Arias (engineer with LIPN, Université Sorbonne Paris Nord), the hired person's main task will be to improve the IMITATOR input syntax. This consists in developing new types, and update consequently the core verification engine of IMITATOR.

For more information on the research topic:

IMITATOR is a parametric timed model checker. It takes as input models expressed using parametric timed automata, a formalism extending finite-state automata. The hired person will not need deep knowledge in this domain. Nevertheless, for information, links to the research domain are given below:

The hired person may developed an expertise in formal verification, a state-of-the-art domain with exciting perspectives in both the academic and industrial domains.

Responsibilities:
The hired person will be in charge of developing the IMITATOR syntax.

Management:

The hired person may have the responsibility to interact with IMITATOR users, including from the industry.

Main activities

Main activities:

  • software engineering
  • OCaml development
  • documentation

Other activities:

  • writing reports
  • using and comparing other model checking software

 

Examples of activities:

  • Analyze the designers and users' needs
  • Interactions with the industrial and academic users of IMITATOR
  • Prioritize and sort requests
  • Propose an incremental development for the syntactic improvement
  • Write documentation
  • Test, modify, and validate
  • Write reports
  • Make presentations to the VeriDis team and other colleagues

Skills

Skills requested:

  • an engineer degree in computer science
  • appreciated programming languages: OCaml, Python
  • Linux OS environment

Languages:

  • English: be able to read and write documentation

Appreciated additional skills

  • formal methods
  • model checking

Benefits package

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage

Remuneration

Rémunération :  à partir de 2562 € brut mensuel selon diplôme et expérience.