Object-oriented (OO) methods have been widely used in software industry and military applications. The second generation OO method called Unified Modeling Language (UML) developed by a group of OO methods design experts based on past success experience has become the standard OO notation. The main success factors of OO methods include simple conceptual models closely matching real-world entities, well-understood development heuristics and process, and high potential for software product re-use. However like other informal methods, UML lack precise semantics and thus does not support formal analysis.

In this research project, we propose to investigate the relationships between UML and a formal method called hierarchical predicate transition nets (HPrTNs) based on Petri nets. First, we will use HPrTNs to define the formal semantics of UML, and then we will develop a derivation methodology from UML specifications to HPrTN specifications based on the formal semantics. The derivation approach will consist of an overall derivation architecture with a set of derivation rules, and will be validated using a set of correctness criteria and evaluated through several case studies.

The derivation methodology will retain the advantages of UML and assure their quality through analyzing the derived HPrTN specifications. The derivation methodology will establish the foundation for reuse and composing existing informal specifications through their common semantics in HPrTNs, and the basis for formal implementation derivation. The experience gained in this research project will be useful for facilitating and promoting the application of other formal specification methods. Another potential benefit of this project is to facilitate the dual use of technology, i.e. the results obtained from this research can be applied to both military and civilian software systems.