Runtime Veri cation is a lightweight formal veri cation technique used to verify the runtime behaviour of software (resp. hardware) systems. Given a formal property, one or more monitors are synthesised to verify the latter against a system execution. A monitor can only conclude the violation of a property when it observes such a violation. Unfortunately, in safety-critical scenarios, this might happen too late for the system to react properly. In such scenarios, it is advised to use Predictive Runtime Veri cation, where monitors are capable of anticipating (by using a model of the system) future events before actually observing them. In this work, instead of assuming such a model is given, we describe a runtime veri cation work ow where the model is learnt and incrementally re ned by using process mining techniques. We present the approach and the resulting prototype tool.
Runtime Veri cation (RV) [7] is a kind of formal veri cation technique that focuses on checking the behaviour of software/hardware systems. With respect to other formal veri cation techniques, such as Model Checking [11] and Theorem Provers [18], RV is considered more dynamic and lightweight. This is mainly due to its being completely focused on checking how the system behaves, while the latter is currently running. This is important from a complexity perspective. RV does not need to simulate the system in order to check all possible execution scenarios; but, it only analyses what the system produces (i.e., everything that can be observed of the system). This is usually obtained through monitors, that are nothing more than validation engines which, given a trace of events generated by the system execution, conclude the satisfaction (resp. violation) of a formal property of interest. In turn, a formal property is the formal representation of how we expect the system should behave. The monitor's job is to verify at runtime whether such a property holds.
Since monitors are usually deployed together with the system under analysis, they are well suited for checking properties that require to be continuously monitored. This is especially true in safety-critical scenarios, where a system's ? Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0). fault can cause injuries, loss of money and even deaths. A key example is autonomous and robotic systems, where reliability is vital [12], and the addition of monitors ensuring a correct behaviour is a valuable feature. Nonetheless, even though monitors are lightweight components, they are still an additional workload for the system. This is not a problem for large systems, but it might be for smaller ones, such embedded systems; where the amount of available resources can be limited. For both increasing reliability and reducing the impact of the monitors on the system, an extension of standard RV named Predictive Runtime Veri cation (PRV) has been proposed e.g. in [31]. As the name suggests, PRV di ers from RV because it does not only consider the events observed by the system execution, but it also tries to predict future events. By predicting future events, the resulting monitors are capable of concluding the veri cation sooner. Indeed, since these monitors can predict how the system is going to behave in the future, they can reduce the search space of possible future continuations and, hypothetically, conclude the satisfaction (resp. violation) by analysing shorter traces of events (w.r.t. the standard counterpart). By concluding earlier, predictive monitors are a good choice: (i) for improving reliability in safety-critical scenarios, since the monitors can conclude a violation of a property before such a violation has even been observed; (ii) for reducing the workload introduced by the monitor, since the monitor can conclude the satisfaction (resp. violation) of the property sooner, it can be removed from the system and its resources can be reclaimed for other purposes.
The problem with PRV is that it requires additional knowledge on the system in order to predict future events. Usually, this is represented through an abstraction, the model, which is manually created by an expert of the system. The problem with this approach is that such a model is not always available, and even when it is, it might not be speci ed in a convenient way (e.g. wrong formalism). One possible way to avoid errors due to human intervention in the model generation step is to resort once again to observations collected at runtime. The guiding principle here is to learn the model behavior by observing real execution traces so as to create a sort of closed loop in which logs are used to adjust the candidate models, models are used to predict faults with certain con dence level, the con dence level increases with the log size, etc.
For this purpose, in this paper we present an initial study on how to use Process Mining (PM) to automate the model generation phase in practical applications of PRV. PM is a rich research area which consists in { but is not limited to { studying and developing automated techniques to synthesise models from log les. Speci cally, we focus on the branch of PM called Process Discovery. We show how it can be applied in the context of PRV, and we present the updated veri cation work ow; where, starting from a set of log les generated by the system execution, we obtain a model that can be used to predict events for the monitor. We also show how the resulting approach can be used to obtain incrementally predictive monitors, where more the monitors are used to verify the system and more they improve at predicting future events, and thus, at concluding the satisfaction (resp. violation) of the analysed property.
It is important to remark that, to avoid human intervention in the model generation phase, the proposed approach has an empirical nature by construction since it always works with partial information on the entire set of possible system behaviours. In theory, a precise model of the system can be obtained only as the limit of a sequence of possible inaccurate candidate models. For this reason, our validation procedure returns truth values enriched with con dence scores that depend on the frequency of observed events applied during the PM preprocessing phase.
The remainder of this paper is structured as follows. Section 2 presents the preliminary notions of RV, PRV and PM. Section 3 shows our general veri cation work ow without selecting any speci c formalism for properties and models. Section 3.1 instantiates our work ow with the most used formalisms in formal veri cation. Section 4 presents the prototype tool representing the implementation of our approach. Section 5 positions this contribution with respect to the state of the art. Finally, Section 6 summarises the results of this work and points out to future directions. 2 2.1
Runtime Veri cation and Predictive Runtime Veri cation A system is denoted by S, and its alphabet (all of its observable events) is denoted by S (or where there is no confusion). Given an alphabet, , a trace, , is a sequence of events in , and tr( ) is the set of all possible traces (the language) over . Properties are denoted by ', potentially with subscripts, and ' denotes their negation. Given an alphabet , a property ' is satis ed by a trace over , written j= ', if ' is true in . The set J'K = f j j= 'g contains the set of traces satisfying ', and we denote that a particular trace satis es a property ' as 2 J'K. A property ' can be speci ed in any formalism such that for a given alphabet , and for any trace 2 tr( ), the following two conditions hold:
2 J'K ()
2= J'K
(
Condition (
De nition 1 (Monitor). Let S be a system with alphabet , and ' be a property. Then, a monitor for ' is a function M on' : tr( ) ! B3, where B3 = f>; ?; ?g:
M on'( ) = 8 >< >
? >: ?
Intuitively, a monitor returns > if all continuations of satisfy '; ? if all possible continuations of violate '; ? otherwise.
De nition 1 describes a generic monitor that does not impose constraints on the formalism used. Consequently, we collapse the de nition of tr( ) for representing nite and in nite traces depending on what is supported by the formalism that is used to de ne '. Thus, if ' accepts only traces of in nite length, then tr( ) = !; if ' accepts only traces of nite length, then tr( ) = ; otherwise, tr( ) = [ !.
Let S be a system with alphabet . We denote its model by , and use J K tr( ) to indicate the set of traces recognised by (i.e., represents a formal abstraction of how S behaves). A model, , can be speci ed in any formalism such that for a given alphabet, , for any trace, 2 tr( ), and for any property, ', the following holds:
(
Often, PRV frameworks express their properties in Linear-time Temporal Logic (LTL) [22] (for example [17,31]); however, we took our inspiration from a PRV framework where both the System Under Analysis (SUA) and property are de ned using Timed Automata (TA) [21]. The reason is that in works such as [17,31], the predictive aspect is not formalised through a model of the system, but as a set of nite su xes. These su xes are then concatenated to the given trace allowing the monitor to predict the initial part of the possible continuations u. Instead, in our work, as in [21], we explicitly represent the model without focusing only on the rst events after , but by applying the prediction to the entire possible continuation. This can be obtained using a model of the system as input to the monitor, alongside the property to be veri ed. Informally, the model generates the set of event traces that can be observed by executing the system. We follow the de nition of a predictive monitor from [21], however, in this paper we remain formalism-agnostic.
De nition 2 (Predictive Monitor). Let S be a system with alphabet , model and let ' be a property. A predictive monitor for ' given is a function, M on'; : tr( ) ! B3, where B3 = f>; ?; ?g:
M on'; ( ) = <> >
? >: ? 8 The intuitive meaning of the return values is the same as in the non-predictive case (De nition 1). Note the use in the de nition. For instance, the case for > requires all traces u not to be in J'K \ J K where ' represents the negation of '. Process Mining (PM) [26] is a technique used in software engineering to automatically synthesise a formal model which denotes the system behaviour. Such analysis is usually performed on event logs generated by multiple executions of the system.
In practice, by using data mining algorithms, knowledge is extracted by these logs and corresponding formal models are generated. These models represent an abstraction of the system, and can be used to understand how the system behaves. Usually, once such models are extracted, an expert of the system can use them to study and check whether the implemented system actually meets his/her expectations. This check can be manually performed by the expert, who inspects the extracted model and searches for inconsistencies, or it can be automatically performed through conformance checking algorithms.
The power of PM lies in its being exible, customisable and automated. Thus, we decided to study and develop its integration in the context of PRV. Mostly because, one of the drawbacks of PRV is the assumption that an existing model of the system exists. Moreover, since PM completely depends on the event logs generated by the system execution, more logs are used, and better (i.e., more precise) models are extracted. Because of this, PM does not only allow PRV to be applied when a model of the system does not exist, but it also makes PRV more robust and reliable. For instance, when the system under analysis presents dynamic aspects, to rely on a static model would eventually bring to wrong predictions. Instead, if the model is automatically obtained by observing how the system behaves, it may keep up with the change and be a more reliable representation of how the system is currently behaving. 3
When applying RV with a predictive avour, we need a model of the system to predict future events. Without such a knowledge, each event would be considered observable in the future, and the monitor would need to evaluate all possible continuations of the current analysed trace. Nonetheless, how the model of the system is generated is not de ned a priori. In previous works [6,30,21,31,17,10], the model of the system is assumed to be manually created by an expert of the system. Here, we show how the standard predictive runtime veri cation work ow can be enhanced using process mining techniques to automatically synthesise the model of the system.
(
(
Process Mining Model
Predictive Model ( )
(
(
(
Step 1: Model extraction As it is true for all process mining algorithms,
everything starts from a set of log les. These log les contain information about
previous executions of the system, and can be used to predict future executions as
well. Given such a set of log les, a process mining algorithm of choice can be
selected to parse the logs and generate a model representing the system behaviour
(Process Mining Model ). Depending on the algorithm, the resulting model may
be di erent; even though usually the most common formalisms used to specify
such models are Petri Net (PN) [20] and Directly-Follows Graph (DFG) [5].
Step 2: Predictive Model derivation The model extracted by the process
mining algorithm (step (
Step 3: Monitor synthesis Once the model of the system is obtained (steps
(
Step 5: Log les update An interesting aspect of our approach is that log les
can be used at two separate levels. They are used to synthesise the model of the
system through process mining at step (
Incrementally Predictive Runtime Veri cation instantiation
In Section 3, we present the general work ow, where no speci c formalism is
xed. In this way, depending on the domain, the approach can be customised for
obtaining better results. Nonetheless, for a better understanding, we present an
instantiation of our approach, where we use DFG as formalism for representing
the Process Mining Model, Probabilistic Finite-State Machine (PFSM) [24] and
(
(
(2b) ev1 s0 ev4 ev4 s2 ev2 s1
s2
Buchi Automaton
hev3; v2;3v+2;3v2;4 i
ev3
log les
(
Figure 2 shows an overview of the instantiated veri cation work ow; where,
starting from a set of log les representing di erent system executions, and an
LTL property ' to verify, we obtain a predictive monitor. The veri cation process
consists in 6 steps (since step (
Step 3: Monitor synthesis Once we obtain a model of the system, a predictive
monitor can be synthesised (following De nition 2). In [31], the authors present
the approach for synthesising predictive monitors for LTL properties, where the
model of the system is assumed being a BA. Following the same approach, at step
(
Steps 4-5: Monitor execution and Log les update These steps do not depend on the speci c instantiation and are the same as the steps in Section 3. 2 Since less future continuations have to be considered. The Python implementation of our approach is publicly available as a GitHub repository3. We implemented all the engineering steps presented in this paper, when instantiated to the case with LTL properties and BA models. More in detail, the resulting tool takes in input: (i) a set of log les (expressed as a single XES le4), which is the standard format used in PM to represent event logs; (ii) a threshold to guide the mapping from PFSM to BA; (iii) an LTL property to verify; (iv) a trace generated by the current system execution to analyse.
To implement step (
RV is a rich research area, but PRV is still rising. One of the oldest works on PRV is presented in [31]. In this work, the authors present an extension of the standard RV approach when applied to LTL properties. Di erently from the 3 https://github.com/AngeloFerrando/IncrementallyPredictiveRV 4 http://www.xes-standard.org/ 5 https://pm4py.fit.fraunhofer.de/ 6 http://fit.fraunhofer.de/process-mining 7 https://github.com/AngeloFerrando/MultiModelPredictiveRuntimeVerification rest of works in literature, the prediction of future events is not obtained using a model of the system, but is limited to a single sequence of events (called nite predictive word ) that is concatenated to the analysed trace. With respect to our solution, no explicit { nor complete { representation of the system is used. The same year, one of the authors proposed an extended version [17], where instead of considering one single predictive word, a BA model is integrated inside the standard generation of LTL monitors. The resulting approach is at the basis of the predictive library we use in our tool to synthesise predictive LTL monitors. The main di erence is in the generation of the BA, which in [17] is given, while in our approach is automatically extracted through PM. Moreover, our approach is intrinsically general. In fact, LTL and BA are just a possible instantiation. A more recent work where prediction is obtained through assumptions is presented in [10]. The authors propose a di erent way to synthesise predictive monitors for LTL properties, where the model used to predict the future events, instead of being a BA, is a Fair Kripke Structure (FKS) [14]. Similarly, in [21], another PRV approach is presented, where the model is instead de ned as a Timed Automaton. In both cases, the main di erence with our approach is in the generality and the fact that the model is not given but automatically synthesised. On a completely di erent line of research, we may nd [6], where probabilistic models, like Markov Models, are used. This work is very similar to ours because, di erently from the others mentioned before, it does not assume the model of the system is given. In fact, the probabilistic model used in the resulting RV framework is trained on samples generated by the system execution using the Baum-Welch algorithm [23]. Even though similar in principle, this work di ers from our solution in three aspects: (i) it uses machine learning techniques to extract the model, while we rely on PM techniques; (ii) it does not de ne any notion of incrementality; (iii) it considers only nite extensions. To the best of our knowledge, the work that is closest to ours is presented in [19]; where the authors use PM to extract the model used for synthesising predictive monitors as well. With respect to our approach, in [19] the objective of the predictive monitor is slightly di erent. Instead of being purely focused on the veri cation of the system under analysis, they are more interested in using the monitors to recommend the system on how to proceed. To do so, they focus on the probabilistic aspects and present a framework to suggest the best actions to perform in order to increase the probability of satisfying a given LTL formula. Moreover, their solution is less general than ours. Their approach is hard-coded in the Business Process scenario, while our veri cation work ow is general and tackles all the engineering steps necessary to integrate PM inside the creation of predictive monitors. 6
In this paper, we present a general veri cation work ow for integrating PM in the generation of predictive monitors. We show all the engineering steps that, from a set of log les, bring to the extraction of a model which can be used to predict future events and speed up the RV process. We present an overview of the veri cation workload where no formalism is enforced. This choice increases the impact of the work in the veri cation community, since these engineering steps can be customised w.r.t. the user's needs. Nonetheless, to help better understanding the approach, we also show an instantiation with LTL properties and BA models. The choice of these two formalisms is due to their being largely used in the veri cation community.
Finally, a Python prototype tool is presented. We brie y show its features and how it implements the engineering steps presented in the paper.
With respect to future directions; this is an initial work on the topic and
there are many di erent aspects that still need to be tackled. For instance, at
the current level, the probability is not considered in the monitor and it is lost
in the translation from PFSM to BA. Nonetheless, this is an interesting aspect
to explore further. Indeed, the notion of threshold could be used to add more
information to the monitor's outcome. This could also bring to the generation of
multiple BA, each corresponding to a di erent threshold. This would be
interesting to analyse, and it could be a starting point for a more thorough comparison
between our approach, and the one presented in [19].
Greece, June 16-20, 2014. Proceedings. Lecture Notes in Computer Science,
vol. 8484, pp. 457{472. Springer (2014).
https://doi.org/10.1007/978-3-319-078816 31, https://doi.org/10.1007/978-3-319-07881-6_31
20. Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Universitat Hamburg
(1962)
21. Pinisetty, S., Jeron, T., Tripakis, S., Falcone, Y., Marchand, H., Preoteasa, V.:
Predictive Runtime Veri cation of Timed Properties. Journal of Systems and Software
132, 353{365 (2017)
22. Pnueli, A.: The temporal logic of programs. In: 18th Annual
Symposium on Foundations of Computer Science, Providence, Rhode Island, USA,
31 October - 1 November 1977. pp. 46{57. IEEE Computer Society
(1977). https://doi.org/10.1109/SFCS.1977.32, https://doi.org/10.1109/SFCS.
1977.32
23. Rabiner, L.: A tutorial on hidden markov models and selected
applications in speech recognition. Proceedings of the IEEE 77(
In: SALOMAA, A. (ed.) Theory of Automata, International Series of Monographs
on Pure and Applied Mathematics, vol. 100, pp. 71{113. Pergamon (1969).
https://doi.org/https://doi.org/10.1016/B978-0-08-013376-8.50008-3, https:
//www.sciencedirect.com/science/article/pii/B9780080133768500083
25. Sarno, R., Sungkono, K.R., Johanes, R., Sunaryono, D.: Graph-based algorithms
for discovering a process model containing invisible tasks. International Journal of
Intelligent Engineering and Systems 12, 85{94 (2019)
26. Van Der Aalst, W.: Data science in action. In: Process mining, pp. 3{23. Springer
(2016)
27. Waspada, I., Sarno, R., Sungkono, K.: An improved method of
parallel model detection for graph-based process model discovery. International
Journal of Intelligent Engineering and Systems 13, 127{139 (04 2020).
https://doi.org/10.22266/ijies2020.0430.13
28. Weijters, A.J.M.M., Ribeiro, J.T.S.: Flexible heuristics miner (FHM). In:
Proceedings of the IEEE Symposium on Computational Intelligence and Data
Mining, CIDM 2011, part of the IEEE Symposium Series on
Computational Intelligence 2011, April 11-15, 2011, Paris, France. pp. 310{317. IEEE
(2011). https://doi.org/10.1109/CIDM.2011.5949453, https://doi.org/10.1109/
CIDM.2011.5949453
29. Wen, L., Wang, J., van der Aalst, W.M.P., Huang, B., Sun, J.: Mining
process models with prime invisible tasks. Data Knowl. Eng. 69(
In: NASA Formal Methods. LNCS, vol. 7226, pp. 418{432. Springer (2012)