Initial work in the design and development of verifiable Workflow Management Systems and some applications to health care

Workflows describe work processes as sequences of tasks and information regarding who performs them and their relative order. Workflows have been found useful to describe processes in a number of industries. This work focuses on workflows used in health care. Formal verification is the growing field of formalizing and verifying specifications for hardware and software systems. Many health care software systems are examples of safety critical systems and their proper function is required to protect the safety of the patients they manage. Formal verification can help assure this safety by checking work-flows before they are put into action, where errors can potentially seriously affect patients. A language for expressing properties that need to be verified is developed and a model checker is implemented. The implementation of the model checker written in XSB Prolog is presented.