Timed-pNets: A formal communication behavior model for real-time CPS systems

Abstract. We propose a semantic model named timed-pNets to define hierarchical structures for CPSs as well as its communication behaviors semantic with time constraints. Logical clocks relations are introduced to describe the partial order of event occurring. After setting (time)-boundaries and designing properties, we use the TimeSquare tool to simulate the system and check its properties.