• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE Annual Computers, Software, and Applications Conference >Model Checking Software in Cyberphysical Systems
【24h】

Model Checking Software in Cyberphysical Systems

机译：网络物理系统中的模型检查软件

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Model checking a software system is about verifying that the state trajectory of every execution of the software satisfies formally specified properties. The set of possible executions is modeled as a transition system. Each "state" in the transition system represents an assignment of values to variables, and a state trajectory (a path through the transition system) is a sequence of such assignments. For cyberphysical systems (CPSs), however, we are more interested in the state of the physical system than the values of the software variables. The value of model checking the software therefore depends on the relationship between the state of the software and the state of the physical system. This relationship can be complex because of the real-time nature of the physical plant, the sensors and actuators, and the software that is almost always concurrent and distributed. In this paper, we study different ways to construct a transition system model for the distributed and concurrent software components of a CPS. We describe a logical-time based transition system model, which is commonly used for verifying programs written in synchronous languages, and derive the conditions under which such a model faithfully reflects physical states. When these conditions are not met (a common situation), a finer-grained event-based transition system model may be required. Even this finer-grained model, however, may not be sufficiently faithful, and the transition system model needs to be refined further to express not only the properties of the software, but also the properties of the hardware on which it runs. We illustrate these tradeoffs using a coordination language called Lingua Franca that is well-suited to extracting transition system models at these various levels of granularity, and we extend the Timed Rebeca language and its tool Afra to perform this extraction and then to perform model checking.
机译：模型检查软件系统是关于验证软件的每次执行的状态轨迹是否满足正式指定的属性。可能执行的集合被建模为过渡系统。过渡系统中的每个“状态”代表变量的值分配，状态轨迹（通过过渡系统的路径）是这种分配的序列。但是，对于网络物理系统（CPS），我们对物理系统的状态比对软件变量的值更感兴趣。因此，对软件进行模型检查的价值取决于软件状态与物理系统状态之间的关系。由于物理工厂，传感器和执行器以及几乎总是并发和分布式的软件的实时性，因此这种关系可能很复杂。在本文中，我们研究了为CPS的分布式和并行软件组件构建过渡系统模型的不同方法。我们描述了一个基于逻辑时间的转换系统模型，该模型通常用于验证用同步语言编写的程序，并推导出该模型如实反映物理状态的条件。当不满足这些条件时（常见情况），可能需要更细粒度的基于事件的过渡系统模型。但是，即使是这种更细粒度的模型也可能不够忠实，并且过渡系统模型还需要进一步完善，以不仅表达软件的属性，而且表达其运行所在的硬件的属性。我们使用称为Lingua Franca的协调语言来说明这些折衷，该语言非常适合于在这些不同的粒度级别上提取过渡系统模型，并且我们扩展了Timed Rebeca语言及其工具Afra来执行此提取，然后执行模型检查。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号