Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue ACM Transactions on Software Engineering and Methodology Année : 2022

Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP

Résumé

Model-based design has become the predominant approach to the design of hybrid and cyber-physical systems (CPSs). It advocates the use of mathematically founded models to capture heterogeneous digital and analog behaviours from domain-specific formalisms, allowing all engineering tasks of verification, code synthesis and validation to be performed within a single semantic body. Guaranteeing the consistency among the different views and heterogeneous models of a system at different levels of abstraction however poses significant challenges. To address these issues, Hoare and He's Unifying Theories of Programming (UTP) proposes a calculus to capture domain-specific programming and modelling paradigms into a unified semantic framework. Our goal is to extend UTP to form a semantic foundation for CPS design. Higher-Order UTP (HUTP) is a conservative extension to Hoare and He's theory which supports the specification of discrete, real-time and continuous dynamics, concurrency and communication, and higher-order quantification. Within HUTP, we define a calculus of normal hybrid designs to model, analyse, compose, refine and verify heterogeneous hybrid system models. In addition, we define respective formal semantics for HCSP (Hybrid Communicating Sequential Processes) and Simulink using HUTP. CCS Concepts: • Theory of computation → Timed and hybrid models; Denotational semantics.
Fichier principal
Vignette du fichier
tosem22.pdf (1.32 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03888055 , version 1 (05-01-2023)

Identifiants

Citer

Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan. Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP. ACM Transactions on Software Engineering and Methodology, 2022, pp.1-47. ⟨10.1145/3517192⟩. ⟨hal-03888055⟩
24 Consultations
96 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More