Model composition for early verification and validation in the context of smart manufacturing
Published : 19 December 2016
A 3-year PhD position is available in the List Institute of CEA (the French Alternative Energies and Atomic Energy Commission) to explore tools and methods for designing and validating smart factories. In particular, the main objective is to define and compose the required modeling languages to capture the architecture of a given factory, the missions of the various coordinated robots and the liveness and safety properties to ensure. Such properties cover different concerns from equipments’ control/command, industrial networks to service orchestration. The required formalisms will be designed as a set of coordinated domain-specific modeling languages, from which one can extract system’s views to verify and validate temporal properties. The second part of the PhD work will consist in defining a verification and validation method based on the designed modeling languages. The method has to handle the dynamicity of such systems and guarantee properties preservation during runtime reconfigurations.
The position is available at CEA Saclay Nano-innov at Palaiseau (near Paris), in collaboration with the DiverSE team at IRISA (Rennes). It will be supervised by Benoît Combemale (thesis advisor at IRISA – Rennes) and Selma Azaiez (co-supervisor at CEA).
The candidate should have a strong background in programming languages, language theory, software-language engineering and model driven engineering. Additionally, the candidate would have additional skills in software validation and verification. Good reading and writing skills in English are required.