Electronic Notes in Theoretical Computer Science · 2001 · 34 citations · 10 references
ComputingComputer ScienceDiagrammingFormal MethodsSystems ModelingModel-based DesignModel-driven DevelopmentPetri NetsSpecification LanguagesDynamic ModelsHigh-level Petri NetsPetri Net ModelsPetri Net SemanticsStandard NotationStandardizationTimed Petri NetsUml Modeling
UML is the OMG standard notation for object-oriented modeling. It is easy, graphical and appealing, but in several cases still too imprecise. UML is strong as modeling means, supplies several different diagrammatic notations for representing the different aspects of a system under development, but lacks simulation and verifiability capabilities. This drawback comes from its semi-formal nature: UML is extremely precise and wide if we consider syntactical aspects, but its semantics is as precise as those of informal notations. Scientists and users, together with standardization efforts (UML 2.0), are trying to overcome this problem, but as side effect, they are also limiting the intrinsic flexibility of UML. Moreover, several formalization efforts concentrated on its static elements (for example, inheritance), leaving dynamic semantics almost untouched. In this paper we propose the paring of UML dynamic models with high-level timed Petri nets (HLTPN) to obtain a flexible and customizable means to reason on the dynamic aspects of object-oriented models, to simulate particular parts of these models, and if necessary analyze them. The proposal exploits rules to ascribe main UML elements with formal semantics in terms of functionally equivalent HLTPNs and to show results (from execution and analysis) as decorations to UML symbols. Besides sketching the approach, the paper presents also some experiences we have gained so far with it and a research agenda to identify other possible uses of the dual definition of the notation.
10
Daniel Jackson · ACM Transactions on Software Engineering and Methodology · 2002 · 1.2K citations
vUML: a tool for verifying UML models
Johan Lilius · 2003 · 225 citations
An Invitation to Formal Methods
Jonathan P. Bowen, Ricky W. Butler, David L. Dill et al. · Computer · 1996 · 134 citations