物联网的建模和验证是物联网研究的一个重要领域。由于集成了物理进程,物联网表现出传统软件系统所不具备的物理特性。这些性质作为物联网系统中必不可少的一部分,必须在物联网模型中进行描述。移动性作为一种物理属性,能够描述物联网中物理实体的移动以及信息的流动,本文对物联网的移动性进行研究,提出了一种基于安全灰箱演算的物联网模型,并且使用灰箱逻辑对其进行分析验证。该方法能够对物联网的移动性进行描述分析,适用于具有移动特征的物联网应用。以欧洲火车控制系统(ETCS)为例,验证了本文建模和验证方法的可行性。
The modeling and verification is an important area in the research of cyber physical systems (CPS). By integrating physical processes, CPS has many physical properties, not in traditional software systems, which must be described in the model of CPS. In this paper, the mobility of CPS is studied. As a physical property, the mobility can describe the movement of physical entities and the flow of information in CPS. A model of CPS based on Mobile Safe Ambients is proposed in this paper, whose properties are analyzed and verified by means of ambient logic. The proposed model can describe and analyze mobility in CPS, and is suitable for applications of mobile CPS. The case study on European Train Control System (ETCS) shows the feasibility of the proposed method on the modeling and verification.