In many industries, such as finance and insurance, business processes represent products which need to be rolled out to customers within a strict deadline, e.g. new insurance policies. The products are also supposed to be modifiable during their period of service and should be verified and tested before being placed in service. In these industries, being able to create a new process or to change one quickly is providing one competitive advantage; carrying out business processes efficiently provides another. Rapid business process prototyping, in this case, is a practically motivated approach.

This contribution presents a realistic business process modeling, verification, and prototyping framework by means of a formal Petri net-based specification language. By specifying process models using this language, executable process controllers can be automatically generated and smoothly integrated into a service-oriented architecture. Furthermore, formal verification techniques and tools can be used to detect errors during the design phase of the process.