Verifying Linear Temporal Logic Properties in UML/OCL Class Diagrams Using Filmstripping

Testing system behavior in real world applications often requires analyzing properties over multiple system states to ensure that operations do not interfere with each other in ways that are not desired. In UML class diagrams, behavior is specified using operations with pre-and postconditions, which alone are not sufficient to formulate temporal properties spanning multiple system states and, thus, require additional description means. For this purpose, multiple extensions of OCL with linear temporal logic (LTL) exist, which provide a formalism to describe temporal properties. Using so-called filmstrip models, this paper provides formal semantics for OCL enhanced by LTL through a translation into standard OCL on the basis of class diagrams and enables verifying these temporal properties using existing model checking tools.