A pragmatic formal method (PFM) for computer system definition and execution

The pragmatic formal method (PFM) process produces a model of a to-be-built target system, provides analysis of model quality, and simulates system operation. PFM incorporates a solution to one of the major problems with Petri nets, i.e., a static Petri net structure of a large system is difficult to define. A formal extension of Petri nets called PFM-nets (nets of interacting PFM functions) is used to simulate system operation and support the development of a rapid prototype. PFM-nets can be generated (in theory) automatically from a PFM model of a target system. The PFM model and model execution are discussed