论文部分内容阅读
信息物理系统被广泛应用于交通、医疗、能源等多个重要发展领域。控制器局域网（CAN）是一种现场总线，该总线可应用于车载信息物理系统。在上述基于CAN的信息物理系统中，保证系统的安全性和可靠性是非常重要的。但是当前对于该系统的验证方法存在验证过程不规范、系统分析验证时对性能方面分析不足以及可验证的系统规模较小等问题。为对基于CAN的信息物理系统进行有效验证，提高人们对系统可靠性的可信度，本文首先提出了一种信息物理系统的形式化验证框架，通过对系统的各部分组件分别建模并根据它们的交互关系形成整个系统的形式化逻辑模型，从而对系统进行功能正确性验证和运行性能评估；然后针对基于CAN的信息物理系统，提供了一种构建时间自动机的方法流程，构建了系统各个基本模块的时间自动机模型，并对各个模型进行了形式化描述；最后，基于所提出的验证框架以及时间自动机模型，利用模型检验工具UPPAAL对基于CAN的车载信息物理系统进行了详细建模，并对不同环境配置下的系统进行了功能正确性验证以及性能分析。本文的实例研究工作表明所提出的形式化验证框架以及时间自动机模型是有效可行的，能够规范验证过程，并可以对系统的功能和性能方面进行有效验证，从而保证系统的安全可靠性。