Formal verification of business processes as role activity diagrams

Business process modeling is performed during the requirements analysis and specification of business software systems. Checking qualitative aspects of business processes is required for quality assurance, as well as for compliance with non-functional requirements. We show how business process models represented as Role Activity Diagrams can be formally checked using process algebras and temporal logics.