Nástroj pro ověřování programů v jazyce BPEL, kontroluje shodu implementace webové služby (BPEL) s formálně specifikovaným modelem chování (BP).
