BPMN and Activiti

A quick guide: http://www.nurkiewicz.com/2011/01/activiti-processes-and-executions.html

BPMN is easy to be transformed to petri net for formal analysis.