CASSANDRAOSGi

CASSANDRA is then based on a run-time checking algorithm that takes in input the interface automata for the various components, the look-ahead value 𝑘, the temporal property that should not be violated by the system:
The interface automata of the various components are composed on the fly to construct the tree of possible paths of length smaller than k,
When a system interaction event is detected the exploration is moved ahead of one step. In particular:
All the subtrees rooted in a next state linked by an event different from the one detected are discarded;
For each leaf in the subtree rooted in the next state linked by the detected event, the exploration is pushed ahead of one step;

We customize CASSANDRA into the OSGi component model and framework.
The OSGi bundle developers provide the architecture with a set of wrappers of bundles (each wrapper is equippe