arXiv subjects

Patricio Saavedra

Publications and source records attributed to Patricio Saavedra.

3 recordsLinked to original sources

arXiv2026

Synthesizing Behavioural Models of CPS Using Automata Learning and Statistical Machine Learning

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.

cs.SE↗

arXiv2024

Enhancing Automata Learning with Statistical Machine Learning: A Network Security Case Study

Intrusion detection systems are crucial for network security. Verification of these systems is complicated by various factors, including the heterogeneity of network platforms and the continuously changing landscape of cyber threats. In this paper, we use automata learning to derive state machines from network-traffic data with the objective of supporting behavioural verification of intrusion detection systems. The most innovative aspect of our work is addressing the inability to directly apply existing automata learning techniques to network-traffic data due to the numeric nature of such data. Specifically, we use interpretable machine learning (ML) to partition numeric ranges into intervals that strongly correlate with a system's decisions regarding intrusion detection. These intervals are subsequently used to abstract numeric ranges before automata learning. We apply our ML-enhanced automata learning approach to a commercial network intrusion detection system developed by our industry partner, RabbitRun Technologies. Our approach results in an average 67.5% reduction in the number of states and transitions of the learned state machines, while achieving an average 28% improvement in accuracy compared to using expertise-based numeric data abstraction. Furthermore, the resulting state machines help practitioners in verifying system-level security requirements and exploring previously unknown system behaviours through model checking and temporal query checking. We make our implementation and experimental data available online.

cs.CR↗

arXiv2023

Learning Non-robustness using Simulation-based Testing: a Network Traffic-shaping Case Study

An input to a system reveals a non-robust behaviour when, by making a small change in the input, the output of the system changes from acceptable (passing) to unacceptable (failing) or vice versa. Identifying inputs that lead to non-robust behaviours is important for many types of systems, e.g., cyber-physical and network systems, whose inputs are prone to perturbations. In this paper, we propose an approach that combines simulation-based testing with regression tree models to generate value ranges for inputs in response to which a system is likely to exhibit non-robust behaviours. We apply our approach to a network traffic-shaping system (NTSS) -- a novel case study from the network domain. In this case study, developed and conducted in collaboration with a network solutions provider, RabbitRun Technologies, input ranges that lead to non-robustness are of interest as a way to identify and mitigate network quality-of-service issues. We demonstrate that our approach accurately characterizes non-robust test inputs of NTSS by achieving a precision of 84% and a recall of 100%, significantly outperforming a standard baseline. In addition, we show that there is no statistically significant difference between the results obtained from our simulated testbed and a hardware testbed with identical configurations. Finally we describe lessons learned from our industrial collaboration, offering insights about how simulation helps discover unknown and undocumented behaviours as well as a new perspective on using non-robustness as a measure for system re-configuration.

cs.SE↗