Automatic Dimensional Analysis of Cyber-Physical Systems

Automatic Dimensional Analysis of Cyber-Physical Systems
复制标题

信息物理系统的自动维度分析

DOI:
--
复制
发表时间:
2012
期刊:
World Congress on Formal Methods
影响因子:
--
通讯作者:
N. Shankar
N. Shankar
中科院分区:
--
文献类型:
--
作者:
S. Owre;I. Saha;N. Shankar

文献摘要

被引文献

相似文献

构建网络物理系统的第一步是构建一个捕获相关行为的忠实模型。尺寸一致性提供了对此类模型及其所表示的物理量的正确性的首次检查。尽管在物理科学中使用尺寸的手动分析来查找公式中的错误,但这种方法无法扩展到具有许多交互组件的复杂网络物理系统。我们推出 DimSim,这是一种自动检查 Simulink 中建模的网络物理系统的尺寸一致性的工具。 DimSim 以模块化方式从 Simulink 模型中为每个子系统生成一组约束,并使用 Gauss-Jordan 消除法求解它们。该工具依赖于用户提供的尺寸注释,它可以检测给定尺寸约束中的不一致和规格不足。如果出现尺寸不一致,DimSim 可以提供一组最小的约束来捕获不一致的原因。我们已将 DimSim 应用到来自不同嵌入式系统领域的大量示例中。实验结果表明,DimSim 中的维度分析具有可扩展性,并且能够发现网络物理系统模型中的关键错误。
The first step in building a cyber-physical system is the construction of a faithful model that captures the relevant behaviors. Dimensional consistency provides the first check on the correctness of such models and the physical quantities represented in it. Though manual analysis of dimensions is used in physical sciences to find errors in formulas, this approach does not scale to complex cyber-physical systems with many interacting components. We present DimSim, a tool to automatically check the dimensional consistency of a cyber-physical system modeled in Simulink. DimSim generates a set of constraints from the Simulink model for each subsystem in a modular way, and solves them using the Gauss-Jordan elimination method. The tool depends on user-provided dimension annotations, and it can detect both inconsistency and underspecification in the given dimensional constraints. In case of a dimensional inconsistency, DimSim can provide a minimal set of constraints that captures the cause of the inconsistency. We have applied DimSim to numerous examples from different embedded system domains. Experimental results show that the dimensional analysis in DimSim is scalable and is capable of uncovering critical errors in models of cyber-physical systems.