查看文章

Object-oriented methodologies are increasingly used in software development. Despite the proposal of several formally based models, current object-oriented practice is still dominated by informal methodologies, like Booch, OMT, and UML. Unfortunately, the lack of dynamic semantics of such methodologies limits the possibility of early analysis of specifications.

This paper indicates the feasibility of ascribing formal semantics to UML by defining translation rules that automatically map UML specifications to high-level Petri nets. This paper illustrates the method through the hurried philosophers problem, that is first specified by using (a subset of) UML, and then mapped onto high-level Petri nets. The paper indicates how UML specifications can be verified by discussing properties of the hurried philosophers problem that can be verified on the derived highlevel Petri net.