We consider the problem of run-time discovery and continuous monitoring of new components that live in an open environment. We focus on extracting a formal model|which may not be available| by observing the behavior of the running component. We show how the model built at run time can be enriched through new observations (dynamic model update). We also use the inferred model to perform runtime veri cation. That is, we try to identify if any changes are made to the component that modify its original behavior, contradict the previous observations, and invalidate the inferred model.
Modern software systems increasingly live in an open world [
IDEAS-ERC, Project 227977-SMScom. 1 Although the terms \component" and \service" can be (and should be) disinguished, in this paper the terms are used interchangeably
In addition to the previous problems, one must consider the fact that the component may change at run time in an unannounced manner. In other words, even if a model were initially provided together with the exposed service, it may become unfaithful and inconsistent because the implementation may change at run time. For this reason, in open-world context the role of models is twofold. It may be necessary to infer it initially and it becomes then necessary to use the (inferred) model at run time to verify if changes invalidate the assumptions we could make based on the initial observations.
In conclusion, in the case where the model is initially absent, we need techniques to infer a formal model (a formal speci cation) for the components we wish to combine. We then need to keep the (inferred) model to analyze the run-time behavior of the component and detect wether the new observed behaviors indicate that a change has occurred in the component which invalidates the model.
In this paper, we propose a technique for run-time monitoring of component
changes that relies on the use of a particular class of formal models, behavior
models. The proposed approach requires a setup phase, in which the component
to be monitored must be in a sort of trial phase in which it can be safely tested
to extract an initial speci cation. This phase integrates techniques to infer
formal speci cations [
The paper is structured as follows. Section 2 presents the formalisms used in
the approach, that is, the kind of behavior models that we can infer and
synthesize. Section 3 describes how these models are constructed to enable the setup
step of our technique, while Section 4 describes their use at runtime to detect
component changes. A simpli ed running example is used to give a practical
hint on how the approach works. Finally, Section 5 discusses related approaches
and Section 6 illustrates nal considerations and future work. Space limitations
only made it possible to explain the innovative approach and to provide basic
examples. Additional details and more complex examples are available online [
We consider software components as black boxes, that is, their internals cannot
be inspected and they are accessible only through their API, which consists of
operations that might modify or not the internal state. Thus, each operation
can be a modi er or an observer, or it can play both roles. Operations may also
have an exceptional result, which is considered as a special observable value. As
a running example, we consider a simple component, called StorageService,
inspired by the ZipOutputStream class of the Java Development Kit [
We now introduce the formal models used in our approach, which belong to the class of so-called behavior models. To accomplish the main task of the approach, that is, the runtime detection of component changes, we rst need to de ne behavior models that they can \summarize" all the possible interactions with the software components, thus providing a description of the behaviors observed by its clients.
We start with Behavioral equivalence models ( Bem [
To describe every possible component interaction outside the Bem scope, we introduce a second kind of behavior model that generalizes the Bem through an abstraction: the protocol behavior models ( Pbm). Pbms provide an abstracted, less precise but generalized description of the interaction protocol with the component as opposed to the precise description in a limited scope provided by Bems. The new model is still based on a nite state automaton, but now states encode whether the results of observers are normal or exceptional2. States also abstract the behavior of modi ers as variant or invariant. A modi er behavior is variant if there exists a possible invocation with speci c actual parameters that brings the component in a di erent behavioral equivalence state. Otherwise, the modi er behavior is invariant. This abstraction is usually (but not always) associated with an exceptional result of the operation: it is the typical behavior of a removal operation on an empty container or a add operation on a full bounded container. Pbm transitions instead keep track only of the operation they represent, ignoring the values of the parameters. Thus they model the behavior of every possible modi er invocation; they synthesize the behavior of possibly in nitely-many behavior changes induced by the possible operation invocation. 2 If observers have parameters, then the abstraction can be i) always (i.e., for every parameter) normal; ii) always exceptional; iii) any intermediate situation, that is, for some parameters the result is normal and for others is exceptional .
S w; c S0 pE1 pE2 S1 S2
S4 In practice, they model the possibility that by performing an operation the set of operations enabled on the object may change. It is worth observing (but we do not show it here) that this abstraction may introduce nondeterminism in the automaton. Figure 2 represents the Pbm derived by performing the abstraction described above to the Bem in Figure 1.
The main contribution of the proposed approach is the integration of Pbms
and Bems. Because the Pbm is derived from the Bem through an abstraction
process, its completeness and accuracy actually depends on the signi cance of the
observations that produced the Bem during the setup phase. The setup phase
is deeply rooted in the small scope hypothesis. In its original formulation [
c pE
S4 c c; w; pE
S5 S1 w w pE
pE S3 c w; pE c S0 S1 S2 S3 S4
S5 The notation: [ ;
Legend: State S0 S1 S2 S3 S4 S5
S:StorageService, w:write, c:close, pE:putNextEntry close putNextEntry write
Observer Abstraction ZipException | [ ; [ ;
ZipException | ZipException] | | ZipException] ZipException | ZipException | | ZipException ZipException | IOException IOException
Modi er Behavior Abstraction Invariant Variant Invariant Variant Variant Invariant Variant Invariant Invariant Variant Variant Invariant Variant Invariant Invariant
Invariant Invariant Invariant
ZipException] means that for some parameter the method returns correctly (|), and for some other parameter throws ZipException which describes the protocol of all the possible interactions of clients with the component, while at runtime we can use the Pbm to nd component changes.
The two di erent models can be used together at run time. The behavior of a component is monitored and checked with respect to the Pbm. When violations are detected, a deeper analysis exploiting the more precise information contained in the Bem can be performed in order to discover whether the observation that is not described by the Pbm is a new kind of behavior that was not observed before, and thus requires a change of both the Bem and the Pbm to accommodate it, or instead it detects a component change that is inconsistent with the models. The Bem synthesizes the observations used to generate the Pbm, and thus it can be used to distinguish between likely changes of the analyzed component from new observations that instead just enrich the Pbm. In the following sections, we will discuss these aspects: the setup time construction of Bems and Pbms, and the runtime use of both models to detect likely component changes.
It should be noted that the Pbm is not a full speci cation of the component, thus it cannot be used to express complex functional behaviors, in particular the ones that are not expressible with a nite state machine, like complex container behaviors. Instead, the Pbm models the protocol that clients can use to interact with the component, that is, the legal sequences of operations. This limitation is also the enabling factor for runtime detection of changes: violations can be checked and detected relatively easily and the model can be promptly updated when needed. Instead, a full edged speci cation that supports in nite state behaviors, like the ones of containers, is de nitely harder to synthesize, check and update at runtime. 3
As we illustrated previously, the approach we propose prescribes two phases. The setup phase is performed on the component in a trial stage. The other phase corresponds to runtime. In the former, the component is analyzed through dynamic analysis (a set of test cases) to infer a Bem for the component. A Pbm abstraction is generated next to generalize the observed behaviors. In the latter phase, the two models are used at run time to detect component changes. In this section, we describe the rst phase, with particular focus on the generation of models, so that designers can get a formal description of a component whose behavior must be validated. 3.1
To generate a Bem during the setup phase, we adapt the algorithm and the
tool described in [
Given the importance of the objects used to perform the Bem generation phase, we want to exploit as much as possible all the knowledge available to analyze the class behavior with the most signi cant set of instances. The original Spy tool relied entirely on instances provided by the user interested in obtaining the Bem of a component. While the assumption that the user is able to provide some signi cant instances is fair, it may be hard to achieve since it requires a lot of e ort and a deep knowledge of the behaviors of the component. Fortunately, in practice the vast majority of the classes comes with a test suite containing exactly the operation calls with some signi cant instances as parameters.
The extraction of the signi cant instances is performed by collecting from the test suite all the objects passed as arguments in an operation call. Each value is then stored in an instance pool that collects all the values for each parameter. The values of the instances are stored directly in the instance pools, ready to be used in the exhaustive search. Instances collected from the test suite are very useful, but it happens that they may be redundant. To avoid the generation of models with a lot of states that do not unveil new behaviors, we should lter out the instances collected in order to keep a minimal subset able to exercise all the possible behaviors of the component without having to deal with a huge model. At this stage of the development, the tool is able to extract instances from a test suite but does not select the minimal subset of instances. This task is left to the user who has to nd the best trade-o between the number of instances used for the analysis and the completeness of the Bem generated. 3.2
Once the Bem is generated we can go further with the analysis and generate the corresponding Pbm. Generation is quite straightforward since the Bem already includes all the needed information about the outcome of each operation in each state of the model. Pbm inference algorithm consists of the following steps: i) generalization of the Bem states through the Pbm abstraction function; ii) introduction of each Bem transition in the Pbm. The generalization of the information contained in a Bem state is performed by applying to each state of the Bem the Pbm abstraction function we discussed earlier. Then for each transition of the Bem we add a transition to the Pbm starting from the representative of the equivalence class of the starting node in the Bem and ending in the representative of the destination node. Because parameters are ignored in the abstraction, the transformation is likely to produce a non-deterministic automaton: it may happen that, given a Pbm state, the invocation of the same operation with di erent values of the parameters produces di erent outcomes that turns into di erent destination states. 4
Bems and Pbms are used to perform runtime veri cation that the component, which may evolve independently, behaves accordingly to its models. To do so, we monitor the execution of an application and detect changes in the behavior of its components. Being able to detect changes is crucial when the application in which the component is embedded has to be self-adaptive and react to component misbehaviors in an appropriate way. More precisely, in this section we show that the data collected at runtime can be used on the one hand to enrich the model with previously unobserved behaviors and on the other hand to highlight behavioral di erences unveiling changes in the component under analysis. 4.1
A monitor is introduced into the running system to allow the comparison of the actual behavior of the component under analysis and the ones encoded by the models. Each time an instance of the scrutinized class is created, it is associated to it a monitoring process in charge of recording the observed execution trace and analyzing it to discover violations with respect to the protocol described by the model. Violation detection is performed by comparing the actual behavior with the one encoded in the model. Therefore it has to gather enough information to determine the state in which the component is. The system reports a violation when it nds an exceptional outcome for an operation that, according to the model, should always terminate normally or, on the opposite, when an operation that the model describes as exceptional does not throw anything.
In order to maintain the lowest overhead possible on the system under analysis, the violation detector relies, when possible, exclusively on the observed trace. When the Pbm has only deterministic transitions this process is straightforward and violations can be detected directly from the execution trace. Unfortunately, almost all components with a complex behavior are non-deterministic so there is the need of a deeper inspection by executing operations that could provide more information and thus reveal the state in which the component is. The solution proposed in this paper is an enhanced monitoring phase, not relying exclusively on what it is observable from the current execution but also able to perform some more queries to the object under analysis. For any state having non-deterministic outgoing transitions, we can determine which are the operations that make it possible to know which one has been taken. These discriminators are the operations on the destination states having di erent behaviors. Nondeterminism can therefore be solved by invoking the discriminating operations on the object under analysis. With these additional operations it is easy to nd the compatible state among the di erent nondeterministic possibilities. Discriminating operations have to be invoked on an instance of the object exactly in the same state of the actual component and should be tested with both the original instance pool and the instances observed in the trace for the operation. The original instance pool alone would not be so e ective as it would make it impossible to nd behaviors related to the parameter re-use.
Clearly it is not possible to call additional operations on the actual component under analysis. It would lead to interferences with the service provided by the system. Modi ers have undesirable side e ects but also the invocation of a pure operation could introduce delays and reduce the quality of service. In order be able to carry on the analysis without disrupting the o ered service, we need to assume that we can create a clone of the component behaving exactly in the same way the actual instance does. Moreover, the operations performed on such clone do not have to change the actual component environment. These assumptions reduce the number of components our methodology can deal with, but we are still able to monitor and analyze a vast class of commonly used elements.
Therefore the monitoring architecture requires: i) to instrument the application using the external services; ii) to have the possibility to call operations on a sandboxed instance of the service; iii) to be able to replay execution traces in order to put the sandboxed instance in a de ned state. With such an infrastructure, the veri cation module can detect changes in the behavior of external services without interfering with the actual execution of the system. 4.2
During the monitoring phase it may happen that an observation on the actual execution con icts with what it is described by the model. There are two possible causes for the violation observed: the model could be incomplete, and therefore needs to be updated, or the behavior of component has changed. The analysis phase has to be able to deal and react properly to both these situations.
It is possible to discover whether the violations is due to the incompleteness of the Pbm or to a change in the behavior by replaying on the clone some signi cant executions encoded in the Bem. If all of them produce again the previously observed results, then the model needs to be completed and that violations simply indicate behaviors never explored before. Otherwise the violation signals a misbehavior of the component that should trigger a reaction aimed at bringing back the system in a safe state.
In order to keep the approach feasible, we cannot just test that everything described by the Bem is still valid. We should rather focus on the part of the model more closely related to the observed violation. The rst step in the selection of the relevant execution traces is the identi cation of the Bem states corresponding to the state of the Pbm in which the violation occurred. The initial part of the test cases can then be generated by looking for the shortest execution traces able to reach the selected Bem states. The traces obtained in that way have then to be completed with the operation that unveiled the violation. For any Bem state the operation has to be called with all the parameters present in the instance pool used to generate the model.
Model updates have to be performed when the monitoring tool discovers a violation but there is no evidence of behavioral change. Models are updated because the behavior of the observed execution does not contrast with what has been observed in the past. Model updates are rst applied to the Bem and then to the corresponding Pbm.
Updating the Bem means enriching the scope it covers with the trace unveiling the new behavior. Keeping all the information in a single Bem would make its dimension increase, so we decided to rely on a set of Bems, each one describing a behavior of the component on the particular scope showing it. Doing that, we can easily keep track of all the relevant execution exposing the di erent behaviors. Although doing that we may miss some behavior due to the interaction of the behaviors described by di erent Bems, this is not an issue: the model will describe them as soon as they appear at run time. From the set of Bems it is easy to get the corresponding Pbm. It is quite straightforward to adapt the inference algorithm described in section 3 to deal with the information contained on more than a behavioral model: the algorithm has to be applied to each Bem and the data gathered have to be added to the same Pbm so that it contains information about all the observed behaviors regardless of the Bem it comes form. To produce correct abstractions for the new Pbm, all the Bems must have a coherent set of observers. To ensure that, we must update the scope for the observer roles in the already existing Bems to have them take into account all the signi cant values of the parameters discovered at run time.
A violation requiring to update the models of StorageService reported in
gures 1 and 2 happens when we try to write an empty string of data when no
entry is available. In such situation, the expected ZipException is not thrown
because the write operation does not have to write anything and the component
does not check for the availability of an entry. Therefore, we need to add a Bem
containing the observed trace. Since the violating trace contained a previously
unseen instance, we also have to update the existing Bem to have it consider
the empty string as a parameter for the write operation. For space limitations
the updated models and other examples are only available online at [
In the rst case, the change has to be noti ed but it does not require to stop the execution of the application. The detected change is probably just an addition of new functionalities or interaction patterns that previously were not present or were disabled. However, for safety reason it is better to leave to the user the nal decision about how to react to this kind of behavioral changes. More serious problems may arise form behavioral changes that turns the outcome of an operation from normal to exceptional. Such a change makes it impossible to substitute the new component to the one the system is expecting to deal with. At some point there may be an invocation to the operation that changes its behavior and it is going to always produce a failure due to the exception thrown. For this reason, when changes like this occur, the only safe solution is to stop the execution of the system requiring the intervention of a supervisor able to decide how to x the problem.
Change detection can be demonstrated using again the models reported in Figure 1 and 2 to monitor the behavior of a StorageService. For a very simple example we can assume that the component stops working and changes its behavior to always throw an exception every time putNextEntry is invoked. In this scenario, any execution of putNextEntry now violates the Pbm. We are interested to check if the violation is speci c to the trace observed or it is a component change; to check this, we derive the simple test case StorageService().putNextEntry(e1) from the Bem. Since this test case violates the Bem, it highlights the change of the behavior of the component.
A more comprehensive evaluation of the e ectiveness of the change detection
methodology has been performed injecting faults into the component under
analysis and is available online at [
It is important to remark that this methodology is able to identify changes only when there is at least one failing test case in the ones that can be derived from the Bem. Since the model does not contain information about every possible execution it is possible that an actual change is detected as a case in which there is the need to update the Bem and the Pbm because they does not contain anything about that particular case. However, since the updates to the model have to be reviewed by the designer of the system the procedure prescribed by our methodology can be considered e ective. 5
The protocol models discussed in this paper describe the behavior of a software
component accordingly to whether its operations are enabled or not. The
underlying idea has been introduced with the concept of Typestate in [
Tautoko [
Monitoring of both functional and non-functional properties of service-based
systems are described in [
Invite [
Tracer [
Behavior models can be useful throughout all the lifecycle of a software component. Traditionally, such models are used at design time to support system designers in they choices. However, they can also play a signi cant role after the application is deployed by monitoring its execution and checking system properties. That is particularly useful in the context of systems in which veri cation must extend to run time, because of unexpected changes that may occur during operation.
This work focuses on the runtime aspects, extending the original scope of behavior models to running systems. The models and methodology proposed can maintain an updated representation of the behavior of the component considering observations made during the actual execution of a running system. Our approach is also able to detect and notify the system designer behavioral changes in the monitored components. Preliminary experiments show that our approach is e ective and can deal with non-trivial components. Further research is going to enhance the models removing current limitations and thus making it possible to monitor an even broader class of software components.