LSC Verification for UML Models with Unbounded Creation and Destruction

The approaches to automatic formal verification of UML models known up to now require a finite bound on the number of objects existing at each point in time. In [4] we have observed that the class of hardware systems with replicated components studied by McMillan [10] is equivalent to the class of systems with unbounded creation and destruction and all other data-types finite. Exploiting the symmetry of UML models induced by objects being instances of classes, the retriction to finite bounds can be overcome applying [10]. In this paper we report on experiences from an evaluation of this approach within the Rhapsody UML Verification Environment, a state-of-the-art tool for formal verification of UML models using Live Sequence Charts for requirements specification. Key words: Formal Verification, Infinite-state, UML, LSC.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Bernd Westphal
• Keywords: Automatic Formal Verification, ENTCS 2006, Formal Verification, UML Models