Download Paper - STS

7 Conclusion
7 Conclusion
The aim of this project was to implement a model repairer for CTL properties in NuSMV.
Since Zhang and Ding build their update functions on five basic operations that can
arbitrarily modify the given Kripke model, these basic operations had to be implemented
into NuSMV. It turned out that this is impossible for some of them in their original form.
While it was no problem to implement the basic operations for the modification of the
transition relation, the addition and removal of states proved to be hard. Furthermore,
changing the label of a state is impossible as the label is implied by the state and not
assigned to the state in NuSMV. Hence, the next step was to adapt these basic operations
to make them compatible with NuSMV. In the case of relabelling a state, it was solved
by replacing the current state with another one that already has the appropriate label.
This is possible as the states for each satisfiable label combination already exist for SMV
models. However, this is a problem in itself as the other state may already have incident
transitions. Hence, using such a state as a replacement state breaks the abstraction of the
basic operation for state relabelling. The next basic operation to adapt was the addition
of a new state. The problem is that NuSMV uses BDDs to verify CTL properties.
The states are given by the minterms of the respective BDDs. Since each possible
minterm already represents a specific state, creating a new state requires to introduce a
new boolean variable in the BDDs. The new variable creates additional minterms that
represent the new states. However, this leads to the serious problem that all existing
BDDs in NuSMV are implicitly changed (i.e., the states sets that they represent). Hence,
after each application of the adapted basic operation, the model repairer has to correct
all existing BDDs. This holds for the creation of a new state as well as for the change
of the label of a state. That is the reason why neither relabelling a state nor creating
a new one are realised in the prototypical implementation of the model repairer. The
prototype repairs models by modifying the transition relation only. The supported CTL
subset corresponds to the AEClass properties. Hence, nesting temporal operators is not
allowed. Regarding the supported language features of NuSMV, the prototype assumes
that there are neither fairness constraints, input variables, nor sub-modules given. These
limitations make it difficult to solve real world problems with the prototype. However,
at the same time it shows that model repair is possible in NuSMV.
44