基于 Real-Time Maude 的飞机多速率控制系统的 PALS 分析
计算机科学中的逻辑
2013-01-03 v1 软件工程
摘要
分布式信息物理系统（DCPS）广泛应用于航空和地面交通系统等领域，包括分布式混合系统的情况。由于异步通信、网络延迟和时钟偏差，DCPS 的设计和验证极具挑战性。此外，由于系统并发性导致的巨大状态空间爆炸，其模型检测验证通常变得不可行。PALS（“物理异步，逻辑同步”）方法已被提出，旨在将 DCPS 的设计和验证简化为设计和验证其底层同步版本这一更简单的任务。原始 PALS 方法假设单一逻辑周期，而多速率 PALS 将其扩展以处理组件可能以不同逻辑周期运行的多速率 DCPS。本文展示了如何应用多速率 PALS 来形式化验证一个非平凡的多速率 DCPS。我们使用 Real-Time Maude 形式化指定了一个多速率分布式混合系统，该系统包含一架由飞行员操纵的飞机，飞行员通过分布式控制系统按照指定角度转动飞机。我们的形式化分析表明，原始设计无法实现平滑的转向机动，从而导致了系统重新设计，以满足所需的正确性属性。这表明多速率 PALS 方法不仅对 DCPS 的形式化验证有效，还可有效地用于 DCPS 设计过程，甚至在属性验证之前。
引用
@article{arxiv.1301.0038,
title = {PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude},
author = {Kyungmin Bae and Joshua Krisiloff and José Meseguer and Peter Csaba Ölveczky},
journal= {arXiv preprint arXiv:1301.0038},
year = {2013}
}
备注
In Proceedings FTSCS 2012, arXiv:1212.6574