VERIFICATION OF HAMMOCK TYPE PROCESSES

摘要

We show a polynomial-time algorithm to verify the partial correctness of Hammock processes w.r.t. given input/output assertions. Earlier work developed a framework for modeling distributed systems (e.g., computing, manufacturing), with Hammock processes as a subclass of processes that have single start and end nodes. This framework has been implemented in a software toolset for process design, the PROCESS BUILDER, where the verification algorithm presented here is currently being integrated.