mosco A BPMN choreography verifier: COnverts bpmn choreography MOdels to promela, includes ltl formulae and verifies them.