ACM通信
研究突出了
技术角度:我们可以验证信息物理系统吗?
在过去的几十年里，计算机已经从专门用途和独立的数字处理处理器转变为与物理世界交互的网络设备。充分认识到这方面的潜力cyber-physical系统要求处理和通信技术的进步与以成本效益的方式设计这种系统的工具的进步相匹配。事实上，如果我们不能保证在所有可以想象的条件下的安全，我们谁也不会愿意驾驶自动驾驶汽车，或使用可以由医生远程编程的起搏器。目前系统设计中的实践主要依赖于模拟，以确保系统仅在设计团队选择的少数场景中按预期工作。另一方面，正式的验证可以通过探索系统所有可能执行的空间，在极端情况下捕获错误。
验证问题在计算上是固有的棘手问题，但是研究人员已经在开发用于验证硬件和软件系统的方法、算法和工具方面取得了稳定的进展。特别是，模型检查——一种象征性地探索系统模型所有可达状态空间的技术——被认为是一个成功的故事理论在实践中，因为它被用于检查多处理器设计和设备驱动程序代码的正确性。在这些应用程序中，模型是纯离散的。为了分析像起搏器这样的信息物理系统，我们需要考虑与物理世界交互的离散软件控制器，这通常是用微分方程建模的。为这种混合离散模拟模型(也称为混合系统)开发有效的符号验证技术已被证明是一个具有挑战性的问题，近年来吸引了形式化方法和控制理论社区的大量研究。Althoff等人的以下论文报告了这一探索的一个重要里程碑。
由于正式的验证技术具有很高的计算成本，因此需要用手术刀而不是锤子来应用它们。两位作者在选择研究对象时表现得非常谨慎。的设计电荷泵锁相环代表了混合系统验证所涉及的技术挑战和形式分析的潜在好处。虽然设计明确规定了稳定性和稳定时间的要求，但模型中的离散开关意味着经典控制理论方法不能从解析上保证这些。初始条件和参数选择的变化使它成为符号方法的理想目标。
下面报告的实验结果非常重要，因为作者证明了他们的符号模拟方法在计算需求方面与工业标准的模拟工具具有竞争力。
混合系统可达状态的符号计算需要为系统状态集选择一种表示形式，因此应用单一模拟步骤的结果可以在这种表示形式上有效地计算。此外，表示的复杂性应该随着模拟步骤的数量而增加。这篇论文的技术优势在于作者使用的技术的精细组合来实现这种符号计算。他们方法的一个关键新颖之处在于通过计算开关时间范围的边界来过度逼近每个模拟步骤的结果。这种新方法在跨模拟步骤保持符号表示的简单性方面至关重要，并允许搜索深入到足以建立稳定性的程度。
下面报告的实验结果非常重要，因为作者证明了他们的符号模拟方法在计算需求方面与工业标准的模拟工具具有竞争力。这种成本效益的演示有望成为说服Mathworks等商业供应商认真投资探索混合系统验证技术向工业实践过渡的关键。
数字图书馆是由计算机协会出版的。版权所有©2013 ACM, Inc.
没有发现记录