Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm

This is the artifact for paper "Automated Verification for Real-Time Systems

via Implicit Clocks and an Extended Antimirov Algorithm"

Our benchmark contains three folders:

- Validation: We manually annotate TimEffs specifications for a set of synthetic examples (for about 54 programs), to test the main contributions, including: computing effects from symbolic timed programs written in C t ; and the inclusion checking for TimEffs with the parallel composition, blok waiting operator and shared global variables.

- Experiment1: For 16 C^t programs8, and the annotated temporal specifications are in a 1:1 ratio for succeeded/failed cases. We record the evaluation

results in Table 3 in the paper

- Experiment12: comparison with the PAT [16] model checker using real-life Fischer’s mutual exclusion algorithm.

本数据集为论文《基于隐时钟与扩展Antimirov算法的实时系统自动化验证》的配套实验工件。本基准测试集包含三个子文件夹：
- 验证集（Validation）：我们针对约54个合成示例程序手动标注了TimEffs规范，用于验证本文的核心贡献，涵盖两大内容：一是从C^t语言编写的符号化实时程序中计算行为效应；二是针对支持并行组合、阻塞等待算子与共享全局变量的TimEffs开展包含性检查。
- 实验1（Experiment1）：针对16个C^t程序，我们为成功与失败用例按1:1的比例标注了时序规范，相关评测结果已收录于论文的表3中。
- 实验12（Experiment12）：采用实际应用中的Fischer互斥算法，与PAT模型检查器（PAT [16]）开展对比实验。