利用简单初等语言和计时增广前缀接受器通过SMT挖掘DTA

中文摘要 AI 辅助

计时自动机通过引入时钟变量扩展了有限状态自动机，是描述和分析实时系统计时行为的流行形式化方法。提取黑盒安全关键系统的计时行为对于设计和分析其实时需求至关重要，但这仍然具有挑战性。在本文中，我们通过生成与给定系统行为集（包括正例和负例）一致的确定性计时自动机（DTA）来解决此问题。为此，我们改进了简单初等语言（sEL）的形式化，并引入了计时增广前缀树接受器（tAPTA）。我们的方法如下：首先，我们通过将样本转换为sEL来预处理样本，这可以丢弃冗余并检测冲突；然后，我们将生成的sEL重写为增量形式，并构建tAPTA以进一步简化样本；最后，我们将搜索接受简化tAPTA的DTA编码为SMT公式。我们在随机生成的基准测试和一个调度案例研究上评估了我们的方法。结果表明，我们的简化方法在减少编码SMT公式大小方面的有效性，以及我们的方法在挖掘DTA方面的效率。

英文摘要

Timed automata, which extend finite state automata by introducing clock variables, serve as a popular formalism for specifying and analyzing the timed behaviors of real-time systems. Extracting the timed behaviors of a black-box, safety-critical system is crucial for designing and analyzing its real-time requirements, yet it remains challenging. In this paper, we address this problem by generating a deterministic timed automaton (DTA) consistent with a given set of system behaviors, comprising both positive and negative examples. To this end, we adapt the formalism of simple elementary languages (sEL) and introduce the timed augmented prefix tree acceptor (tAPTA). Our approach proceeds as follows: First, we preprocess samples by translating them into sEL, which discards redundancy and detects conflicts; then, we rewrite the resulting sELs in an incremental form and construct a tAPTA to further simplify the samples; finally, we encode the search for a DTA that accepts the simplified tAPTA as an SMT formula. We evaluate our approach on randomly generated benchmarks and a scheduling case study. The results demonstrate the effectiveness of our simplification method in reducing the size of the encoded SMT formula and the efficiency of our approach in mining a DTA.

发表机构

• Key Lab. of System Software (Chinese Academy of Sciences), Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences（中国科学院软件研究所系统软件重点实验室 & 中国科学院大学）
• National Key Lab. of Space Integrated Information System, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences（中国科学院软件研究所空间信息系统全国重点实验室 & 中国科学院大学）
• MoE Key Lab. of High Confidence Software Technologies, School of Computer Science, Peking University & Zhongguancun Laboratory（北京大学计算机学院教育部高可信软件工程技术与系统重点实验室 & 中关村实验室）

机构由 AI 辅助整理，请以论文原文为准。