AI 中文总结
研究针对CPS数值时间序列数据难以直接用自动机学习建模的问题，提出结合机器学习的MELA方法，经实验验证其可减少状态机规模并提升准确率，支持系统级需求验证。
AI 中文摘要
从系统执行中推断行为模型对支持复杂异构网络物理系统（CPS）的形式化验证与分析至关重要。自动机学习提供了从系统执行中推断状态机模型的有效方法，但CPS的输入输出通常包含数值时间序列数据，而自动机学习算法假设输入来自有限符号字母表，因此原始数值数据必须先抽象为有限符号集。本文提出MELA，一种结合机器学习的被动自动机学习方法，用于从CPS生成的数值时间序列数据中合成行为模型。MELA将统计机器学习与自动机学习系统结合，自动将原始数值信号抽象为与系统状态强相关的可解释区间，具体采用信息论变量选择和基于决策树的范围抽象，将数值轨迹转换为适合自动机学习的符号表示。我们在两个CPS上评估MELA：工业合作伙伴RabbitRun Technologies开发的商用网络入侵检测系统，以及航空领域公开的工业自动驾驶基准。与基于专业知识的数值数据抽象相比，MELA使所学状态机的状态和转移数量平均减少49.20%，同时准确率平均提升41.71%。此外，所学状态机支持系统级需求验证，帮助从业者探索系统需求中未明确的行为。我们将实现代码和实验数据公开在线。
英文摘要
Inferring behavioural models from system executions is essential for supporting formal verification and analysis of complex, heterogeneous cyber-physical systems (CPS). Automata learning provides an effective way to infer state machine models from system executions. However, CPS inputs and outputs often consist of numeric time-series data, while automata learning algorithms assume inputs over a finite symbolic alphabet. As a result, raw numeric data must first be abstracted into a finite set of symbols. In this article, we present MELA, a passive automata learning approach enhanced with machine learning to synthesize behavioural models from numeric time-series data generated by CPS. MELA systematically combines statistical machine learning with automata learning to automatically abstract raw numeric signals into interpretable intervals that are strongly correlated with system states. Specifically, MELA uses information-theoretic variable selection and decision-tree-based range abstraction to transform numeric traces into symbolic representations suitable for automata learning. We evaluate MELA on two CPS: a commercial network intrusion detection system developed by our industry partner, RabbitRun Technologies, and a publicly available industrial autopilot benchmark from the aerospace domain. Compared with expertise-based numeric data abstraction, MELA reduces the number of states and transitions in the learned state machines by 49.20% on average, while improving accuracy by 41.71% on average. Furthermore, the learned state machines support system-level requirement verification and help practitioners explore behaviours that are not explicit in the system requirements. We make our implementation and experimental data available online. Keywords: Automata learning, Cyber-physical systems, Behavioural model synthesis, Decision trees, Model checking, Intrusion detection, Simulink.
CommentsThis paper has been accepted for publication in the Automated Software Engineering journal
