首页/论文/1111.0370

arXiv 1111.03702011-11-02cs.SEcs.DC

分布式参数和统计模型检验

Distributed Parametric and Statistical Model Checking

Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Marius Mikučionis, Axel Legay

备注：: In Proceedings PDMC 2011, arXiv:1111.0064
发表信息：: EPTCS 72, 2011, pp. 30-42
DOI：: 10.4204/EPTCS.72.4

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

统计模型检验（SMC）是测试和形式化验证之间的折衷。该方法的核心思想是对系统进行一些模拟，并验证它们是否满足某些给定的性质。在本文中，我们表明，SMC是很容易并行化的主/从架构，通过引入一系列的算法，规模几乎线性相对于从计算机的数量。我们的方法已在UPPAAL SMC工具集中实现，并应用于非平凡的案例研究。

英文摘要：

Statistical Model Checking (SMC) is a trade-off between testing and formal verification. The core idea of the approach is to conduct some simulations of the system and verify if they satisfy some given property. In this paper we show that SMC is easily parallelizable on a master/slaves architecture by introducing a series of algorithms that scale almost linearly with respect to the number of slave computers. Our approach has been implemented in the UPPAAL SMC toolset and applied on non-trivial case studies.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

分布式算法和系统的安全性保证：安全性和活性的可靠性检验

Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness

本文提出了一个通用的框架和方法，在一个高层次的分布式算法的完整的编程和检查，在伪代码语言，但精确指定和直接执行，在正式的规约语言和实用的程序设计语言，分别。检查框架，以及分布式算法的编写和它们的安全性和活性属性的规范，使用DistAlgo，一种用于分布式算法的高级语言。我们给出了一个完整的可执行规范的检查框架，一个完整的例子算法和例子的安全性和活性属性。

2020-12-24cs.DCcs.SE

基于领域知识的参数化模型检验

Efficient Parametric Model Checking Using Domain Knowledge

我们介绍了一种有效的参数化模型检验（ePMC）方法的可靠性，性能和其他服务质量（QoS）属性的软件系统的分析。ePMC通过利用软件组件的特定领域建模模式，加快了对软件行为建模的参数马尔可夫链的分析。为此，EPMC预先计算这种模式的关键QoS属性的封闭形式的表达式，并使用这些表达式在整个系统模型的分析。为了评估EPMC，我们表明，它的应用程序基于服务的系统和多层软件架构减少了几个数量级的分析时间相比，目前的参数模型检验方法。

2018-12-24cs.SE

单调抽象技术：从参数化到软件模型检验

Monotonic Abstraction Techniques: from Parametric to Software Model Checking

单调抽象是在参数化分布系统的模型检验中引入的一种技术，用于处理保护中包含全局条件的转换。该技术已被重新解释在声明性的设置在我们以前的论文，并适用于验证容错系统下的所谓的“停止故障”模型。声明性的重新解释包括逻辑技术（量词相对化，特别是量词实例化）在更广泛的背景下有意义。事实上，我们最近表明，这种技术可以过近似阵列加速度，使他们可以作为一个有意义的（和实际有效的）组件CEGAR循环在软件模型检验了。

2014-11-14cs.LOcs.SE

PRESTO：通过参数模型检验预测系统级中断

PRESTO: Predicting System-level Disruptions through Parametric Model Checking

自适应系统有望通过不断调整其配置和行为来减轻中断。这种缓解往往是被动的。通常，环境或内部变化仅在违反系统要求后才会触发系统响应。尽管人们普遍认为，在自我适应方面，预防胜于治疗，但在自我适应系统开发者可用的解决方案中，主动适应方法的代表性不足。为了解决这一差距，我们提出了一个正在进行的方法，通过参数模型检验预测系统级中断（PRESTO）。PRESTO用于自适应系统的MAPE-K（基于共享知识的搜索-分析-规划-执行）反馈控制回路的分析步骤，包括两个阶段。首先，对监测数据进行时间序列分析，以确定个别系统和/或环境参数值的趋势。接下来，未来的非功能性需求违规预测使用参数模型检验，以建立这些趋势对系统的可靠性和性能的潜在影响。我们说明了PRESTO的应用程序中的案例研究，从自治农业领域。

2022-05-07cs.SE

SpinJa模型中的分布式MAP

Distributed MAP in the SpinJa Model Checker

Spin in Java（SpinJa）是Promela建模语言的显式状态模型检查器，也被SPIN模型检查器使用。SpinJa的实现被设计为可扩展和可重用的，它遵循分层的方法，其中每个新层都扩展了前一层的功能。虽然SpinJa初步支持共享内存模型检验，但它还不支持分布式内存模型检验。该工具文件提出了一个分布式实现的最大接受前辈（MAP）搜索算法的SpinJa。

2011-11-02cs.DCcs.SE

分布式系统模型检测与验证的多粒度规约

Multi-Grained Specifications for Distributed System Model Checking and Verification

本文针对复杂分布式系统ZooKeeper的模型检测与验证，提出多粒度规约方法以平衡细粒度规约的状态空间爆炸与粗粒度规约的模型代码差距，成功检测并修复六个严重错误。

2024-09-27cs.DCcs.SE

更多相关论文收起更多论文

云中的分布式CTL模型检验

Distributed CTL Model Checking in the Cloud

最近广泛使用的“大数据”平台要求形式化验证社区更广泛地采用。事实上，形式化验证需要高性能的数据处理软件，用于从来自被分析系统的空前数量的数据中提取知识。由于基于云的计算资源已经变得易于访问，因此验证技术和工具有机会经历深刻的技术转型，以利用新的可用架构。这使得人们对并行化和分布式验证技术越来越感兴趣。在本文中，我们介绍了一种分布式的方法，利用通常使用的技术，由“大数据”社区，使验证的计算树逻辑（CTL）公式非常大的状态空间，使用分布式系统和云计算设施。基准规范上进行的几个测试的结果，从而显示所提出的方法的方便。

2013-10-24cs.DCcs.LOcs.SE

基于遗传编程和模型检验的参数程序综合

Synthesis of Parametric Programs using Genetic Programming and Model Checking

Bar Ilan University（巴伊兰大学）

形式化方法应用基于数学原理的算法来增强系统的可靠性。尝试从验证、模型检验或根据系统的正式规范测试系统到自动构建系统，这是很自然的。经典的算法综合理论提供了有趣的算法，但也令人震惊的高复杂性和不可判定性的结果。结合模型检验和测试，遗传编程的使用提供了一个强大的启发式综合程序。该方法不是完全自动的，因为它由设置规格和参数的用户进行微调。它也不能保证总是成功并收敛到满足所有所需属性的解决方案。然而，我们成功地将其应用于相当重要的示例，并设法找到解决方案，以应对困难的编程挑战，以及改进和纠正代码。我们在这里描述了几个版本的我们的方法合成顺序和并发系统。

2014-02-27cs.AIcs.NEcs.SE

基于模型分割的快速参数化模型检验

Fast Parametric Model Checking through Model Fragmentation

University of York（约克大学）

参数模型检验（PMC）计算表示系统的关键非功能属性（可靠性、性能等）的代数公式。作为系统和环境参数的有理函数。在软件工程中，PMC公式可以在设计期间使用，例如，分析不同系统结构对参数变化的敏感性，或找到最佳系统配置。它们也可以在运行时使用，例如，检查环境变化后是否仍满足非功能性要求，或在环境变化后选择新的配置。然而，当前的PMC技术不能很好地扩展到具有复杂行为和多个参数的系统。我们的论文介绍了一种快速PMC（fPMC）的方法，克服了这一限制，PMC的适用性扩展到更广泛的一类系统比以前可能的。为此，fPMC将PMC处理的马尔可夫模型划分为\emph{fragments}，并对\emph{fragments}的可达性进行独立分析，结合这些片段分析的结果得到PMC可达性公式.为了证明FPMC的有效性，我们展示了我们的FPMC工具可以分析三个系统（取自研究文献，属于不同的应用领域），目前的PMC技术和工具的斗争。

2021-02-02cs.FLcs.ROcs.SE

分布式有界模型检验

Distributed Bounded Model Checking

程序验证是一项耗费大量资源的任务。本文着眼于并行化SMT为基础的自动程序验证，特别是有界模型检查，使其可以分布和执行的机器集群的问题。我们提出了一个算法，动态展开的程序的调用图，并经常分裂它创建子任务，可以并行解决。该算法是自适应的，根据可用资源控制拆分速率，并且还利用来自SMT求解器的信息来拆分搜索中最复杂的地方。我们实现了我们的算法，通过修改CORRAL，微软的静态驱动程序验证器（SDV）使用的验证器，并评估它的一系列硬SDV基准。

2020-05-16cs.PLcs.SE

一种分布式航空电子系统可扩展性分析的建模框架

A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

本文提出了一个分布式综合模块化航空电子（DIMA）系统，由空间分布的ARINC-653模块连接一个统一的AFDX网络的可扩展性分析的建模框架。在UPPAAL中，我们将DIMA系统建模为一组秒表自动机（SWA），分别用经典模型检验（MC）和统计模型检验（SMC）分析其可并行性。该框架的目的是使三种类型的分析：全球SMC，全球MC和成分MC。这允许一种有效的方法，包括（1）使用全局SMC分析的快速可验证性证伪，（2）在简单情况下使用全局MC分析的直接可验证性证明，以及（3）对于更大的状态空间使用组合MC分析的严格可验证性证明。该框架被应用到一个具体的DIMA系统的分析。

2018-03-27cs.DCcs.SE

面向基于Actor的系统的高效线性一致性检查

Efficient Linearizability Checking for Actor-based Systems

针对基于actor的分布式软件正确性验证难的问题，提出DS2框架的线性一致性检查方法，通过对照顺序模型验证子组件、优化调度空间探索算法，可高效发现系统漏洞。

2023-07-19cs.DCcs.MAcs.SE

生物信息学中分布式人工智能系统的验证

Verification of Distributed Artificial Intelligence Systems in Bioinformatics

软件是许多项目的重要推动者，否则这些项目将无法执行。这些项目包括太空探索，天气建模，基因组计划等。帮助这些项目的软件做它被期望做的事情是至关重要的。在软件工程的术语中，符合需求的软件，也就是做了预期要做的事情的软件被称为正确的。软件的正确性检查一直是软件工程领域的研究热点。软件应用领域的从业者通常不重视检查这种正确性。然而，随着软件系统变得越来越大，可能与由不同作者编写的分布式子系统相结合，这种验证变得更加重要。并发分布式系统由于其组件的执行速度不同而容易出现危险的错误，例如死锁、竞争条件或违反项目特定属性。本计画描述一种称为模型检验的静态分析方法，应用于生物资讯学过程的分散式系统验证。在它，我们评估的模型检验方法的效率，以验证组合过程的并发执行的步骤越来越多。我们表明，我们的实验结果符合分析推导的期望。我们还强调了静态分析在生物信息学领域中对组合过程的重要性。

2023-02-09cs.SE

参数、概率、定时资源发现系统

Parametric, Probabilistic, Timed Resource Discovery System

本文提出了一个完全分布式的资源发现和预留系统。这样一个系统的验证是很重要的，以确保在适当的条件下执行一组资源上的分布式应用程序。一个半形式化的模型，他的系统使用概率时间自动机。这个模型是定时的，参数化的和概率的，使它成为一个挑战的参数合成社区。

2016-08-02cs.DCcs.SE

基于SystemC和统计模型检验的控制系统可靠性分析

Dependability Analysis of Control Systems using SystemC and Statistical Model Checking

随机Petri网通常用于分布式系统的建模，以研究其性能和可靠性。本文提出了一种随机Petri网在SystemC中的实现，用于大型嵌入式控制系统的建模。然后利用统计模型检验对所建模型的可靠性进行分析。我们的验证框架允许用户表达广泛的有用的属性进行验证，这是通过案例研究说明。

2016-02-25cs.PFcs.SE

当存在分布式观测时检查有限状态机一致性

Checking Finite State Machine Conformance when there are Distributed Observations

本文关注的是基于状态的系统，它们在物理上分布的接口（称为端口）与环境进行交互。当使用这样的系统时，在每个端口处观察到全局轨迹的投影，称为局部轨迹。这导致环境具有降低的观测能力：所观测到的局部轨迹集不需要唯一地定义所发生的全局轨迹。我们认为以前定义的实现关系$\sqsubseteq_s$和开始调查的问题，定义一个语言${\mathcal {\tilde L}} (M)$的多端口有限状态机（FSM）$M$，$N \sqsubseteq_s M$当且仅当每个全局跟踪$N$是在${\mathcal {\tilde L}} (M)$。其动机是，如果我们能够产生这样一种语言${\mathcal {\tilde L}} (M)$，那么它就有可能用于通知开发和测试。我们证明了${\mathcal {\tilde L}} (M)$可以被唯一地定义，但不需要是正则的。然后，我们证明，它是一般不可判定的是否$N \sqsubseteq_s M$，这个结果的后果是，它是不可判定的，是否有一个测试用例，能够区分两个状态或两个多端口FSM在分布式测试。该结果补充了先前的结果，即是否存在保证区分两个状态或多端口FSM的测试用例是不可判定的。给出了$N \sqsubseteq_s M$可判定的条件.然后，我们考虑的实施关系$\sqsubseteq_s^k$，只涉及输入序列的长度$k$或更少。自然，给定FSM $N…

2011-08-26cs.SE

定价时间自动机网络的随机语义和统计模型检验

Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata

本文提出了一种基于组件竞争的定价时间自动机网络的自然随机语义。语义提供了满足概率加权CTL属性（PWCTL）的基础上，保守地扩展了经典的时间自动机满足TCTL。特别是扩展允许硬实时性能的时间自动机表达在TCTL的性能属性，例如，在概率保证的时间和成本有界的属性。本文的第二个贡献是统计模型检验（SMC）的应用程序，有效地估计正确性的非嵌套PWCTL模型检验问题与所需的置信水平，根据一些独立运行的NPTA。除了应用经典的SMC算法，我们还提供了一个扩展，允许有效地比较性能特性的NPTA在参数设置。第三个贡献是一个有效的工具实现我们的结果和应用程序的几个案例研究。

2014-11-28cs.SE

分布式航空电子系统可扩展性分析的组合方法

A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

这项工作提出了一个组成的分布式集成模块化航空电子（DIMA）系统，包括空间分布的ARINC-653模块连接一个统一的AFDX网络的可扩展性分析的方法。我们在UPPAAL中将DIMA系统建模为一组秒表自动机，通过模型检验验证其可并行性。然而，直接的模型检验是不可行的，由于大的状态空间。因此，我们引入了组合分析，它检查每个分区，包括单独的通信环境。基于消息接口的概念，构建了一些消息发送者自动机来为分区的环境建模。我们定义了一个定时选择模拟关系，它支持复合消息接口的建设。通过使用假设保证推理，我们确保每个任务都满足最后期限，并且通信约束也在全球范围内得到满足。该方法被应用到一个具体的DIMA系统的分析。

2018-06-26cs.FLcs.LOcs.SE

BeSpaceD：分布式软件构件系统空间行为描述与验证的工具框架与方法

BeSpaceD: Towards a Tool Framework and Methodology for the Specification and Verification of Spatial Behavior of Distributed Software Component Systems

在这份报告中，我们提出了一个框架的建模和检查行为的空间分布组件系统的工作。我们的框架的设计目标是能够在一个面向组件的，简单和直观的方式，自动分析和验证系统和集成的可能性与其他建模和验证工具的空间行为建模的能力。我们提出的例子和必要的验证步骤，以证明属性，如范围覆盖或组件和技术细节之间的冲突的情况下。

2014-04-14cs.SE

基于统计模型检验的软件生产线概率模型定量分析

Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking

我们调查的统计模型检验技术分析软件产品线模型的定量属性与概率方面的适用性。为此，我们丰富了面向功能的语言FLan的动作率，它指定的可能性表现出特定的行为或安装功能在特定的时刻或以特定的顺序。丰富的语言（称为PFLan），使我们能够指定模型的软件产品线的概率配置和行为，例如，通过考虑基于离散时间马尔可夫链的PFLan语义。PFLan的Maude实现与分布式统计模型检查器MultiVeStA相结合，对一个简单的产品线案例研究进行定量分析。所提出的分析包括某些感兴趣的行为（例如产品故障）的可能性和产品的预期平均成本。

2015-04-14cs.LOcs.SE