Adaptive Verification using Forced Simulation

Simulation (a pre-order) over Kripke structures is a well known formal verification technique. Simulation guarantees that all behaviours of an abstracted structure (a property or function, F) are contained in a larger structure (a model M). A model, however, may not always simulate a property due to the presence of design errors. In this case, the model is debugged manually. In this paper, we propose a weaker simulation over structures called forced simulation for automated debugging. Forced simulation is applied when normal simulation fails. Forced simulation between a model (M) and a function (F) guarantees the existence of a modifier, D, to adapt M so that the composition of M and D is observationally equivalent to F. Observational equivalence over structures called weak bisimulation is developed in this paper. It is also established that when two structures are weakly bisimilar all CTL^* properties holding over one also holds over the other structure. Forced simulation based algorithm has been used to adapt many designs which had failed certain properties during conventional verification.