Abstracting UML Behavior Diagrams for Verification

Abstract

UML (Unified Modeling Language) and XML (Extensible Markup Language) related technologies have matured, and at present many novel applications of both languages are frequently appearing. This chapter discusses the combined use of both UML and XML in the exciting application domain of software abstraction for verification. In particular, software development environments that use UML notations are now including verification capabilities based on state exploration. This method is effective for many realistic problems, although it is well known that it is affected by the state explosion problem for many complex systems and that some kind of abstraction is needed. This is the point where XML can be used as a powerful technology, due to its features for program transformation. We describe how to use XML-related standards like dom or xmi in order to extend UML verification tools with automatic abstraction.