Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking
嵌入式系统中软件的复杂性在过去几年中显著增加，因此软件验证现在在确保整体产品质量方面起着重要作用。在这种背景下，基于SAT的有界模型检验被成功地应用于发现细微的错误，但对于更大的应用，它往往遭受状态空间爆炸问题。本文介绍了一种新的方法，称为连续验证，以检测设计错误，尽快通过查看软件配置管理（SCM）系统，并结合动态和静态验证，以减少状态空间进行探索。我们还给出了一组编码，提供准确的支持程序验证，并使用不同的背景理论，以提高可扩展性和精度在一个完全自动的方式。从电信领域的案例研究表明，所提出的方法提高了错误检测能力，并减少了高达50%的整体验证时间。
2009-11-19 cs.SE
Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems (extended version)
我们提出了一种替代方法来解决硬件（HW）和软件（SW）分区问题，它使用基于可满足性模理论（SMT）的有界模型检验（BMC）结合使用开放多处理的多核支持。基于多核SMT的BMC方法允许基于模型检查器可用的处理器核数初始化许多验证实例。每个实例检查不同的最优值，直到满足优化问题。我们的目标是表明，多核模型检查技术可以是有效的，在特定情况下，找到最佳的解决方案的HW-SW分区问题使用基于SMT的BMC方法。实验结果表明，该方法与传统的线性规划算法和遗传算法相比具有更好的收敛性。
2015-09-08 cs.LO cs.SE
Evaluation of A Resilience Embedded System Using Probabilistic Model-Checking
如果微处理器单元（MPU）接收到作为噪声的外部电信号，则系统功能将容易冻结或故障。一个新的弹性策略，以实现自动复位MPU和停止冻结或故障的MPU。该技术对于工作在非人类环境中的嵌入式系统是有用的。然而，评估复原力战略是困难的，因为它们的有效性取决于许多复杂的相互作用的因素。在本文中，我们使用概率模型检验来评估安装了上述新的弹性策略的嵌入式系统。定性评价采用6个PCTL公式，定量评价采用两种评价方法。一个是减少系统故障，另一个是ADT（平均停机时间），这是行业标准。我们的工作证明了弹性战略带来的好处。实验结果表明，我们的评估是成本效益和可靠的。
2014-05-06 cs.LO cs.SE math.PR
Model Checking Embedded C Software using k-Induction and Invariants (extended version)
本文提出了一种基于归纳法的证明方法，将k-归纳法与不变量相结合，对嵌入式C软件中有界循环和无界循环进行模型检验。k-归纳算法由三种情况组成：在基本情况下，我们的目标是找到一个反例，最多有k个循环展开;在正向条件下，我们检查循环是否已经完全展开，以及安全属性P是否在k个展开内的所有状态下都成立;在归纳步骤中，我们检查每当P对k个展开成立时，它在系统的下一个展开后也成立。对于k-归纳算法的每一步，我们使用仿射约束来推断不变量（即，多面体）指定前置和后置条件。实验结果表明，我们的方法可以处理各种各样的安全特性，在典型的嵌入式软件应用程序，从电信，控制系统和医疗设备，我们证明了改进的感应算法的有效性，如果与其他方法相比。
2015-09-08 cs.LO cs.SE
Dynamic Verification of SystemC with Statistical Model Checking
许多嵌入式和实时系统具有固有的概率行为（传感器数据，不可靠的硬件等）。在这种情况下，至关重要的是评估系统属性，如“特定硬件故障的概率”。这样的属性可以通过使用概率模型检验来评估。然而，由于状态空间爆炸，这种技术在代表现实嵌入式和实时系统的模型上失败了。为了克服这个问题，我们提出了一个基于统计模型检验的验证框架。我们的框架是能够评估的概率和时间属性在SystemC，一个标准的系统级建模语言建模的大型系统。它作为Plasma-lab统计模型检查器的扩展完全实现。我们说明了我们的方法上的多升系统的案例研究。
2015-09-21 cs.LO cs.SE
Early Verification of Legal Compliance via Bounded Satisfiability Checking
本文提出一种基于 SMT 的有界可满足性检查方法，用于在早期需求阶段验证 MFOTL 形式化的法律合规性，并在多个领域案例中证明其能高效判定合规或生成反例。
2023-05-28 cs.SE
Variability Abstraction and Refinement for Game-based Lifted Model Checking of full CTL (Extended Version)
可变性模型允许为各种配置有效地构建许多自定义模型变体。针对可变性模型的提升模型检验能够通过利用变体之间的相似性在单次运行中同时验证其所有变体。提升模型检验的计算成本仍然很大程度上取决于变量的数量（配置空间的大小），这通常是巨大的。在提升模型检验中，对抗配置空间爆炸问题的最有前途的方法之一是可变性抽象。在这项工作中，我们定义了一种新的基于游戏的方法，用于特定于变量的抽象和改进，用于对完整CTL进行提升模型检验，并在3值语义上进行解释。我们提出了一个直接的算法来解决一个3值（抽象）提升模型检验游戏。针对抽象变异模型的模型检验结果不确定的情况，提出了精化的概念，消除了不确定结果。这提供了一个迭代的增量可变性特定的抽象和细化框架，其中细化仅应用于存在不确定结果的情况，并且重用来自先前迭代的确定结果。
2019-02-14 cs.PL cs.SE
Model-Checking in the Loop Model-Based Testing for Automotive Operating Systems
本文提出MCIL-MBT集成方法，将操作系统规范的模型检查与基于模型的实现一致性测试迭代结合，并在工业应用中发现传统方法遗漏的缺陷。
2023-10-02 cs.SE
Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
本文首次实证研究用于内存安全验证的单元证明，提出结合验证反馈与客观标准的系统化构建方法，并在四个嵌入式操作系统上验证其有效性与成本。
2025-03-17 cs.SE
Checking the HAL Interface Specification Continuously, Right from the Start
University of Freiburg（弗赖堡大学）；Hahn-Schickard Institute（汉-希克哈德研究所）；Offenburg University（奥芬堡大学）
本文提出了一种持续检查HAL接口规范的方法，从开发一开始就进行检查，通过多次迭代开发嵌入式应用程序，确保每个步骤的检查成功。
2025-12-18 cs.LO cs.SE
Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development
Hahn-Schickard Institute（汉-席克哈德研究所）；University of Freiburg（弗赖堡大学）；German Aerospace Center（德国航空航天中心）
本文提出时间HAL-API依赖关系作为形式化方法在嵌入式软件开发中的应用桥梁，通过规范和验证相结合的方法提升正确性保障。
2025-12-14 cs.SE
Model Checking with Program Slicing Based on Variable Dependence Graphs
在嵌入式控制系统中，由于软件复杂性导致例如与时序相关的问题，软件缺陷的潜在风险一直在增加。这些缺陷很少通过测试或模拟发现。为了检测这种缺陷，我们提出了一种建模方法，可以生成软件模型的模型检验与程序切片技术的基础上的变量依赖图。最后将该方法应用于一个汽车控制软件的实例中，验证了该方法的有效性。此外，我们开发了一个软件工具来自动化模型生成，并取得了35%的总验证时间减少模型检验。
2013-01-01 cs.LO cs.SE
Formal Verification of Probabilistic SystemC Models with Statistical Model Checking
SystemC的事务级建模通过提供高级可执行模型在描述嵌入式系统的行为方面非常成功，其中许多模型具有固有的概率行为，例如，随机数据和不可靠的组件。因此，对系统属性的概率进行定量和定性分析至关重要。这种分析可以通过构造被验证系统的形式化模型并使用概率模型检验（PMC）来进行。然而，这种方法是不可行的大型系统，由于状态空间爆炸。在这篇文章中，我们展示了统计模型检验（SMC）的成功使用，直接从大型SystemC模型进行这样的分析，并允许设计人员表达广泛的有用属性。这项工作的第一个贡献是一个框架，以验证属性表示的有界线性时序逻辑（BLTL）的SystemC模型的时间和概率特性。其次，该框架允许用户在BLTL中将丰富的用户代码原语集作为原子命题公开。此外，用户可以定义自己的细粒度时间分辨率，而不是SystemC仿真中的时钟周期边界。第三个贡献是统计模型检查器的实现。它包含一个自动生成的监视器，用于产生执行跟踪的模型验证（MUV），自动仪表化的MUV的机制，和统计模型检验算法的相互作用。
2017-12-04 cs.SE
Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art
属性导向可达性（PDR）是一种基于SAT/SMT的可达性算法，它递增地构造归纳不变量。在成功地应用于硬件模型检验之后，提出了几种适用于软件模型检验的改进方法。我们贡献了一个可复制的和彻底的比较评估的最先进的：我们（1）实现了一个独立的PDR算法，并作为改进，基于PDR的k-induction的不变量生成器，（2）进行了实验研究的最大的公开可用的基准测试集的C验证任务，在其中，我们探索的有效性和效率的软件验证PDR。我们工作的主要贡献是通过提供一个精心设计的参考实现和现有技术的实验评估，为该领域正在进行的研究建立一个可重复的基线。
2020-02-24 cs.SE
Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version)
嵌入式系统的软件开发过程越来越快，这通常会导致相关复杂性的增加。因此，消费电子公司通常在快速和自动验证过程中投入大量资源，以创建强大的系统并降低产品召回率。正因为如此，本文提出了一个简化版本的Qt框架，这是集成到有效的基于SMT的有界模型检验工具，以验证实际应用程序，使用所提到的框架。本文提出的方法提出了一个成功率为94.45%，为开发的测试套件。
2015-09-05 cs.LO cs.SE
Incremental Model Transformations with Triple Graph Grammars for Multi-version Models
本文提出一种基于三重图语法和多版本模型的技术，用于联合转换源模型多版本到目标模型，支持批量转换与增量同步，并通过实证评估证明其在内存和执行时间上的优势。
2023-07-07 cs.SE
Bounded Invariant Checking for Stateflow
状态流模型是复杂的软件模型，通常用作使用Matlab Simulink设计的工业安全关键软件解决方案的一部分。作为安全关键解决方案的一部分，这些模型需要应用严格的验证技术来确保其正确性。在本文中，我们提出了一个基于反驳的形式化验证方法分析Stateflow模型的不变属性，基于有界模型检验（BMC）。我们的技术的关键是：i）状态流模型的状态空间表示为模型的符号配置上的符号转换系统（STS），以及ii）增量BMC的应用程序，在每次展开转换系统的下一个状态关系后生成验证结果。为此，我们开发了一个符号结构操作语义（SSOS）的状态流，从现有的结构操作语义（SOS），并显示两者之间的不变属性的保存。我们将符号配置上STS的有界不变检验定义为可满足性问题。我们开发了一个自动化的程序，用于生成的STS的初始和下一个状态谓词，并在一个工具的形式，利用标准的，现成的可满足性求解器的技术的原型实现。最后，我们提出了初步的性能结果，通过应用我们的工具上的一个说明性的例子和两个工业模型。
2022-09-28 cs.FL cs.SE
Contract Based Program Models for Software Model Checking
本文提出在组件状态转换性质已演绎验证的基础上，利用 flow graphs 低成本构建独立于语言的抽象程序模型，并规划支持 C 语言安全关键嵌入式软件验证的工作流与工具链。
2025-03-14 cs.FL cs.SE
Bounded Invariant Checking for Stateflow Programs
状态流模型是复杂的软件模型，通常用作Matlab Simulink设计的安全关键软件解决方案的一部分。它们包含了通常很难正式验证的设计原则。特别是，标准的详尽的形式化验证技术不太可能很好地扩展工业中开发的复杂设计。此外，Stateflow语言缺乏形式化的语义，这也阻碍了形式化的分析。为了解决这些挑战，我们奠定了一个可扩展的技术的基础，可证明正确的形式分析的Stateflow模型，相对于不变的属性，有界模型检验（BMC）的基础上符号执行。我们的技术的关键是：i）Stateflow模型的状态空间表示为模型的符号配置上的符号转换系统（STS），作为BMC的基础，以及ii）应用增量BMC，在每次展开转换系统的下一个状态关系后生成验证结果。为此，我们开发了一个符号结构操作语义（SSOS）的状态流，从现有的结构操作语义（SOS），并显示两者之间的不变属性的保存。接下来，我们定义了符号配置上STS的有界不变检验作为一个可满足性问题。我们开发了一个自动生成的初始和下一个状态的STS谓词的过程，并提出了一个编码方案的有界不变的检查问题作为一组约束条件，准备自动分析标准，现成的可满足性求解器。最后，我们提出了初步的性能结果，通过应用我们的工具上一个说明性的例子。
2021-11-19 cs.FL cs.SE
A Formal Verification Technique for Architecture-based Embedded Systems in EAST-ADL
随着汽车嵌入式系统等软件密集型系统的复杂性显著增加，开发有质量保证的软件密集型系统是一项日益严峻的挑战。EAST-ADL是一种架构描述语言，旨在在安全关键汽车产品的开发中以多个抽象级别指定汽车嵌入式系统架构。在本文中，我们提出了一个基于架构的验证技术，增强了基于模型的开发过程中支持的EAST-ADL适应模型检查EAST-ADL规范。我们采用UPPAAL作为验证工具，以确保预测的功能行为的模型在EAST-ADL满足功能和实时要求。提出了基于体系结构的验证准则，并推导出符合该准则的转换规则。这使我们能够从EAST-ADL规范中提取相关信息，并生成可分析的UPPAAL模型。定义了EAST-ADL规范的形式化语义，这对EAST-ADL规范的自动验证至关重要。我们的方法是通过验证转向车系统单元的安全性来证明的。
2019-03-14 cs.SE
Formal Verification, Engineering and Business Value
如何将模型检验和静态程序分析等自动化验证技术应用于数百万行嵌入式C/C++代码？如何将这种技术包装成软件开发人员和工程师可以使用的方式，他们可能没有形式化验证的背景？以及如何说服企业经理实际支付这样的软件？这项工作解决了其中一些问题。基于我们自己开发和发布Goanna源代码分析器的经验，我们解释了模型检验，静态分析和SMT解决的底层技术，涉及创建工业证明工具的步骤。
2013-01-01 cs.SE
Multi-Grained Specifications for Distributed System Model Checking and Verification
本文针对复杂分布式系统ZooKeeper的模型检测与验证，提出多粒度规约方法以平衡细粒度规约的状态空间爆炸与粗粒度规约的模型代码差距，成功检测并修复六个严重错误。
2024-09-27 cs.DC cs.SE
BlueCov: Integrating Test Coverage and Model Checking with JBMC
自动化测试用例生成工具帮助企业编写测试，并在进行代码更改时增加高回归测试覆盖率所提供的安全网。测试生成需要覆盖尽可能多的未覆盖代码，同时避免为现有测试套件已经覆盖的代码生成冗余测试。在本文中，我们提出了我们的工作在现实世界中的应用集成形式分析与自动测试用例生成的工具。测试用例的生成是基于使用Java有界模型检查器（JBMC）的覆盖率分析。模型检查器的反例可以转换为具有特定参数的Java方法调用。为了避免生成冗余测试，有必要以与JBMC生成其覆盖目标完全相同的方式测量覆盖率。每个现有的覆盖测量工具使用稍微不同的仪器，因此使用不同的覆盖标准。这使得与基于形式分析的测试用例生成器的集成变得困难。因此，我们开发了BlueCov作为一个特定的运行时覆盖率测量工具，它使用与JBMC完全相同的覆盖率标准。这种方法还允许增量测试用例生成，仅为先前未测试的代码生成测试覆盖率，例如，以完成现有的测试套件。
2022-12-30 cs.PL cs.SE
2LS for Program Analysis
2LS（“tools”）是一个基于CPROVER框架的C程序验证工具。它允许验证用户指定的断言，内存安全属性（例如缓冲区溢出），数值溢出，除以零，内存泄漏和终止属性。分析是通过将验证任务转换为二阶逻辑公式，包括位向量、数组和浮点算术理论来执行的。该公式是解决了一个模块化的组合算法，涉及展开和基于模板的不变合成的帮助下，增量SAT解决。2LS的优点包括其非常快速的增量有界模型检验算法和其灵活的框架，用于试验新的分析和抽象思想的不变推理。缺点是它缺乏对某些程序特性的支持（例如多线程）。
2023-02-05 cs.LO cs.PL cs.SE
Static Analysis using Parameterised Boolean Equation Systems
当将这种技术应用于程序设计语言时，模型检验中众所周知的状态空间爆炸问题甚至更加关键，这主要是由于复杂数据结构的存在。一个最近的和有前途的方法来处理这个问题是一个抽象的和正确的表示，允许在程序模型探索匹配访问状态的全局程序状态的建设。特别是，实现抽象匹配的一个强大方法是为每个程序点用最少量的相关变量填充状态向量。在本文中，我们结合了在飞模型检查方法（增量建设的程序状态空间）和静态分析方法称为影响分析（提取的重要变量为每个程序点），以自动构建一个抽象的匹配功能。首先，我们将问题描述为一个无选择的基于值的μ演算公式，其有效性可以在表示为标记变迁系统（LTS）的程序模型上进行检查。其次，我们将分析转化为局部分辨率的参数化布尔方程系统（PBES），其表示，使一个更有效的建设所产生的抽象匹配功能。最后，我们展示了如何将我们的建议优雅地集成到CADP中，这是一个通用的框架，用于分布式系统的设计和分析以及验证工具的开发。
2006-07-03 cs.SE
Experiences from Large-Scale Model Checking: Verification of a Vehicle Control System
在自动驾驶汽车的时代，嵌入式系统的功能和复杂性正在急剧增加。安全方面变得更加重要，并且要求这样的系统以最高可能水平的容错来操作。模拟和系统测试技术在这方面已经达到了极限。在这里，形式化验证作为一种长期建立的技术可以是一种适当的补充。然而，必要的准备工作，如充分建模系统和指定属性的时态逻辑是微不足道的。在本文中，我们报告我们的经验，应用模型检验，以验证仲裁逻辑的车辆控制系统。我们权衡了不同模型检验技术和工具的利弊，并对我们选择的符号模型检验器NuSMV的原因。我们描述的过程中建模的架构，导致约1500个，69个状态变量和38个LTL约束。为了处理这种大规模的模型，我们自动化和优化的模型检验过程中使用的多核CPU和采用有界模型检验，以避免状态爆炸问题。我们分享我们的经验教训，并为架构师，开发人员和测试工程师提供有价值的见解。
2020-11-20 cs.AR cs.SE cs.SY
Approaches for Software Verification of an Emergency Recovery System for Micro Air Vehicles
本文介绍了微型飞行器的竞争降落伞系统的开发和验证，特别是侧重于嵌入式软件的验证。我们首先介绍了包括系统级故障分析的整体解决方案，然后展示了我们如何最大限度地减少错误软件的影响。本文表明，仔细的抽象和过度近似，整个代码运行在微处理器上可以使用有界模型检验进行验证，这是一个有用的方法，资源受限的嵌入式系统。据我们所知，由此产生的紧急恢复系统是第一个通过形式化验证的紧急恢复系统，而且从操作的角度来看，它优于所有其他现有的解决方案（包括商业上可用的解决方案）。
2017-06-08 cs.SE
Engineering the Hardware/Software Interface for Robotic Platforms - A Comparison of Applied Model Checking with Prolog and Alloy
Chalmers University of Technology（查尔姆斯理工大学）；University of Gothenburg（哥德堡大学）
机器人平台服务于不同的用例，从原型辅助应用的实验到在各个领域实现网络物理系统的嵌入式系统。我们正在使用1：10比例的微型车辆作为机器人平台，在自动驾驶汽车和协作车队领域进行研究。因此，使用不同传感器的实验，例如~超声波、红外线和旋转编码器需要使用我们的车辆平台来准备和实现。对于每个设置，我们需要配置硬件/软件接口板来处理所有传感器和执行器。因此，我们需要为接口板的每个引脚找到一个特定的配置设置，既可以处理我们当前的硬件设置，又足够灵活，可以为未来的用例支持更多的传感器或执行器。在本文中，我们展示了如何建模的硬件/软件接口板的配置空间域，使模型检验解决任务，找到任何，所有，最好的可能的引脚配置。我们提出了一个正式的实验结果，应用声明性语言合金和Prolog来指导工程的硬件/软件接口的机器人平台上的配置复杂性高达10引脚的配置空间大于1450万的可能性的例子的过程。我们的研究结果表明，我们的领域模型在合金相比，Prolog更好地找到可行的解决方案，为更大的配置，平均时间为0.58秒。为了找到最佳解决方案，我们的Prolog模型在最大所需配置下的性能更好，仅需1.38秒;然而，本文中作为示例使用的现有硬件工具目前没有涵盖这个重要的用例。
2014-01-16 cs.RO cs.SE
Rapid Recovery of Program Execution Under Power Failures for Embedded Systems with NVM
电源接通后，从初始状态恢复中断的程序可能会造成负面影响。有些程序甚至无法恢复。为了在掉电情况下快速恢复程序的执行，对于具有NVM的嵌入式系统，在掉电情况下，检查点的执行状态由NVM备份。然而，频繁的检查点将缩短NVM的寿命并导致显著的写入开销。本文提出了一种由函数调用触发的检查点设置技术，以减少对NVM的写操作。测试结果表明，与基于日志的方法和基于步骤的方法相比，堆栈备份的NVM备份大小分别减少了99.8%和80.5$%.为了更好地实现这一点，我们还提出了伪函数调用来增加备份点以降低恢复成本，以及基于指数增量调用的备份方法来降低循环中的备份成本。为了进一步避免NVM上的内容杂乱和脱离NVM，提出了一种清除NVM上无用内容的方法。基于上述问题和技术，提出了故障恢复技术，并通过案例分析了在不同电源故障下如何快速恢复。
2022-09-19 cs.OS cs.SE
