Debugging UML Designs with Model Checking

version of CD_PLAYER The verification with abstraction of events works as follows. Given a model M composed by a set of statecharts and a sequence diagram SD, we proceed by constructing and checking a more abstract model M* against an abstract sequence diagram SD* until deciding about the satisfaction of SD against M, or until finding specific errors (phases 2 and 3 in our proposed methodology). The abstraction in both diagrams is done using the same abstract events. The verification of undesired behaviors (Phase 3) is done directly: If M* does not verify SD*, then M does not verify SD. Therefore, M can be employed to continue the development cycle (e.g. code generation). For example, let us assume that the simulation of statecharts in Figure 2 exhibits too many unexpected errors, probably because it is a very early version. If we want to have a minimum confidence about its correctness, we could try to check sequence diagrams considering the number of events that the actor and the system send, without taking care about the events themselves. For instance, the sequence diagram in Figure 8 (left) shows a non-desirable SD (it is forbidden for this system to start the music automatically after inserting the CD; the user is required to explicitly push the button play.) Figure 8 (right) shows its corresponding abstract version (SD*). The model checker will now report that the system (using the statechart in Figure 7) will never produce a sequence of abstract events like the one in Figure 8 (right), and we could conclude that the initial system never produces a sequence like the one in Figure 8 (left). It is worth noting that the computational effort in verifying the abstract version has been reduced with respect to the verification of the initial model. In..