PhD in Computer Science

Location: Université Sorbonne Paris Nord

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 exhibit 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 provide approaches to verification benefiting from both model checking Parametric Timed Automata [1] (PTA) and the Event-B methodology [2]. This should start by expressing PTAs in Event-B, and in practice encode them as a Rodin plugin [3,4]. Then, base on the refinement capabilities of Event-B to refine the automata locations. Note that a smart separation of concerns between the timed and untimed components will be a key to a successful approach. For refining the timed parts, necessary conditions will have to be determined.

The verification and model checking capabilities associated with both types of models will be investigated, so as to identify properties that can be stated by Rodin/Event-B and benefit the model checking of PTAs with Imitator [5] and vice-versa. For example invariants on variables and parameters could improve handling zones of PTAs [6]. This will lead to an orchestration methodology for the verification of hybrid functional temporal models.

To demonstrate the benefits of the approach, it will be experimented with several case-studies.

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 language.
  • 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 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 Laure Petrucci (first.last at lipn.univ-paris13.fr). University Sorbonne Paris Nord 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] É. André, M. Knapik, D. Lime, W. Penczek, and L. Petrucci, “Parametric Verification: An Introduction”, in Transactions on Petri Nets and Other Models of Concurrency XIV, vol. 11790 of LNCS,pp. 64-100, Springer, 2019. paper

[2] J. Abrial, “Modeling in Event-B - System and Software Engineering”. Cambridge University Press, 2010. Book

[3] J. Abrial, M. J. Butler, S. Hallerstede, T. S. Hoang, F. Mehta, and L. Voisin, “Rodin: an open toolset for modelling and reasoning in Event-B”, Int. J. Softw. Tools Technol. Transf., vol. 12, no. 6, pp. 447–466, 2010. pdf

[4] Y. A. Ameur, G. Dupont, I. Mendil, D. Méry, M. Pantel, P. Riviere, and N. K. Singh, “Empowering the Event-B Method Using External Theories”, in 17th Int. Conf. IFM 2022, vol. 13274 of LNCS, pp. 18–35, Springer, 2022. HAL

[5] Imitator web page: https://imitator.fr

[6] É. André, D. Marinho, L. Petrucci and J. van de Pol, “Efficient Convex Zone Merging in Parametric Timed Automata”, in 20th Int. Conf. FORMATS 2022, vol. 13465 of LNCS, pp. 200-218, Springer 2022. paper