面向信息物理系统的模块化规约与验证
计算机科学中的逻辑
2018-03-09 v1
摘要
信息物理系统 (CPS) 是由一个或多个基于计算机的组件与一组物理组件（通常描述为传感器与执行器）紧密集成控制的系统，这些物理组件可直接连接到计算机组件，或位于远程位置并通过网络连接访问。此类系统的建模与验证是一项困难且易出错的任务，需要严谨的技术。混合自动机是一种用常微分方程描述连续行为来扩展有限状态自动机的形式化方法。本文使用基于重写逻辑的技术对 CPS 进行建模与验证，从而探索一种形式化技术来开发此类系统，该技术将富有表达力的规约与基于状态的高效分析相结合。此外，我们旨在实现此类系统的模块化规约，使每个 CPS 组件独立规约，最终系统作为其组成组件的同步乘积浮现。我们使用线性混合自动机对 CPS 建模，并在 Real-Time Maude（一种用于实时系统的重写逻辑工具）中实现。利用该方法，我们为 -水库问题开发了一个规约，该 CPS 根据水管与水库的物理性质控制水管以填充若干水库。
引用
@article{arxiv.1803.03173,
title = {Towards the Modular Specification and Validation of Cyber-Physical Systems},
author = {Andre Metelo and Christiano Braga and Diego Brandão},
journal= {arXiv preprint arXiv:1803.03173},
year = {2018}
}