Over the last decades, the advancements in microelectronic technologies allowed for the embedding of complex digital sensors in several systems, ranging from home appliances to health tracking devices and industrial plant machinery. The resulting systems are, in general, quite complex, given the possible heterogeneity of their components and the non-trivial ways in which sensors may interact. In critical domains, formal methods have been employed to ensure the correct behaviour of a system. However, a complete specification of all the properties that have to be guaranteed turns out to be often out of reach, due to the inherent complexity of the system and of its interactions with the environment in which it operates. To overcome these limitations, some approaches that complement formal verification with model-based testing and monitoring have been recently proposed. In this paper, we argue for the opportunity of pairing monitoring with machine learning techniques in order to improve its ability of detecting critical system behaviours.
Over the last decades, thanks to new microelectronic technologies, even the simplest measuring devices
have progressively evolved into complex digital systems capable of performing several processing and
communication operations related to the measured values (smart sensors). A smart sensor can be defined
as a device that takes its input from the physical environment and uses built-in computational resources
to perform some predefined functions upon detection of specific input, thus processing data before passing
them on [
In such a complex environment, formal methods can be exploited to devise methods and techniques for
the automated verification of software and hardware systems, a task which is of paramount importance
in many critical domains. However, the inherent complexity of the systems and the non-trivial ways in
which their components may interact among themselves and with the environment, make it very difficult
(and sometimes impossible) to specify in advance all the relevant properties that have to be guaranteed
(or, dually, avoided). To overcome these limitations, some approaches that complement formal verification
with model-based testing and monitoring have been recently proposed in the literature (see, for instance,
[
In this contribution, we focus our attention on monitoring, a runtime verification technique which is gaining more and more attention within the formal method and verification community. We outline a novel framework for online system verification that integrates monitoring with machine learning and can be applied in anomaly detection and predictive maintenance tasks. As we shall see, the proposed approach allows a domain expert to start with the specification of the most important and natural properties to monitor. Then, the framework autonomously discovers new relevant properties by means of an iterative refinement process, becoming capable, over time, of identifying undesired behaviours in advance, with a considerably higher level of detail and coverage than the original specification.
This extended abstract is organized as follows. Section 2 provides a short introduction to the concept of system monitoring. Section 3 deals with machine learning and, specifically, with pattern mining techniques that may be used to analyze system traces to extract relevant properties. In section 4, we envision a framework that combines system monitoring and machine learning. A short recap of the distinctive features of the proposed approach concludes the extended abstract. 2
Monitoring [
Classic, static techniques, such as, for instance, model checking [
Even though monitoring has been mostly studied in the setting of linear time temporal logics [
The basic principles on which monitors (and the theory of monitorability) are built are the ability of reaching a verdict by just observing a finite prefix of a single execution trace (a finite trace) and the fact that, once a verdict is reached, it is irrevocable, as it is a guarantee that the system satisfies or violates the property, independently from all the other possible (unobserved) behaviours it might exhibit. This latter feature ensures the soundness of a monitor. We introduce and discuss the notion of completeness of a monitor below.
We say that a property is positively monitorable if every system satisfying it features a finite trace that witnesses the satisfaction; conversely, we say that a property is negatively monitorable if every system violating it features a finite trace that witnesses the violation. A monitorable property is a property that is either positively or negatively monitorable.
Safety properties are negatively monitorable, as their violation is witnessed by a finite trace. Dually, co-safety properties are positively monitorable. On the other hand, there exist properties like it is possible to reach a success state, but it is not possible to reach it in less than 3 steps which are neither positively nor negatively monitorable. A monitor observing a system execution trace that is compatible with the property, e.g., a success state is reached at the third execution step, indeed, cannot issue a satisfaction verdict, thus stating that the property is fulfilled by every run, as there might be a run along which a success state is reached in less than 3 steps. Moreover, a system might violate the property by never reaching a success state at all; in this case, no finite trace witnesses the violation, as the success state might be reached at the next step, or through a completely different run. Instead, the property
it is not possible to reach a success state in less than 3 steps is negatively monitorable, as every system violating it features a finite trace that reaches a success state in less than 3 steps.
Given a positively (resp., negatively) monitorable property P , we say that a monitor is satisfactioncomplete (resp., violation-complete) for P if every system satisfying P features a finite trace that is accepted (resp., rejected) by the monitor.
It is clear that sound and complete monitors only exist for monitorable properties. Thus, characterizing
the set of monitorable properties is one of the major challenges in the field. However, some work has
also been done in the attempt of weakening the notion of monitorability (see [
Machine learning (ML) is an area of Artificial Intelligence (AI) that focuses on algorithms and statistical models that have the ability to automatically learn (and improve their behaviour) from experience without being explicitly programmed. In particular, in supervised machine learning, the goal is that of building a model capable of mapping a given input to a desired output. Depending on the kind of output to generate, it is possible to distinguish between regression and classification tasks, characterized by numerical and categorical (classes) values, respectively.
In order to learn a model, a machine learning algorithm undergoes a so-called training phase, during which several examples (or instances) of the concept that has to be learnt are taken into consideration. For each considered instance, both the input and the output variables are known. Once the model has been built, it can be applied to new instances, for which only the input variables are known, in order to predict the output values.
Among supervised learning tasks, in this work we are mainly interested in pattern mining. In such a setting, the input consists of a sequence of numerical (time series) or categorical (e.g., sequences of system states) values, whereas the output is, typically, categorical. The goal is to extract a set of relevant patterns from the input sequences, that characterize (and make it possible to distinguish among) instances belonging to different classes.
Patterns can be of different kinds. For lists of categorical values, frequent patterns have been investigated
(see, for instance, [
As for a more formal characterization of a pattern, the task of learning temporal logic formulas from
examples is attracting an increasing interest. For instance, a decision tree learning algorithm which is
capable of generating interval temporal logic formulas from sequences of categorical values, in order to
perform a classification task, is described in [
As it is emerging from the most recent literature in the field, machine and statistical learning solutions
can be successfully combined with formal methods techniques to deal with complex real-world problems
[
Specification of the initial set of properties. Domain experts are asked to specify the most significant properties that the system under consideration should exhibit. These properties are then formalized in a suitable temporal logic and a monitor that checks them against execution traces is synthesized (obviously, monitorability of the relevant formulas is a critical issue here). Monitoring of system properties. The monitor checks whether the system satisfies/violates the considered properties during its execution (monitoring).
Detection of a failure. Traces for which the monitor reaches a verdict of failure are collected. These are considered to be failure traces. In addition, traces generated by the system during previous normal behaviour are extracted, and considered to be normal traces. Of course, the length of the time window that is used to extract failure traces depends on the specific application domain, and it must be carefully chosen according to the results of a dedicated tuning phase, possibly with the help of domain experts. Mining of the relevant behaviour patterns. Failure and normal traces are put together to generate a dataset for supervised machine learning. Each instance is characterized by a trace that can be numerical (as in the case of a temperature signal) or categorical (this is the case, for instance, with a sequence of system calls made in a Unix system). Moreover, each instance is labeled with a binary class, that can be either failure or normal behaviour. Pattern mining algorithms are run on the dataset, with the goal of extracting the (temporal) logic formulas that best characterize and discriminate between the two classes. Extension of the pool of properties. The (temporal) logic formulas extracted during the mining phase are added to the monitoring pool of properties (possibly after their transformation into safety properties), and the process restarts from the monitoring phase.
As it can be observed, the proposed framework works in an iterative way. It starts from a set of basic properties, and new ones are then added over time. The discovered logical properties are closely related to the original ones and, in principle, they should allow the system to discover anomalous behaviours earlier and with ever increasing accuracy and coverage. 5
Thanks to the new microelectronic technology advancements, measuring devices can now be easily transformed into complex digital systems capable of processing data, and of interacting with one another and with the surrounding environment. As a result, their emerging behaviour is typically non trivial, and difficult to formalize into a set of logical properties to be used for standard system verification, even for a pool of domain experts. For such a reason, approaches that complement formal verification with model-based testing and monitoring have been recently investigated in the literature.
In this work, we outlined a possible solution to such a problem which integrates machine learning and monitoring techniques. The proposed formal verification framework starts with the runtime verification of the most important and natural properties that should be guaranteed during the execution of the analyzed system. Then, it autonomously discovers new ones in an iterative way, becoming capable of identifying unwanted behaviours earlier, and with ever higher detail and coverage than the original specification. In the long run, the verification tool is expected to gain the ability of performing advanced tasks such as self-diagnosis, predictive maintenance, adaptation, and robustness enhancement.
A practical implementation of the system introduced here in the context of a real-world scenario represents a natural development of the present work. [18] S. Nihtianov and A. Luque. Smart Sensors and MEMS: Intelligent Sensing Devices and Microsystems for Industrial Applications. Woodhead Publishing, 2018.