A Semantic Model for Interacting Cyber-Physical Systems

被引:3
作者
Lion, Benjamin [1 ]
Arbab, Farhad [1 ,2 ]
Talcott, Carolyn [3 ]
机构
[1] Leiden Univ, Leiden, Netherlands
[2] CWI, Amsterdam, Netherlands
[3] SRI Int, Menlo Pk, CA USA
来源
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2021年 / 347期
关键词
D O I
10.4204/EPTCS.347.5
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the no-tion of a component abstracts the internal details of both cyber and physical processes, to expose a uniform semantic model of their externally observable behaviors expressed as sets of sequences of observations. We introduce algebraic operations on such sequences to model different kinds of component composition. These composition operators yield the externally observable behavior of their resulting composite components through specifications of interactions of the behaviors of their constituent components, as they, e.g., synchronize with or mutually exclude each other's alternative behaviors. Our framework is expressive enough to allow articulation of properties that coordinate desired interactions among composed components within the framework, also as component behav-ior. We demonstrate the usefulness of our formalism through examples of coordination properties in a CPS consisting of two robots interacting through shared physical resources.
引用
收藏
页码:77 / 95
页数:19
相关论文
共 24 条
  • [1] DEFINING LIVENESS
    ALPERN, B
    SCHNEIDER, FB
    [J]. INFORMATION PROCESSING LETTERS, 1985, 21 (04) : 181 - 185
  • [2] Abstract Behavior Types: a foundation model for components and their composition
    Arbab, F
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2005, 55 (1-3) : 3 - 52
  • [3] Arbab F, 2003, LECT NOTES COMPUT SC, V2755, P34
  • [4] Bouraoui Nina., 2007, Tomboy
  • [5] Hyperproperties
    Clarkson, Michael
    Schneider, Fred
    [J]. JOURNAL OF COMPUTER SECURITY, 2010, 18 (06) : 1157 - 1210
  • [6] cwi, US
  • [7] de Alfaro L., 2001, EMSOFT 01, V2211, P148, DOI DOI 10.1007/3-540-45449-7_11
  • [8] Dynamic networks of heterogeneous timed machines
    Fiadeiro, Jose
    Lopes, Antonia
    Delahaye, Benoit
    Legay, Axel
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2018, 28 (06) : 800 - 855
  • [9] Realizing ω-regular Hyperproperties
    Finkbeiner, Bernd
    Hahn, Christopher
    Hofmann, Jana
    Tentrup, Leander
    [J]. COMPUTER AIDED VERIFICATION, PT II, 2020, 12225 : 40 - 63
  • [10] Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
    Kanovich, Max
    Kirigin, Tajana Ban
    Nigam, Vivek
    Scedrov, Andre
    Talcott, Carolyn
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2016, 2016, 9884 : 228 - 244