Search

Model checking is a well known technique for the verification of finite state models using temporal logic specification. While model checking is suitable for transformational systems (also called closed systems), it is unsuitable for open systems (also known as reactive systems) where the nondeterminism in the environment must be considered during verification. Module checking is an approach for the verification of open systems which have both closed (internal) and open (environment or external) states. It has been demonstrated in [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. Module checking. Information and Computation, 164:322–344, 2001] that the complexity of module checking branching time logic CTL is EXPTIME-complete. The approach to module checking is global and the method tries to establish that the property in question holds over all possible environments.This papers develops a local approach to CTL module checking using tableau rules. The proposed approach tries to determine a single environment under which the negation of the property is satisfied over the given module. Such a strategy, thus, leads to a local approach to module checking where we only explore states that are relevant to proving that the negation of the property can be satisfied over the given module using an appropriate witness (environment) that the algorithm also generates. While the worst case complexity of our algorithm is identical to the earlier complexity, we demonstrate that practical implementation of the proposed approach is feasible and yields much better results than the global approach.

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.

System-on-chip verification is an active research area. Of particular interest is protocol conversion, where two components with different protocols are controlled to communicate accurately. We present an approach to protocol conversion using model checking. The temporal logic ACTL is used to describe desired behaviour and finite state machines are used for protocol description. We use tableau-based converter construction and prove that a converter exists only when a successful tableau can be constructed. Liveness is incorporated so that converters satisfy additional constraints on protocol communication. A NuSMV-based implementation has been created and we present results on various problems including a large NuSMV example.