The tree-like local model update with domain constraints

Abstract

Model update is the logical extension of model checking, allowing automated modification to models found not to satisfy a given property in the checking process. In local model update, counterexamples are derived from model checking sessions where some ACTL formula has been found unsatisfied. By updating the localised models to satisfy the underlying property, we may derive modifications to the original global model. Constraints also play an essential role in describing allowable system behaviour. Variable and action constraints can be defined which describe allowable updates on a counterexample in the update process, extending developer control over what is a valid update on the original system. In previous attempts, methods of update required the processing of the entire model. With larger scale industrial models, this was not feasible due to the inherent complexity. Further, constraints placed on the model in question were not addressed, and as such critical functionality could be circumvented (e.g. breaking a resource deadlock using some method should not cause some critical functionality of the module to cease functioning). In this dissertation, the foundations of ACTL tree-like local model update are thoroughly studied. We define necessary elements of ACTL local model update, describing ordering metrics for determining which updates are simpler with respect to weak bisimulation ordering. Further to this, we look at the link between local model update and belief revision, semantic characterisations for typical updates, analyse the complexity for general cases of update and present the theory underlying constraint automata.

Date of Award	2011
Original language	English