A Model-Based Toolchain to Verify Spatial Behavior of Cyber-Physical Systems

被引：12

作者：

Herrmann, Peter ^{[1
]}

Blech, Jan Olaf ^{[2
]}

Han, Fenglin ^{[1
]}

Schmidt, Heinz ^{[2
]}

机构：

[1] Norwegian Univ Sci & Technol NTNU, Trondheim, Norway

[2] RMIT Univ, Melbourne, Vic, Australia

来源：

INTERNATIONAL JOURNAL OF WEB SERVICES RESEARCH | 2016年 / 13卷 / 01期

关键词：

BeSpaceD; Model-Based System Engineering; Reactive Blocks; Real-Time Properties; Spatial Behavior Modeling and Verification; LOGIC; CONCURRENCY; AUTOMATA;

D O I：

10.4018/IJWSR.2016010103

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

080201 [机械制造及其自动化];

摘要：

A method preserving cyber-physical systems to operate safely in a joint physical space is presented. It comprises the model-based development of the control software and simulators for the continuous physical environment as well as proving the models for spatial and real-time properties. The corresponding toolchain is based on the model-based engineering tool Reactive Blocks and the spatial model checker BeSpaceD. The real-time constraints to be kept by the controller are proven using the model checker UPPAAL.

引用

页码：40 / 52

页数：13

共 27 条

[1]

Alur Rajeev, 1990, LNCS, V443, P322

[2]

[Anonymous], IMPR SYST SOFTW ENG

[3]

Bengtsson J., 1996, Hybrid Systems III. Verification and Control, P232, DOI 10.1007/BFb0020949

[4]

Multi-dimensional modal logic as a framework for spatio-temporal reasoning [J].