Overview
This research presents MELA, a method designed for synthesizing behavioral models of Cyber-Physical Systems (CPS) by integrating automata learning with statistical machine learning. MELA addresses the challenge of inferring state machine models from system executions that involve numeric time-series data, which is common in CPS, while automata learning typically requires symbolic inputs.
MELA's core functionality involves automatically abstracting raw numeric signals from CPS into interpretable intervals. These intervals are then used as symbolic representations for automata learning algorithms. The approach was evaluated on two distinct CPS: a commercial network intrusion detection system and an industrial autopilot benchmark.
Research Context
Inferring behavioral models from system executions is a critical component for formal verification and analysis of complex, heterogeneous Cyber-Physical Systems. Automata learning offers a mechanism to infer state machine models from these executions. However, a significant challenge arises because CPS inputs and outputs frequently consist of numeric time-series data. Traditional automata learning algorithms, in contrast, operate on inputs defined over a finite symbolic alphabet.
This disparity necessitates an initial abstraction step where raw numeric data must be converted into a finite set of symbols before it can be processed by automata learning algorithms. The research aims to bridge this gap by providing an automated and effective abstraction method.
Approach
MELA is a passive automata learning approach specifically enhanced with machine learning to synthesize behavioral models from numeric time-series data generated by CPS. The methodology systematically combines statistical machine learning techniques with automata learning to achieve its objectives.
A key aspect of MELA's approach is the automatic abstraction of raw numeric signals. This abstraction transforms the continuous numeric data into interpretable intervals. These intervals are specifically designed to be strongly correlated with the system's states, facilitating effective model inference.
The specific techniques employed within MELA for this transformation include:
- Information-theoretic variable selection, which aids in identifying relevant variables from the numeric data.
- Decision-tree-based range abstraction, which is utilized to convert numeric traces into a symbolic representation suitable for subsequent automata learning processes.
The synthesized symbolic representations then serve as inputs for automata learning algorithms to infer the behavioral state machine models.
Findings
MELA was evaluated on two distinct Cyber-Physical Systems:
- A commercial network intrusion detection system developed by RabbitRun Technologies.
- A publicly available industrial autopilot benchmark from the aerospace domain.
The evaluation compared MELA's performance against expertise-based numeric data abstraction methods. The findings indicate the following:
- MELA reduced the number of states and transitions in the learned state machines by an average of 49.20%.
- MELA improved accuracy by an average of 41.71% in the learned state machines.
Furthermore, the learned state machines were found to support system-level requirement verification. They also facilitate practitioners in exploring behaviors that are not explicitly stated in the system requirements.
Potential Applications
The learned state machines generated by MELA have potential applications in:
- System-level requirement verification, assisting in confirming that the system operates according to specified requirements.
- Exploration of system behaviors that may not be explicitly documented in system requirements, providing a deeper understanding of system dynamics for practitioners.
The implementation and experimental data associated with MELA have been made available online for further use and verification.