Abstract

The growing importance of Connected Objects in the Internet of Things (IoT) poses new challenges concerning modeling and design of so-called Cyber-Physical Systems (CPS), where cyber/discrete controler programs interplay with physical (often continuous) environments. While there are generally well-established modeling practices in physical science domains (often including discretization), the need for equally formal modeling treatment of reactive control software itself becomes all the more important, since correctness of functional and non-functional properties relies on the whole range of models, including the software executable specification models. The scope of the PLoT4IoT proposal is entirely devoted to the definition and analysis of modeling paradigms relevant for design of (mainly the cyber part of) CPS. In this context, we shall study extensions to Logical Time models for CPS, dedicated one one hand to uncertainty and variability, on the other hand to spatio-temporal aspects and mobility. These models will be proposed for standardisation into the forthcomming version of the OMG UML Marte profile. On a more abstract level, we shall study the semantics and the analysis methods for open (concurrent) systems featuring explicit handling of data, time, locations, and propose new approaches to formal verification of safety properties of these systems. As a transversal mathematical tool for these works, we plan to develop new efficient stategies for “Satisfiability Modulo Theory” tools adapted to the 3 three modeling theories above.

Résumé

L’importance croissante des objets connectés dans l’Internet des objets (IoT) pose de nouveaux défis en matière de modélisation et de conception de systèmes dits cyber-physiques (CPS), dans lesquels les programmes de contrôle discrets (cyber) interagissent avec des environnements physiques (souvent continus). Bien qu’il existe généralement des pratiques de modélisation bien établies dans les domaines des sciences physiques (incluant souvent la discrétisation), la nécessité d’un traitement de modélisation formelle du logiciel de contrôle réactif lui-même devient d’autant plus importante que la correction des propriétés fonctionnelles et non fonctionnelles repose sur toute une variété de modèles, y compris les modèles de spécification exécutables par logiciel. Le champ d’application de notre projet est entièrement consacré à la définition et à l’analyse de paradigmes de modélisation pertinents pour la conception de (principalement la partie informatique de) CPS. Dans ce contexte, nous étudierons des extensions aux modèles de temps logique pour CPS, dédiées d’une part à l’incertitude et à la variabilité, d’autre part aux aspects spatio-temporels et à la mobilité. Ces modèles seront proposés pour normalisation dans la prochaine version du profil OMG UML Marte. A un niveau plus abstrait, nous étudierons la sémantique et les méthodes d’analyse de systèmes ouverts (concurrents) comportant un traitement explicite des données, du temps et de l’espace, et proposerons de nouvelles méthodes de vérification formelle des propriétés de sécurité de ces systèmes. En tant qu’outil mathématique transversal pour ces travaux, nous prévoyons de développer de nouvelles stratégies efficaces pour les outils «Théorie de la satisfiabilité», adaptées aux trois extensions de modélisation ci-dessus.