Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

KeY [2] is a deductive verification tool for data-centric functional correctness properties of Java source code. KeY generates proof obligations in dynamic logic (DL), a modal logic for reasoning about programs. DL extends first-order logic with two modalities, and \({[p]}{\phi }\), where p is a program and \(\phi \) is another DL formula. The formula is true in a state s if there exists a terminating run of p, starting in s, resulting in a state where \(\phi \) holds. The formula \({[p]}{\phi }\) holds in a state s if all terminating runs of p, starting in s, result in a state in which \(\phi \) holds. For deterministic programs p, the only difference between the two modalities is that termination is stated in , and assumed in \({[p]}{\phi }\).

KeY features (static) verification of Java source code annotated with specifications written in the Java Modelling Language (JML) [29]. JML allows for the specification of pre- and postconditions of method calls, and class/interface invariants. The main features of KeY are the translation of JML annotated Java programs to Java DL, and a theorem prover for validity of Java DL formulae, using a sequent calculus, covering almost all features of sequential Java (with the exception of generics and floating-point types currently). Given a set of formulae \(\varGamma \), the sequent holds if p, when starting in a state fulfilling all formulae in \(\varGamma \), terminates in a state fulfilling \(\phi \). The calculus uses the symbolic execution paradigm. For that, DL is extended by explicit substitutions. During the symbolic execution of p, the effects of p are gradually, starting from the front, turned into explicit substitutions. Thereby, after some proof steps, a certain prefix of p has turned into a substitution \(\sigma \), representing the effects so far, while a remaining program \(p'\) is yet to be executed. While verifying p, an intermediate proof node may look like . It tells us that, if \(\varGamma \) was true before the original program p, and \(\sigma \) is the accumulated effect up to now, then \(\phi \) will be true after executing the remaining program \(p'\).

As an example, consider a proof of the following DL sequent:(where \(p_1\), \(p_2\), and q are Java fragments and \(\phi \) is some postcondition). The sequent says that in each state where x and y are positive, the program given in the modality (which first swaps x and y using arithmetics) will terminate and result in a state where \(\phi \) holds. When proving this sequent, the KeY prover will first, in a number of steps, turn the three leading assignments into explicit substitutions, apply the first to the second, the result to the third, and perform arithmetic simplification, arriving at

where \((\texttt {x}\leftarrow \texttt {x+y}\,\Vert \,\texttt {y}\leftarrow \texttt {x}\,\Vert \,\texttt {x}\leftarrow \texttt {y})\) denotes the explicit (parallel) substitution resulting from symbolic execution of the first three statements. A ‘right-win’ semantics is adopted to resolve clashes in substitutions, such that the above simplifies to:

In general, most proofs branch over case distinctions, often triggered by Boolean decisions in the source code. The branching happens by applying rules like the following, simplified¹ if rule:

In our example, applying the if rule to the latest sequent results in splitting the proof into two branches, with the following sequents, respectively:

Applying the substitution on the left side of either sequent results in: Note that in this step, by applying the swapping substitution, the branching condition (x being even or odd) on the state after swapping got translated into a condition on the prestate of the original program p, before the swapping. The resulting sequents tell us, among other things, that if y is even (respectively odd) in the prestate of p, then path \(p_1\) (respectively \(p_2\)) is taken in the execution of p. In general, when building a proof in such a symbolic manner, the left side of sequents accumulate conditions on the original prestate through a particular execution path.

Once all proof branches are closed, we have a complete proof of the root sequent. However, a proof attempt may result in a partial proof, only, where some proof branches are closed and others are not. Such partial proofs are important for the work presented in this article. In the above example, consider a partial proof where the left branch, i.e., the sub-proof for sequent (2), is closed, whereas the right branch, i.e., the sub-proof for sequent (3), is not closed. From this partial proof, we can conclude that the following modification of the root sequent (1) is valid:(We added \(\texttt {y\%2} = \texttt {0}\) to the left side of (1), as additional assumption.) This sequent can be proven by replaying the original proof, where now both branches would close. The left branch closes as the sub-proof for (2) will replay identically. The right branch closes because the following variant of (3) can be closed immediately, due to contradicting assumptions:

Larva ² [19] is an automata-based runtime verification tool for Java programs. As with many other runtime verifiers, Larva automatically generates a runtime monitor from a property written in a formal language, in its case using Dynamic Automata with Timers and Events (DATEs) [18]. Transitions in a DATE are of the form: \({event} \mid {condition} \mapsto {action}\), where event is what triggers the transition, the condition is checked and must hold in order the transition to take place, and the action is a code snippet to be performed when taking the transition (after checking the condition). DATEs are an extension of timed automata—they are effectively finite state automata, whose transitions are triggered by system events (primarily entry points and exit points \(\texttt {f}^\uparrow \) of methods) and timers, but augmented with: (i) A symbolic state which may be used as conditions to guard transitions and can be modified via actions also specified on the transition; (ii) replication of automata, through which a new automaton is created for each discovered instance of an object; (iii) communication between automata using standard CCS-like channels with c! acting as a broadcast on channel c and which can be read by another automaton matching on event c? Full details of the formalisation of DATEs can be found in [19].

The automata illustrated in Fig. 1 represent an example of DATE automata describing a property which should hold during a connection. The first automaton ensures that if the connection drops (event ) occurs five times, a message is broadcast (over channel \( unreliable \)) to highlight the fact that the connection port is unreliable. The second automaton (with the \( foreach \) keyword) ensures that every time a file transfer is initiated, an automaton is created to monitor that transfer. If during the transfer (i.e. between the events and \(\texttt {end}^\downarrow \)) one receives event \( unreliable? \), no further transfers may occur.

In order to monitor a system using Larva, the user must provide the system to be monitored (a Java program) and a set of properties in the form of a Larva script (a textual representation of DATEs). Larva transforms the set of properties into monitoring code together with AspectJ code to link the system with the monitors. Since the Java byte code is used for instrumentation, it is possible to monitor third-party software with Larva, though knowledge of methods names is still required.

We will use the following notation to write quantified formulae, based on the notation used by Gries [27].These formulae mean “for all x satisfying R, B is fulfilled” and “there exists x satisfying R for which B is fulfilled”, respectively. Both R and B are formulae potentially containing x as a free variable. We will refer to R and B as the range and body of the quantified formula, respectively. This notation relates to standard (un-ranged) quantified formulae in the following way:

In this section we formally define the notion of ppDATE previously introduced in Sect. 3. In order to do so, we first introduce formal definitions for triggers, conditions and actions.

In the previous definition, systemtrigger matches a visible system event, such as the point of entry into a method or the termination of a method execution. Given a method name \(\sigma \in \varSigma \),

represents entering method \(\sigma \) and

represents the termination of the execution of \(\sigma \).

In addition, actevent represents an event generated by the execution of an action in a transition of a ppDATE, which we will call action events. This kind of events can only be generated by bang (“!”) actions (see Definition 2). An action h! generates the action event h, which in the next step can activate the trigger h? This way, action events enable communication among ppDATEs, where h! and h? mean sending and receiving a message, respectively.

As we have mentioned before, whenever a transition is fired an action can be executed. The following shows the definition of actions.

skip is the effect-less action. The ‘\(=\)’ is an assignment operator, v is a ppDATE variable and e is a (side-effect free) expression that may depend on system variables and ppDATE variables; actevent! represents the generation of action event actevent; create represents the creation of a ppDATE, where template is a ppDATE template to be instantiated (see Definition 8), and \(\overline{{args}}\) are the values which the formal parameters of template are instantiated with; the ‘; ’ is the sequence operator for actions; if-then is a conditional whose branching condition depends on the valuations of system variables (\(\textit{Sys}\)) and ppDATE variables (\(V\)); and Program represents a side-effect free program (see Definition 3), i.e., it is restricted to not have any effect on the system which could in turn be observed by the (ppDATE generated) monitor. For instance, a Program could perform logging of system/monitor behaviour. More powerful Programs, which would for instance allow error recovery, are relevant, but left for future work.

Boolean expressions are used in different contexts: (i) conditions (c) of transitions; (ii) conditions of if-then actions, and (iii) pre- and postconditions (\(\pi \), \(\pi '\)) in Hoare triples. As a syntactic category for such Boolean expressions, we chose Boolean JML expressions. They extend Boolean Java expressions, and thereby allow Java methods as sub-expressions (like in ‘m.get(k) == o’). Additional features of Boolean JML expressions include universal and existential quantification, which are frequently used in Hoare triples, the ability to refer in a postcondition to a) the return value (with ‘ ’), and b) the preexecution value of an expression (like in ‘ ’).

We do not give a formal definition of the semantics of BJMLE here, just the following comments. The meaning of negation, conjunction, disjunction, implication, and equivalence are standard. The same is true for the first two forms of quantification. Concerning the other two forms, “\(\ldots \) a; b)”, they relate to standard quantification in exactly the same way as was explained in Sect. 5.1. (The only difference is that there we discussed meta-level notation, whereas BJMLE is part of ppDATE.) The constructs and are only allowed in postconditions of Hoare-triples (i.e., in \(\pi '\)). refers to the return value of a (non-void) method. allows to evaluate sub-expressions not in the post-state (which is the default), but in the prestate of a method’s execution. For instance, ‘ ’ in a postcondition of method m says that the difference between the values of x before and after the execution of m is the value which y had before m’s execution.

In order to allow or disallow and , in the following, we provide one syntactic category for postconditions, and one for all other conditions.

Now we can formally define ppDATE. As a ppDATE describes properties about a particular system, we assume that every time we make reference to the set of system variables, these variables belong to the system under scrutiny.

We will write to mean that, given a ppDATE m whose transition relation is t, \((q,tr,c,a,q')\in t\). The subscript m is omitted if it is clear from the context. In addition, we will use the usual Hoare triple notation \(\in \varPi (q)\) to denote \((\pi ,\sigma ,\pi ') \in \varPi (q)\).

In addition to ppDATEs which exist up-front, and ‘run’ from the beginning of a system’s execution, new ppDATEs can be created by existing ones. For instance, one may want to create a separate ‘observer’ for each new user logged into a system. For that, one needs to be able to define parameterised ppDATEs, which we call templates, and allow ppDATEs to create new instantiations of templates. Given a ppDATE m, the creation of a new ppDATE, which will run in parallel to m, can be achieved by using action create on a transition of m. This action receives as arguments a ppDATE template describing the ppDATE to be created and a list of arguments to instantiate the quantified variables on the template. Below, we formally define ppDATE templates.

In the above definition, a template of order \(n+1\) is defined by ‘abstracting’ over templates of order n, annotating the abstracted ‘hole’ X by the right category, such that template instantiation (see below) can be guaranteed to result in a well-typed ppDATE. When constructing a ppDATE template, the choice of trm in Definition 7 does not matter. Its only role is to carry well-typedness of ppDATEs over to ppDATE templates. Informally, the above definition says that, within \(\lambda X\!\!:\!\!C.m'\), the X can appear anywhere in \(m'\) where a term of category C is expected.

If \(\overline{X}\) is a vector of template variables \(X_1,\ldots ,X_n\) and \(\overline{C}\) is a vector of syntactic categories \(C_1,\ldots ,C_n\), then we can write \(\lambda \overline{X}\!\!:\!\!\overline{C}.m\) to mean \(\lambda X_1\!\!:\!\!C_1\ldots \lambda X_n\!\!:\!\!C_n.m\).

We can expand template instantiation to multiple arguments in the following way. Given \(n\ge 2\), assume \(\overline{X} = X_1,\ldots ,X_n\), and \(\overline{C} = C_1,\ldots ,C_n\), and \(\overline{{trm}} = {trm}_1,\ldots ,{trm}_n\) (with \({trm}_i \in C_i\)). We extend the instantiation function inst to an arbitrary number of arguments in the following way:

Note that the previous property should hold for any possible instance of the (boolean) variables appearing in both c and \(c'\). In addition, although determinism on the Hoare triples’ preconditions is not problematic in itself, we choose to extend the determinism condition to ensure that for any two Hoare triples in a single state over the same function have disjoint precondition so as to have a more effective monitoring algorithm of these triples: for any and in \(\varPi (q)\), \(not (\pi _1\ and\ \pi _2)\).

After having defined (individual) ppDATEs, we can now define a network of ppDATEs.

Note that on a network, whenever a trigger is activated, several ppDATEs can have an enabled transition ready to be fired, i.e., a transition whose trigger is active and whose condition holds. Whenever this happens all these enabled transitions are fired in parallel. Also note that the set of ppDATE variables \(V\) is global to the network of ppDATEs, rather than local to individual ppDATEs. Thereby, \(V\) is effectively the ‘shared memory’ of the network.

Finally, we extend the notion of deterministic ppDATE to a ppDATE network.

ppDATE networks describe which system behaviours are allowed, and which are not. Here, we consider as behaviour basically a series of system events, where each event also comes with a ‘snapshot’ of the values of (visible) system variables, taken at the time where the event occurs. Formally, these snapshots are valuations, i.e., mappings from variables to values (of adequate types). Apart from the observed system, the ppDATE networks themselves may create new events.

An event may therefore either be a system event (i.e., generated by the system under scrutiny due to entering or leaving a method) or an action event (i.e., generated by the execution of an action ! in a ppDATE transition). Formally:

A systemevent consists of a systemtrigger which is indexed with a natural number representing the nth execution of the method associated to the trigger. Such an index will be considered an identifier⁶ unique to each execution of the method.

We distinguish the set of system variables valuations \(\varTheta _{\textit{Sys}}\), with typical element \(\theta \), and the set of ppDATE variable valuations N, with typical element \(\nu \). We represent valuations both as functions and (functional) relations⁷, i.e., sets of pairs. This means that the notation \(\beta (v) = val\) is equivalent to the notation \((v, val) \in \beta \). The union of valuations is therefore a set union such that, for any two valuations \(\beta \) and \(\beta '\), \(\beta \cup \beta ' = \{ (v,val) \mid (v,val) \in \beta \ or\ (v,val) \in \beta ' \}\). In the presentation of examples, we limit the valuations to those variables which matter for the example at hand, for simplicity.

In our semantic rules, we will use union over valuations only when the domain of valuations do not overlap, as for instance in \(\theta \cup \nu \). Another operation on valuations is the modification of a valuation \(\beta \) at variable x by value val, written \(\beta [x\leftarrow val]\). It is defined as:

Given a set of variables S, a valuation \(\beta \) for S, and condition \(c \in cond_{S}\), we will write \(\beta \models c\) to denote that c is satisfied by \(\beta \). This is however not sufficient for postconditions as they can refer to two valuations, after and before (“ ”) a method’s execution. For that, \(\models \) will be overloaded. Given a set of system variables \(\textit{Sys}\), valuations \(\theta \) and \(\theta '\), and a postcondition \(c \in postcond_{\textit{Sys}}\), we will write \(\theta , \theta ' \models c\) to denote that c is satisfied by \(\theta \) and \(\theta '\). When this is used, \(\theta '\) will be the current valuation of \(\textit{Sys}\) when exiting a certain method execution, whereas \(\theta \) holds the valuation from before that method execution. We only sketch the definition of \(\models \) here as it follows the standard of first-order logic semantics. We use the two semantic truth values T and F. For \(c \in cond_{S}\), we define \(\beta \models c\) iff \({eval}_\beta (c) = T\), where \({eval}_\beta \) is recursively defined over the structure of c as standard in first-order logic⁸, with the base case \({eval}_\beta (\texttt {x}) = \beta (\texttt {x})\) for variables x. For \(c \in postcond_{\textit{Sys}}\), we define \(\theta , \theta ' \models c\) iff \({eval}_{\theta , \theta '}(c) = T\). The definition of \({eval}_{\theta , \theta '}\) is almost identical to the definition \({eval}_\beta \), with the base case \({eval}_{\theta , \theta '}(\texttt {x}) = \theta '(\texttt {x})\) for program variables x. The only case in the definition where the pre-valuation \(\theta \) matters is the evaluation of -expressions: . This means that, in postconditions, the post-valuation \(\theta '\) acts as the default, however not inside -expressions, where instead the pre-valuation \(\theta \) counts. The other additional operator in postconditions is . To handle its evaluation properly, we assume a special system variable named . Whenever a non-void method returns, its return value, say val, is assigned to , such that, in the post-valuation \(\theta '\), we have .

A system trace is a sequence of tuples consisting of an event and a ‘system snapshot’, i.e., a valuation of the system variables taken at the time when that event occurs.

Given a system trace w, each tuple in w will shift a global configuration of a ppDATE network to another. Global configurations are defined in terms of local configurations.

The tuple \((m,q,\rho )\) is a configuration of ppDATE m—where q represents the current state, and \(\rho \) allows to monitor potential violations of Hoare triples. For that, \(\rho \) stores which exit event (\(\in {systemevent}\)) should cause a checking of which postcondition (\(\in {postcond}\)). The semantic rules described below (Sect. 6.4) will guarantee that only method exit events (of the form

) will appear in \(\rho \). During the processing of a trace, the appearance of

at the same time as the current state has a Hoare-triple with a fulfilled precondition, \(\theta \models \pi \), the corresponding postcondition \(\pi '\) is associated with

in \(\rho \), together with \(\theta \). Later, the appearance of

will cause a look-up of

in \(\rho \), in order to check \(\theta , \theta ' \models \pi '\).

Before giving an example, we define the notion of initial global configuration for a ppDATE network.

In the above example, the action \(v=v+1\), does not generate any event. In general, however, actions may generate events. For storing action events (and process them in the next step), we introduce the concept of extended global configuration.

E contains the events to be processed in the next (small) step. In the operational semantics to be described below, E will either be a singleton set containing a system event, or a set of action events generated by the executions of actions in the latest transition.

The structural operational semantics given in Sect. 6.4 formalises such behaviour.

When assigning meaning to actions, there are two levels to consider. One is the level of the local actions, executed when an individual ppDATE takes a transition. The semantics of those is sequential, as defined below. On top of the assignments changing the ppDATE variable valuation, the local actions may generate events, and create new instances of ppDATE templates.

The other level is parallel actions, where we compose simultaneous actions of transitions taken in parallel by different ppDATEs. Here, we need to devote special care to exclude conflicting writes to, as well as race conditions between reads and writes from/to, the same variable. Also, we need to make sure that if only one ppDATE writes to x, then the parallel composition propagates this effect. All this makes it necessary to keep track of all reads and writes at the local level, prior to execute the parallel composition. However, the treatment of the local effects and newly created ppDATEs is simpler: we just take the union of those when doing the parallel composition.

Following the definition of actions (Definition 2), the prog in the last line above is a side-effect free program, i.e., it has no effect which could be noticed in the current formalism, which is why we can simulate it with skip. prog will have purposes orthogonal to our formalisation, like logging.

We are now in the position to define the parallel composition of actions. Imagine we have a configuration with 5 parallel ppDATEs, 3 of which have enabled transitions, with actions \(a_1\), \(a_2\), and \(a_3\), respectively. Assume moreover that the current ppDATE variable valuation is \(\nu \). The parallel composition of the meaning of \(a_1\), \(a_2\), and \(a_3\), is performed by \({mergeParalActs}_\nu (\{[\![a_1]\!], [\![a_2]\!], [\![a_3]\!]\}) = (\nu ', E', {New}')\). The function mergeParalActs takes a set of semantic actions as input, and computes a resulting valuation \(\nu '\), a resulting set of events \(E'\), and a resulting set of newly generated ppDATEs, \({New}'\). The sets \(E'\) and \({New}'\) will simply be the union of the corresponding sets from \([\![a_1]\!]\), \([\![a_2]\!]\), and \([\![a_3]\!]\). But the resulting valuation is slightly more involved. Actions may conflict (e.g., we write to the same variable in different actions), or have race conditions (i.e., we read from a variable and write to it in different actions). In those cases, we leave the result of mergeParalActs deliberately undefined. In all other cases, the different effects of the actions are merged. The index of the merging function, \(\nu \), serves as a fall back for those variables which have not been written to. In particular, \(\nu ' = \nu \) in case the set of actions to be merged is empty.

These explanations are formalised in the following function, merging a set of action meanings (Definition 19):

Note that if there are no actions to merge, we have \({mergeParalActs}_\nu (\emptyset ) = (\nu ,\emptyset ,\emptyset )\).

In this section we give structural operational semantics rules (SOS) for ppDATEs. These rules will have the following generic form:where name is a label used to identify the rule, Goal is the property enforced by the rule and the premises \(H_1, \cdots , H_n\) are assumptions over the values of the Goal.

Before defining violating system traces, we have to introduce the notion of counter-example.

(The symbol \(\mathbin {++}\) represents the concatenation of traces.) This means that a counter-example either (i) ends in a bad state (in one of the local configurations), or (ii) ends with the exiting of a method execution who’s postcondition (stored in \(\rho \)) is currently violated. Note that (i) and (ii) are not exclusive, so a counter-example may have both properties at once. Also note that violations of preconditions when entering methods is not mentioned here. In our semantics, the violation of preconditions does not as such result in a counter example. It only means that the postcondition of the corresponding Hoare triple does not need to be checked further on (see \({entry}_2\), Fig. 7).

DATE [18] is a formalism similar to ppDATE, except that the automata do not include Hoare triples in the states. DATEs also include support for timers, which are not in ppDATEs. However, since the work we present here does not use timers, we leave them out from the formalisation. Formally:⁹

Note that since a DATE is effectively a ppDATE, the semantics for DATEs are already covered by the semantics of ppDATEs. We will also refer to a (deterministic) network of ppDATEs where each ppDATE in the network is a DATE, as a network of DATEs and similarly DATE templates.

Here we present how to translate a ppDATE (network) into a DATE (network). However, first, let us intuitively analyse how the ppDATE depicted in Fig. 2, which we will refer to as m, can be translated into a DATE \(m'\).

For simplicity, we assign the following names to the different Hoare triples in the states of m.Then, we begin the translation by generating the DATE template illustrated in Fig. 10, which will be used to create DATEs in charge of controlling the postconditions of the previous Hoare triples.

Next, we start dealing with the translation of the transitions of m. \(m'\) will have exactly the same set of states as m, and it will have similar transitions to the ones of m. The only difference is that the transitions in \(m'\) will also have to address the verification of the Hoare triples. For instance, while being in state q, if the method brew() is executed and the precondition of \(h_1\) holds, then its postcondition will have to be verified whenever method brew() finishes its execution.

Therefore, for every transition of the form

such that a Hoare triple is in q, \(m'\) will include a modified version of this transition in such a way that whenever this transition is fired, if \(\pi \) holds, then the execution of its action will have to create an instance of template \(exit\_cond\_checker\). Thus, transitions \(t_1\), \(t_3\) and \(t_4\) (recall Fig. 2) are modified as follows:where,In the previous transitions we have used as the conditions of the if-expressions in actions \(a_1\), \(a_2\) and \(a_3\), the preconditions of the different Hoare triples to be verified in each case. Moreover, function part_eval partially evaluates its argument, replacing the expressions operator the current value of e. If a postcondition does not include such operator, then part_eval is the identity. Note that even though the if-expression in the transitions \(t_1'\) and \(t_4'\) may seem unnecessary, we include it anyway in order to exactly reflect how the translation algorithm works.

In addition, if at a certain state, a Hoare triple has to be verified, but in that state there are no outgoing transitions with an event related to the method in the Hoare triple, then a new transition is added to \(m'\) in order to be able to control such Hoare triple. For instance, in state q the following self-transition has to be added in order to verify \(h_2\) and \(h_3\).where,Again, we use the preconditions of the Hoare triples as conditions of the previous action.

Given a transition such that (i) tr fires upon exiting a method, or (ii) tr fires upon entering a method but there is no Hoare triple associated to this method in q, these transitions remain untouched, i.e., it is translated as . For instance, transition \(t_2\) is translated as follows.Figure 11 illustrates the DATE obtained when translating m following the previous steps. Note that whole translation would consist on the previous DATE and the generated template exit_cond_checker.

In this section we will show that the translation algorithms introduced in the previous section are sound.

Here, we formally introduce two lemmas which together form the coupling invariant that is used to prove soundness. The proofs of these lemmas can be found in “Appendix 1”.

Lemma 2 states that given a trace, both a ppDATE network \(pn\) and its translation to DATE will change their initial global configuration to global configurations and , respectively, such that \(\nu = \nu '\), and that for every where m is in \(pn\), there is a local configuration \((m',q',\emptyset ) \in \tilde{L}\) such that \(m'\) is the translation of m and both m and \(m'\) are in the same state, and vice versa.

In this lemma we represent the translation of a single ppDATE to DATE with the function \(\kappa \in \textit{ppDATE} \mapsto \textit{DATE} \).

Lemma 3 states that given a trace, if this trace shifts a ppDATE network \(pn\) and its DATE translation from their respective initial global configuration to some global configurations and , respectively, then for each entry

in a \(\rho \) component of a local configuration in there is one local configuration in whose DATE component is an instance of the template \(exit\_cond\_checker\) in charge of controlling \(\pi '\), and vice versa.

Before describing how StaRVOOrS works, we need to introduce how a ppDATE specification is written as an input script for this tool. Below, we show the input script for the ppDATE template illustrated in Fig. 13, and the ppDATE which creates its instances. In addition, we give a brief description of each one of the sections this script. For a full description on how to write ppDATEs as an input script for our tool, one may refer to the StaRVOOrS User Manual.¹¹

The section IMPORTS lists the Java packages which may be used in any of the other sections of the script, in this case UserInterface and Hashtable. The section TEMPLATES contains the description of the ppDATE templates (tagged by TEMPLATE). Here, the section TRIGGERS is used to declare the different triggers which may be used in the transitions of the ppDATE, i.e, login_exit, logout_entry, deposit_entry, and the section PROPERTY describes the different states, i.e., q1, q2 and bad, and transitions of the ppDATE. Note that the syntax q1 (add_ok) associates the Hoare triple tagged as add_ok to state q1. This means that the Hoare triple add_ok has to be verified if the method associated to it, in this case method add, is executed whenever the ppDATE is in state q1. The section GLOBAL contains the description of the ppDATE. Here, ppDATEs are described in the same manner as in a TEMPLATE section. However, note that it is also possible, as it is the case in our example, to use the special section PINIT when describing the section PROPERTY. Section PINIT represents a ppDATE with single state, and a looping transition which is fired every time an object of the class listed within this section (UserInterface in our example) is declared, leading to the creation of an instance of the listed template for that object (prop-deposit-temp in our example). We have included this special case because it is quite common to have ppDATEs only focus on creating instances of a template upon declaration of a particular object. Regarding the section CINVARIANTS, class invariants are described by the syntax class_name {invariant}, meaning that invariant has to be fulfilled by all the methods in the class class_name. These invariants are only meant as a help for the deductive verification of the Hoare triples (see Sect. 8.2). If no invariants are needed, then this section can be omitted. Finally, the section HTRIPLES gives a list of named Hoare triples (tagged by HT). Here, PRE describes the precondition of the Hoare triple, POST describes the postcondition of the Hoare triple, METHOD indicates which one is the method associated to the Hoare triple, and ASSIGNABLE lists the (class) variables that might be modified when the method associated to the Hoare triple is executed. Note that the predicates in invariants, pre- and postconditions follows JML-like syntax and pragmatics. For instance, in the Hoare triple add_ok the second semicolon separates the range predicate (\(\texttt {i}>\texttt {=0}\)&& \(\texttt {i}<\texttt {capacity}\)) from the desired property over integers in that range, (arr[i]==o).

StaRVOOrS is a fully automatic verification tool which takes the Java source code of the system under scrutiny and a file with the ppDATE specification for this system and produces (i) a runtime monitor, (ii) an instrumented version of the system given as input with event generation and additional code infrastructures required, (iii) a report summarising the results of the deductive verification of the Hoare triples, and (iv) a refined version (if any) of the provided ppDATE specification.

This tool implements the framework described in Sect. 4 with each stage of the framework, i.e., Deductive Verification, Specification Refinement, Translation and Instrumentation, and Monitor Generation, being performed automatically by the tool. Below, we describe the implementation of these stages through the use of the working example.

Note that even though we could have either described more properties or specified more control- and data-oriented behaviour in the properties we are depicting in this section, the ppDATEs introduced here are sufficient to highlight the benefits of using StaRVOOrS in a real application. In addition, for readability reasons, Hoare triples are not going to be included on the figures depicting the ppDATEs. Moreover, as the application is placed in a server, the monitor generated by our tool is placed in the server as well.

The previous specifications were analysed on a PC Pentium Core i7 using a sinlge core. A similar setup was used to perform the experiments in the following Sect. (9.3).

Since SoftSlate uses many Java libraries, to perform static analysis on its source code it was necessary to generate stub files for some of these libraries in order to allow KeY to find information about their method declarations.

Figure 19 illustrates a ppDATE describing the top-level specification of Mondex. To keep the ppDATE readable, the description of the different Hoare triples are not included in the figure. (We will show some of them below.)

At the automaton level, the ppDATE specifies the control-oriented property which indicates how the multi-step message exchange protocol is suppose to work. For instance, after the parties are initialised (encoded in state Parties Initialised), a message requesting to transfer more money than the one available in the source purse should fail. Otherwise, such a message should take the ppDATE to a state in which the protocol now allows for the money to be transferred to the destination purse (named Money deducted). Note that the ppDATE will not take any explicit action whenever the state BAD STATE is reached. It will stay in this state until the whole monitor is restarted.

In contrast, the pre/postconditions properties placed on the states of the ppDATE ensure the well-behaviour of the methods involved in the individual steps of the protocol, behaviour which obviously changes together with the status of the protocol. For instance, once two purses agree on participating in a money transfer and the destination purse has requested for certain amount of money, (encoded in state Money Deducted), method val_operation which transfers money from the source purse to the destination one should succeed and increase the money of the destination purse by the sent amount (provided the limit of its account has not been reached), as shown in the Hoare triple below:

On the other hand, if the same method is accessed after the funds have already been transferred (encoded in state Money deposit), then the destination purse content should remain unchanged, and the request should be ignored:

Note that both Hoare triples above have the same precondition, but depending on the state of the ppDATE (i.e., the state of the protocol) different behaviours (i.e., postconditions) are expected for method val_operation.

For this case study, we have used a setup identical to the one described in Sect. 9.2. Running StaRVOOrS on the source code of Mondex and the ppDATE depicted in Fig. 19 automatically produces a runtime monitored version of the application and a report summarising the results obtained from the static analysis. The static analysis and instrumentation process takes 1 minute 20 seconds, where most time is used by KeY to statically analyse the Hoare triples (approximately 1 minute 15 seconds).

The monitor generated by our tool consists one DATE to control the main property, and 24 DATEs templates to control the postconditions which were only partially verified by KeY, with 106 states and 196 transitions in total. By inspecting the report we can see that the two Hoare triples associated to the initialisation and termination of a transaction were fully proved, and that all the other 24 triples about the methods involved in the transaction protocol were the partially verified ones. For instance, let us consider the property already discussed in the previous section about method val_operation, which we will refer here to as val_operation_ok:

The report shows that the postcondition will have to be checked at runtime only when the condition status != 2 holds upon entering val_operation (i.e., the destination purse is not waiting for the arrival of the requested money). Thus, the previous Hoare triple was refined by StaRVOOrS as follows:

This refined version of the property is the one which will be runtime verified by the generated monitor.

The size of the source code of the original implementation of Mondex was 23.5kB. After running the tool, the total size of all the generated files (i.e. instrumented version of the source code and the implementation of the monitor) grows to 277.4kB.

We now summarise the experimental results of applying our approach to the Mondex case study.