Runtime Monitoring of Functional Component Changes with Behavior Models

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 (dy- namic model update). We also use the inferred model to perform run- time verification. 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.