Spatio-Temporal Properties Analysis for Cyber-Physical Systems
100 浏览量
2021-02-08
23:28:36
上传
评论
收藏 460KB PDF 举报
Spatio-Temporal Properties Analysis for Cyber-Physical Systems
Zhucheng Shao
1
, Jing Liu*
1
, Zuohua Ding
2
, Mingsong Chen
1
, Ningkang Jiang
1
1 Shanghai Keylab of Trustworthy Computing, East China Normal University, Shanghai, China
shaozhucheng@ecnu.cn, jliu@sei.ecnu.edu.cn
2 Center of Math Computing and Software Engineering, Zhejiang Sci-Tech University, Hangzhou, Zhejiang, China
Abstract—Cyber-Physical Systems (CPSs) integrate comput-
ing, communication and control processes. Close interactions
between the cyber and physical worlds occur in time and space
frequently. Therefore, both temporal and spatial information
should be taken into consideration when specifying properties
of CPS systems for verification. However, how to formulate
properties specifying spatial together with temporal features
is still an unsolved problem in the CPS. In this paper, we
propose an approach to analyze the spatio-temproal properties
of CPS. A spatio-temporal logic is developed, including the
syntax and semantics of the logic. With that logic, properties
of both states, transitions and global systems could be specified,
paving the way for further verification. To show the efficiency
of the approach , a Train Control System is introduced as a
case study. Meanwhile, more details about how to specifying
properties of CPS systems with our method are elaborated.
Keywords-spatio-temporal logic, CPS, property, specification
I. INTRODUCTION
The Cyber-Physical Systems (CPSs) are envisioned as
heterogeneous systems of systems, which involve com-
munication, computation, sensing, and actuating through
heterogeneous and widely distributed physical devices and
computation components [5], [6]. Therefore, CPS requires
close interactions between the cyber and physical worlds
in aspects of both in time and space. There are some
research works on designing and modeling CPS, such as
a CPS event model, which incorporates the spatio-temporal
attributes and observer information into the event definition,
which has been proposed by Tan.Y and et al [4]. An
extended UML statechart, Spatio-Temporal UML statechart
for CPSs (STUML Statechart) has been proposed in [3]. This
statechart is based on the UML Profile for Modeling and
Analysis of Real-time and Embedded (MARTE) systems.
In STUML Statecharts, they unified the logical time and
the chronometric time variables, and extend the traditional
events to CPS events. However, those work does not involve
in formal verification for CPSs. Our work is try to specify
properties of CPSs, as the prerequisite for formal verifica-
tion.
Temporal logic is used to describe any system of rules
and symbolism for representing, and reasoning about propo-
sitions qualified in terms of time. It has found an important
* Corresponding Author
application in formal verification, where it is used to specify
requirements of real-time systems. Propositional temporal
logic (PTL) is one of the best known temporal logics which
has found many applications in CS and AI, e.g. program
verification and specification [1], [10], [19]–[21], distributed
and multi-agent systems [9] or temporal databases [8]. In [1],
Zahar Manna and Amir Pnueli gave a detailed methodology
for the specification, verification, and development of real-
time systems using the tool of temporal logic. However, the
existing approaches can not be used directly to specifying
properties of Cyber-Physical Systems. The reason is the
truth-values of spatial propositions can not be expressed.
Spatial logic is a number of logics suitable for quali-
tative spatial representation and reasoning, such as RCC-
8, BRCC, S4
u
and other fragments of S4
u
. The most
expressive spatial formalism of them is S4
u
, which extends
by S4 with the universal modalities [13]–[15]. S4 was
introduced independently be Orlov, Lewis and G
¨
odel without
any intention about space [11], [12]. In [13]–[15], they gave
an interpretation of topological space. For modeling the
truth-values of spatial propositions, the spatial logic should
be taken into consideration in our constructed logic.
Spatio-temporal logic is the next apparent and natural
step by combining these two kinds of reasoning. There
have been attempts to construct spatio-temporal hybrids.
For example, in [16], Finger and Gabbay introduced a
methodology whereby an arbitrary logic system L can be
enriched with temporal features to create a new system
T (L). The new system is constructed by combining L with
a pure propositional temporal logic T . In [17], Wolter and
Zakharyaschev constructed a spatio-temporal logic, based
on RCC-8 and PTL, intended for qualitative knowledge
representation and reasoning about the behavior of spatial
regions in time. Nevertheless, RCC-8 is a fragment of S4
u
and has rather limited expressive power [18]. The syntax
of RCC-8 only contains eight binary predicates. Nor can
RCC-8 represent complex relations between more than two
regions. Following their way, we will construct our spatio-
temporal logic by enriching PTL with S4
u
.
This paper is organized as follows. Section II gives
the existent propositional logics(e.g. S4, S4
u
, PTL) for
modeling the space and time. In section III, we develop a
spatio-temporal logic based on S4
u
and PTL, together with
the syntax and semantics of the logic. Section IV presents
2013 International Conference on Engineering of Complex Computer Systems
978-0-7695-5007-7/13 $26.00 © 2013 IEEE
DOI 10.1109/ICECCS.2013.23
101
评论0