Our main objectives on formal method research are to adapt and enhance well-defined formal models so that they can be effectively applied in software engineering practices. In the past decade, we have concentrated on a specific formal model, Petri nets, for specifying concurrent and distributed systems. We have obtained many significant results including (1) the development of hierarchical predicate transition nets, (2) the integration of high-level Petri nets with other formalisms - algebraic specifications, temporal logic, and Z, (3) specification development methods based on modern structured analysis and object-oriented analysis, (4) several formal property analysis techniques for high-level Petri nets - a temporal logic approach, a structural induction approach, and a behavioral transformation technique, and (5) several code generation techniques from hierarchical predicate transition nets to CC++ and Java programs.