PhD in Computer Science

Location: Inria Sophia Antipolis, Kairos team

Laboratory:

Duration: 3 years

Context

In the ANR Project #TAPAS, we consider safety-critical systems that have strong interactions with humans and physical components in the domains of electric/autonomous vehicles (EV/AV), (smart) transportation systems (train, tramway), avionics, and healthcare. Such systems must be trustworthy and therefore require sound and formal design frameworks that come with tools for validation and verification. These systems usually exhibits heterogeneous intertwined requirements both functional and non-functional like safety, security, performance, where time plays a key role. These systems usually rely on embedded equipment that are reactive and deterministic, leaving nondeterminism outside their scope of interest. #TAPAS ultimate objective is to define a sound methodology for the design of trustworthy cyber-physical systems (CPS) from requirements to code deployment, supported by an open-source modeling, validation and verification framework. This shall be achieved by plugging into a formal generic language (Event-B) some efficient analysis tools (Provers, Model-checkers, Simulation). We focus on functional and time requirements that are the ground requirements on which systems are built. Indeed, most other considered non functional requirements (safety, security, energy) directly depend on time, more precisely on heterogeneous models of time, including discrete and continuous time.

Objectives

The objective of this PhD is to define an heterogeneous model of time based on the tagged signal model [3] into the Event-B methodology [2]. This should consist in defining hooks (called Logical clocks [1]) for both probing and control into an Event-B machine in such a way that several models of time (synchronous, event-triggered, discrete-event, continuous-time) can be used jointly as part of the Event-B models.

To demonstrate the usefulness of the approach, we shall use several case-studies and produce an open-source demonstrator based on Rodin platform [4] using Rodin’s component plugin [5]. Once the clocks are injected within the Event-B model, we expect to be able to run ad-hoc verification techniques that shall largely depends on the actual model of time in use. Such verification techniques and tools can range from assistant provers, model-checkers (symbolic, stochastic) to heterogeneous simulation tools (like Ptolemy [6]), TESL [7], ModHel’X [8], GeMoC [9].

Required skills

  • Master degree in Computer Science, formal methods, embedded systems, or a related field.
  • Background in the use of formal methods.
  • Open mindedness about the use of different languages and frameworks, proficiency in at least one classical programming languages (e.g., Java, Typescript, C++).
  • Familiarity with classical development practices, including unit testing and CI/CD (Continuous Integration/Continuous Deployment).
  • Strong ability to adapt to dynamic research environments and solve complex technical challenges.

Working Environment

Application

Interested candidates are invited to submit their CV along with a cover letter detailing their relevant experience and interest in the position to Frédéric Mallet (first.last at univ-cotedazur.fr). CNRS is an equal opportunities employer. All applications will be considered on merit and the applicant’s ability to meet the requirements of the role.

References

  1. Lamport, Leslie (1978). Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7), 558–565. doi: 10.1145/359545.359563.
  2. Abrial, Jean-Raymond (2010). Modeling in Event-B: System and Software Engineering. Cambridge University Press. url
  3. Lee, E.A. and Sangiovanni-Vincentelli, A. (1998). A framework for comparing models of computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 17(12), 1217–1229. doi: 10.1109/43.736561.
  4. Abrial, Jean-Raymond et al. (2010). Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf., 12(6), 447–466. url
  5. Aït-Ameur, Yamine et al. (2022). Empowering the Event-B Method Using External Theories. In: Integrated Formal Methods, Springer International Publishing, pp. 18–35. url
  6. Eker, J. et al. (2003). Taming heterogeneity - the Ptolemy approach. Proceedings of the IEEE, 91(1), 127–144. doi: 10.1109/JPROC.2002.805829.
  7. Boulanger, Frédéric et al. (2014 10). TESL: A language for reconciling heterogeneous execution traces. In: 12th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 114 - 123. doi: 10.1109/MEMCOD.2014.6961849.
  8. Hardebolle, Cécile and Boulanger, Frédéric (2008). ModHel'X: A Component-Oriented Approach to Multi-Formalism Modeling. In: Models in Software Engineering, Springer Berlin Heidelberg, pp. 247–258. url
  9. Combemale, Benoit et al. (2013). Reifying Concurrency for Executable Metamodeling. In: Lecture Notes in Computer Science, Springer, pp. 365-384. doi: 10.1007/978-3-319-02654-1_20.