Formal Verification of Cyber-Physical Systems using Theorem Proving (Invited Paper)
由于软件和工程技术的重大突破，嵌入式系统越来越多地用于航空航天和下一代交通系统，智能电网和智能城市，医疗保健系统，以及广义上的网络物理系统（CPS）。CPS主要由几个电子、通信和控制器模块以及一些致动器和传感器组成。异构底层智能技术的混合对设计提出了许多技术挑战，更严重的是对这种复杂基础设施的验证。事实上，CPS应遵守严格的安全性，可靠性，性能和安全性要求，其中需要捕获各种CPS模块的物理和随机方面，然后分析它们在相互关联的连续和离散动态中的相互关系。然而，通常情况下，系统错误在分析过程中不会被发现，从而导致不必要的情况，这些情况可能在安全关键应用中产生严重后果。在本文中，我们介绍了一些挑战，围绕当代CPS的设计和验证与智能技术的出现。特别是，我们调查最近的事态发展中使用的定理证明，一种正式的方法，CPS的建模，分析和验证，并概述了一些现实世界的CPS案例研究，从汽车，航空电子和健康技术领域从系统级的物理组件。
2020-03-08 cs.LO
An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems
基于搜索的测试被广泛用于发现复杂网络物理系统模型中的错误。最新的研究工作已经改进了这种方法，铸造它作为一个正式指定的时间属性的证伪过程，利用信号时序逻辑的鲁棒性语义。将这种方法扩展到高度复杂的工程系统需要有效的证伪程序，这也应该适用于黑箱模型。输入往往是时间依赖函数，这也加剧了伪造。我们利用主动学习领域的机器学习技术，解决了网络物理系统复杂黑盒模型的形式属性的伪造问题。量身定制这些技术与时间相关的，功能性输入的证伪问题，我们表现出相当大的增益计算工作量，通过减少所需的模型模拟的数量。所提出的方法的优点是讨论了一个具有挑战性的工业级基准汽车。
2017-08-28 cs.LO
Monitoring Spatially Distributed Cyber-Physical Systems with Alternating Finite Automata
本文提出从STREL逻辑规范构建加权交替有限自动机，以高效编码时空语义，并在模拟无人机群环境中实现离线和在线监控。
2025-03-27 cs.FL cs.LO cs.MA
Hybrid Automata for Formal Modeling and Verification of Cyber-Physical Systems
离散控制（“网络”）和模拟环境（“物理”）之间的紧密集成-通过有线或无线通信网络上的传感器和执行器-是网络物理系统的定义特征。因此，信息物理系统的功能正确性不仅关键地取决于模拟物理环境的动态，而且还取决于改变环境动态的离散控制所采取的决策。混合自动机的框架-介绍了由Alberr，Courcoubetis，Henzinger和Ho-提供了一个正式的建模和规范环境来分析网络物理系统的离散和连续部分之间的相互作用。混合自动机可以被认为是有限状态自动机的推广，其在每个状态下的动态由常微分方程系统控制。此外，混合自动机的离散转换是由这些实值变量的值的约束，并使这些变量的演化不连续的跳跃。考虑到混合自动机中动力学的丰富性，一般模型的基本验证问题（如可达性和可扩展性）是不可判定的，这也许并不奇怪。在这篇文章中，我们提出了一个审查的混合自动机作为建模和验证框架的网络物理系统，并调查一些关键结果有关的实际验证问题的混合自动机。
2015-03-17 cs.FL cs.LO
Formal Requirement Elicitation and Debugging for Testing and Verification of Cyber-Physical Systems
School of Computing, Informatics and Decision Systems Arizona State University（亚利桑那州立大学计算、信息与决策系统学院）
本文提出一个用于物理系统形式化规格的 elicitation 与调试框架，通过图形界面处理规格 elicitation，提供两种调试算法以解决规格错误，通过用户研究验证框架能有效解决常见规格错误。
2018-07-27 cs.LO cs.SE cs.SY
Cyber-Physical Systems, a new formal paradigm to model redundancy and resiliency
网络物理系统（CPS）是由物理组件组成的系统，该物理组件由网络组件（基于计算机的算法）控制或监控。CPS技术和科学的进步正在实现远远超过当今简单嵌入式系统的能力、适应性、可扩展性、弹性、安全性和可用性。CPS技术正在改变人们与工程系统交互的方式。新的智能CPS正在推动农业、能源、交通、医疗保健和制造业等各个领域的创新。他们正在引领第四次工业革命（工业4.0），这得益于生产的高度灵活性。工业4.0生产模式的特点是其生产要素在所有制造过程中具有高度的相互通信特性。这就是为什么它是一个核心概念，系统应该如何结构优化，以具有足够的冗余水平，令人满意的弹性。这一目标可以受益于在各种科学领域如人工智能中众所周知的形式化方法。因此，当前的研究涉及CPS元模型的提出及其实例化。通过这种方式，它列出了CPS本身之间及其（网络和物理）组件之间可能发生的所有类型的关系。使用CPS元模型形式化，适应形式概念分析（FCA）的正式方法，本文提出了一种方法来优化CPS系统的建模，强调其冗余和弹性。
2018-10-16 cs.DB cs.IT cs.LO
Towards an ontology of state actors in cyberspace
University at Buffalo（布法罗大学）；National Center for Ontological Research（国家本体论研究中心）
本文提出构建网络空间国家行为体与网络行动的形式化本体，以整合多源数据、支持自动推理和情报复用，并给出评估、扩展现有网络安全本体工具的指标与计划。
2024-08-03 cs.AI cs.CR cs.LO
A Theory of Hypergames on Graphs for Synthesizing Dynamic Cyber Defense with Deception
Worcester Polytechnic Institute（伍斯特理工学院）
在这一章中，我们提出了一种方法，使用形式化的方法来综合反应式防御策略的赛博网络，配备了一套诱饵系统。我们首先推广正式的图形安全模型-攻击图-将防御者的对策在博弈论模型，称为攻击-防御游戏图。这个游戏以形式逻辑捕捉防御者和攻击者之间的动态交互以及他们的防御/攻击目标。然后，我们引入了一类超对策模型的攻击者和防御者的互动中的诱饵所产生的信息不对称。给出了形式逻辑中的定性安全规范，我们证明了形式方法中的超博弈和反应合成的解决方案概念可以扩展到使用网络欺骗来合成有效的动态防御策略。该策略利用攻击者的错误感知来保证安全性，而当信息对称时，这可能是不满足的。
2020-08-07 cs.AI cs.CR cs.GT
Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
本文提出 IsaVODEs 框架，在 Isabelle/HOL 中形式化信息物理系统验证，并通过 ODE 唯一解认证与不变式推理等机制提升自动化和可扩展性。
2024-01-22 cs.LO cs.MS
Modeling and Verifying Cyber-Physical Systems with Hybrid Active Objects
网络物理系统（CPS）的正式建模很困难，因为它们提出了离散-连续动态和并发行为相结合的双重挑战。现有的CPS形式化规范和验证语言都是在其底层证明搜索技术之上设计的。它们缺乏高层次的结构要素。此外，它们不能有效地执行。这使得正式的CPS模型难以理解和验证，从而削弱了它们的可用性。相反，我们建议在一个活动对象（AO）语言设计的并发系统的简洁，直观的建模CPS模型。为此，我们扩展了AO语言ABS和混合主动对象（HAO）的运行时环境。在HAO中形式化的CPS模型和需求必须遵循某些通信模式，这些模式允许自动转换为差分动态逻辑，即顺序混合程序逻辑。验证是通过使用定理证明器KeYmaera X释放结果公式来实现的。我们证明了我们的方法与案例研究的实用性。
2019-06-13 cs.LO cs.PL cs.SY
A Formal Approach to Physics-Based Attacks in Cyber-Physical Systems (Extended Version)
我们应用形式化方法来奠定和简化理论基础，以推理网络物理系统（CPS）和基于物理的攻击，即，针对物理设备的攻击。我们专注于一个正式的治疗的完整性和拒绝服务攻击的传感器和执行器的CPS，这些攻击的时间方面。我们的贡献是四倍的。(1)~我们定义了一个混合进程演算来对CPS和基于物理的攻击进行建模。(2)我们正式定义了一个威胁模型，该模型指定了MITM攻击，这些攻击可以操纵传感器读数或控制命令，以将CPS驱动到不期望的状态，并且我们提供了评估攻击容忍度/漏洞的方法。(3)~我们正式确定了如何估计成功攻击对CPS的影响，并调查攻击成功机会的可能量化。(4)~我们通过在Uppaal SMC中形式化一个非平凡的运行示例来说明我们的定义和结果，Uppaal SMC是Uppaal模型检查器的统计扩展;我们使用Uppaal SMC作为一个自动工具，用于对我们的运行示例进行静态安全分析，并且当暴露于三种不同的基于物理的攻击时，具有不同的影响。
2021-05-22 cs.CR cs.LO cs.SY
Structured Proofs for Adversarial Cyber-Physical Systems
许多网络物理系统（CPS）是安全关键的，因此形式化地验证它们是很重要的，例如，在形式逻辑中显示模型的正确性规范始终保持。构造性微分博弈逻辑（CdGL）是一种用于（构造性）混合博弈（包括混合系统）的逻辑。为了克服不可判定性，用户首先写一个证明，我们提出了一个证明检查工具。我们介绍Kaisar，第一个语言和工具的CdGL证明，到目前为止，只能用一个低层次的证明演算手工编写。Kaisar的结构化证明简化了具有挑战性的CPS证明任务，特别是通过使用程序设计语言原则和高级状态推理。Kaisar利用CdGL的构造性和细化关系来构建游戏策略模型的证明。该评估再现并扩展了现有的1D和2D驾驶案例研究。证据指标进行了比较，并报告的经验进行了讨论，为原来的研究和他们的复制品。
2021-07-19 cs.LO cs.PL
Compositional Cyber-Physical Systems Theory
本论文建立了一个组成的网络物理系统理论，以开发具体的语义相关的安全和安全保证所需的上述不同的观点。在这个意义上，组合可以采取两种形式。第一种是在需求、行为和体系结构的每一个单独的形式体系中，将较小的模型组合成较大的模型，这可以被认为是水平组合--这是一个很大程度上已经解决的问题。该理论的第二个也是主要贡献是垂直组合，这意味着在需求、行为和架构模型及其相关的代数中关联或以其他方式提供经过验证的组合。在这篇论文中，我们展示了一个可能的解决方案，垂直组合是使用工具，从范畴理论。范畴论是使水平和垂直组合形式上明确的自然候选者，因为它可以联系，比较和/或统一不同的代数。
2021-09-10 cs.CR cs.LO cs.SY
Self-Driving Vehicle Verification Towards a Benchmark
University of Pennsylvania（宾夕法尼亚大学）
本文提出一个简单的形式化模型用于自动驾驶车辆，尽管经过简化后其安全性已手动证明，但目前尚无自动形式化验证工具支持其动态特性，旨在为形式化验证工具提供挑战。
2018-06-20 cs.LO cs.RO cs.SY
Measuring Robustness in Cyber-Physical Systems under Sensor Attacks
本文基于微分动态逻辑提出信息物理系统传感器攻击下的定量鲁棒性分析框架，定义前向/后向安全与鲁棒性、仿真距离概念，构建证明系统，并通过自动驾驶车辆、水箱案例验证方法有效性。
2024-03-09 cs.CR cs.ET cs.LO
