CMMI-CM compliance checking of formal BPMN models using Maude

From the perspective of business process improvement models, a business process which is compliant with best practices and standards (e.g. CMMI) is necessary for defining almost all types of contracts and government collaborations. In this thesis, we propose a formal pre-appraisal approach for Capability Maturity Model Integration (CMMI) compliance checking based on a Maude-based formalization of business processes in Business Process Model and Notation (BPMN). The approach can be used to assess the designed business process compliance with CMMI requirements as a step leading to a full appraisal application. In particular, The BPMN model is mapped into Maude, and the CMMI compliance requirements are mapped into Linear Temporal Logic (LTL) then the Maude representation of the model is model checked against the LTL properties using the Maude’s LTL model checker. On the process model side, BPMN models may include structural issues that hinder their design. In this thesis, we propose a formal characterization and semantics specification of well-formed BPMN processes using the formalization of rewriting logic (Maude) with a focus on data-based decision gateways and data objects semantics. Our formal specification adheres to the BPMN standards and enables model checking using Maude’s LTL model checker. The proposed semantics is formally proved to be sound based on the classical workflow model soundness definition. On the compliance requirements side, CMMI configuration management process is used as a source of compliance requirements which then are mapped through compliance patterns into LTL properties. Model checking results of Maude based implementation are explained based on a compliance grading scheme. Examples of CMMI configuration management processes are used to illustrate the approach.