"Verification and Debugging of UML/OCL Models"
: International Workshop on Constraints in Formal Verification (CFV), 2015
Verification and Debugging of UML/OCL Models
Sprache des Titels:
International Workshop on Constraints in Formal Verification (CFV)
Motivated by the ever increasing complexity of today?s systems, designers more and more start to use modeling languages such as UML/OCL in order to (formally) describe a system to be realized. Once such a formal specification has been derived, the structure, the behavior, and the properties of the desired system can automatically be checked for correctness -- even in the absence of a precise implementation. Besides structural aspects (Is it indeed possible to instantiate a system considering all constraints?), also precise behavior (e.g. the reachability of bad states, good states, etc.) can be proven. To this end, automatic methods and approaches are available which will be reviewed in this talk. Besides that, also debugging methods are covered that, in case errors in the UML/OCL specification have been detected, help to identify the source of them.