Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by concurrent processes that communicate with each other. However, existing specification logics cannot easily handle such models. In this paper, we present a specification logic and proof system for Hybrid Communicating Sequential Processes (HCSP), that extends CSP with ordinary differential equations (ODE) and interrupts to model interactions between continuous and discrete evolution. Because it includes a rich set of algebraic operators, complicated hybrid systems can be easily modelled in an algebra-like compositional way in HCSP. Our logic can be seen as a generalization and simplification of existing hybrid Hoare logics (HHL) based on duration calculus (DC), as well as a conservative extension of existing Hoare logics for concurrent programs. Its assertion logic is the first-order theory of differential equations (FOD), together with assertions about traces recording communications, readiness, and continuous evolution. We prove continuous relative completeness of the logic w.r.t. FOD, as well as discrete relative completeness in the sense that continuous behaviour can be arbitrarily approximated by discretization. Besides, we discuss how to simplify proofs using the logic by providing a simplified assertion language and a set of sound and complete rules for differential invariants for ODEs. Finally, we implement a proof assistant for the logic in Isabelle/HOL, and apply it to verify two case studies to illustrate the power and scalability of our logic.


翻译:---- 混合系统的演绎式验证近年来日益受到关注,因为它具有强大的可扩展性,其中一个适应于混合系统的强大规约逻辑是其基石。通常情况下,混合系统被自然地建模为相互通信的并发进程。然而,现有的规约逻辑不能轻松处理这种模型。本文介绍了一种用于混合通信顺序进程 (HCSP) 的规约逻辑和证明系统,该系统扩展了CSP与常微分方程 (ODE) 和中断以模拟连续和离散演化之间的交互。由于它包括一组丰富的代数运算符,所以可以使用类似代数的组合方法轻松地建模复杂的混合系统。我们的逻辑可以看作是基于持续时间演算 (DC) 的现有混合Hoare逻辑 (HHL) 的一般化和简化,也是并发程序现有Hoare逻辑的保守扩展。它的断言逻辑是关于微分方程的一阶理论 (FOD),同时包括记录通信、就绪性和连续演化的痕迹的断言。我们证明了逻辑相对于FOD的连续相对完备性,以及离散相对完备性,即连续行为可以通过离散化进行任意逼近。此外,我们讨论了如何使用逻辑简化证明,提供了简化的模式语言和一组基于ODE的微分不变量的声音和完整规则。最后,我们在Isabelle/HOL中实现了逻辑证明助手,并应用它来验证两个案例研究,以阐明我们逻辑的强大和可扩展性。

0
下载
关闭预览

相关内容

南大《优化方法 (Optimization Methods》课程,推荐!
专知会员服务
77+阅读 · 2022年4月3日
【2022新书】强化学习工业应用,408页pdf
专知会员服务
226+阅读 · 2022年2月3日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
【Google】平滑对抗训练,Smooth Adversarial Training
专知会员服务
48+阅读 · 2020年7月4日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
深度自进化聚类:Deep Self-Evolution Clustering
我爱读PAMI
15+阅读 · 2019年4月13日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【推荐】ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
机器学习研究会
20+阅读 · 2017年12月17日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
36+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2010年12月31日
Arxiv
0+阅读 · 2023年5月14日
Arxiv
0+阅读 · 2023年5月12日
Arxiv
12+阅读 · 2022年4月30日
VIP会员
相关VIP内容
南大《优化方法 (Optimization Methods》课程,推荐!
专知会员服务
77+阅读 · 2022年4月3日
【2022新书】强化学习工业应用,408页pdf
专知会员服务
226+阅读 · 2022年2月3日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
【Google】平滑对抗训练,Smooth Adversarial Training
专知会员服务
48+阅读 · 2020年7月4日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
深度自进化聚类:Deep Self-Evolution Clustering
我爱读PAMI
15+阅读 · 2019年4月13日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【推荐】ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
机器学习研究会
20+阅读 · 2017年12月17日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
36+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2010年12月31日
Top
微信扫码咨询专知VIP会员