Protocol-Safe Workflow Support for Santa Claus

Practical software analysis techniques exploit a form a process description, mostly in some avour of state diagram. Unlike typing information, these process structures are usually not passed down to the implementation level, and neither are they exploited in any form of consistency check. It is our belief that the information in most designs suffices to perform all sorts of consistency checks. This workshop paper studies a simple case where work ow processes interact with `actual' objects at the implementation level, and demonstrates how useful protocol checking can be in making and keeping these processes consistent with each other.