Parametric Timed Model Checking Benchmark Library

Parametric Timed Model Checking Benchmark Library是由法国巴黎第十三大学LIPN实验室创建的数据集，旨在为参数化定时模型检查提供基准测试。该数据集包含34个基准，涵盖学术和工业案例，以及现有技术无法解决的示例。数据集内容丰富，包括硬件异步电路、通信协议、实时系统等领域的模型。创建过程中，数据集聚焦于参数化定时模型，支持多种类型的属性分析。应用领域广泛，旨在解决实时系统中的硬时序约束和并发性验证问题。

The Parametric Timed Model Checking Benchmark Library was developed by the LIPN Laboratory at Paris 13 University, France, aiming to provide benchmark resources for parametric timed model checking. This library includes 34 benchmarks covering academic and industrial cases, as well as examples that cannot be solved by state-of-the-art technologies. The dataset has rich content, comprising models from fields such as hardware asynchronous circuits, communication protocols, and real-time systems. During its development, the library focuses on parametric timed models and supports analysis of multiple types of properties. It has a wide range of application scenarios, targeting the verification of hard timing constraints and concurrency issues in real-time systems.

搜集汇总

数据集介绍

构建方式

该基准测试库的构建源于对参数化时间模型检测领域日益增长的公平比较需求。研究者从多年积累的学术论文与工业合作中系统收集案例，涵盖学术基准、工业案例以及当前技术无法求解的典型示例。所有模型均以IMITATOR输入格式呈现，并遵循GNU通用公共许可证进行分发，确保开放性与可复现性。

使用方法

用户可通过在线网页访问分类列表，选取特定基准后，针对同一模型的不同属性（如安全性、可达性、鲁棒性）进行参数合成。例如，Fischer互斥协议可分别用于安全性合成或给定参数估值下的鲁棒性评估。库中部分示例虽超时但可输出部分结果，或通过手工计算获得解，鼓励新算法的发展。

背景与挑战

背景概述

在实时系统验证领域，硬时序约束与并发行为的严格保障已成为工业标准（如DO-178C）的核心要求。参数化时间模型检测作为一种前沿形式化方法，能够在设计阶段处理未知或不确定的时序常数（如周期的不精确性），从而显著扩展了传统模型检测的适用范围。然而，随着近年来基于SMT、整数凸包抽象、机器学习等多种新型分析技术的涌现，公平比较这些工具效率的标准化基准库却长期缺位。为填补这一空白，Étienne André等研究者于2018年发布了参数化时间模型检测基准库，该库由巴黎第十三大学等机构联合创建，系统收集了34个基准案例、80种模型及122项性质，涵盖学术协议（如Fischer互斥协议）、工业案例（如Thales FMTV挑战）及公认的不可解示例，为领域内算法性能的客观评估奠定了关键基础。

当前挑战

该基准库面临的核心挑战源于参数化时间自动机（PTA）理论的高度不可判定性。具体而言，全类PTA的参数综合问题已被证明不可判定，尽管L/U-PTA等子类具备单调性并享有部分可判定结果，但实际工业模型（如含stopwatches或共享变量的系统）往往突破这些受限子类的边界。此外，构建过程遭遇多重困难：首先，基准需覆盖从学术玩具到工业复杂系统的广泛领域，但工业案例（如SIMOP、SPSMALL）中参数数量与状态空间的爆炸性增长导致现有工具在300秒内超时；其次，部分案例（如toy:1/n）虽可人工求解，却因缺乏自动化算法而成为‘人类可解但工具无解’的典型；最后，多属性验证（如可达性、最优性、鲁棒性）的异构需求，以及不同工具输入格式的转换损失（如Uppaal不支持参数），进一步加剧了基准的可移植性与可比性挑战。

常用场景

经典使用场景

在实时系统的形式化验证领域，Parametric Timed Model Checking Benchmark Library 被广泛用于评估和比较各类参数化时间模型检测工具的性能与能力。该库汇集了从学术论文与工业合作中积累的数十个基准案例，涵盖硬件异步电路、通信协议、互斥协议、实时调度问题以及参数化时间模式匹配等多元领域。研究者借助这些精心设计的模型，能够系统地测试工具在处理参数化时间自动机时的效率、可扩展性及对复杂属性（如可达性、最优性、不可避免性与鲁棒性）的求解能力。例如，Fischer互斥协议与CSMA/CD协议等经典案例，为验证算法在安全性与可达性合成方面的表现提供了标准化的测试平台。

解决学术问题

该数据集有效应对了参数化时间模型检测领域长期存在的基准缺失与公平比较难题。在缺乏统一基准库的背景下，不同工具与算法之间的性能评估往往依赖零散且不可复现的案例，难以客观衡量新技术的进步。该库通过提供公开、稳定且分类明确的基准，解决了学术研究中工具对比的标准化问题，促进了SMT求解、整数抽象、分布式验证及机器学习等新兴技术在参数化时间自动机分析中的发展。此外，库中收录了若干当前技术无法自动求解的困难实例，激励研究者探索更强大的算法，从而推动了参数化时间模型检测理论边界的拓展。

实际应用

在实际工业应用中，该基准库为嵌入式系统、航空航天电子及汽车控制等对时间约束极度敏感的领域提供了关键支撑。例如，Thales公司的FMTV挑战案例与汽车系统模型，展示了参数化时间模型检测在系统设计早期阶段处理未知时序常数或不确定性（如周期波动）时的实用价值。通过该库提供的工业级案例，工程师能够验证系统在不同参数配置下的行为是否满足安全性与实时性要求，从而在设计阶段规避潜在缺陷。此外，参数化时间模式匹配基准（如加速计与齿轮箱案例）使离线日志分析成为可能，帮助工业界在系统运行后追溯异常事件的时间模式。

数据集最近研究

最新研究方向

在实时系统验证领域，参数化时间模型检测因能够处理未知时序常数与不确定性而备受关注。Parametric Timed Model Checking Benchmark Library的建立填补了该领域缺乏统一基准的空白，为评估新兴技术如基于SMT的求解、整数壳抽象、机器学习驱动的参数合成等提供了标准化平台。该库涵盖学术协议、工业案例及经典难解实例，尤其聚焦于L/U-PTA等可判子类的边界探索与鲁棒性分析，推动了对参数化时间自动机中可达性、最优性与不可避免性等核心问题的算法突破。这一基准库的发布不仅促进了工具间的公平比较，更催化了分布式验证与模式匹配等前沿方向的发展，对航空航天等高可靠性系统的形式化验证具有深远意义。

相关研究论文

• A benchmark library for parametric timed model checking

  法国巴黎第十三大学，LIPN，CNRS，UMR 7030，法国维勒塔讷斯 · 2018年