Sciweavers

Share
ENTCS
2006

LSC Verification for UML Models with Unbounded Creation and Destruction

8 years 10 months ago
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.
Bernd Westphal
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Bernd Westphal
Comments (0)
books