- Alexandre Chapoutot (ENSTA Paris)
- Franck Delaplace (IBISC, UEVE)
Cyber-physical systems or biological systems are made of different kinds of components which are of different natures. Usually they can be modelled by hybrid systems mixing continuous-time parts and discrete-time parts which communicate and influence each other. Automatically analyzing, verifying, or synthetizing (part of) such systems is required to deal with the complexity.
Mathematical modelling of cyber-physical systems or biological systems involves different classes of mathematical models going from finite state automata to differential equations which may also involve distributed computations. The coupling of these classes of models requires a great care. All these elements make the application of formal methods challenging.
Formal methods as used in software verification (model checking, abstract interpretation, interactive proof) have to be adapted, extended to deal with continuous-time dynamical systems and the interaction with discrete-time parts.