Please use this identifier to cite or link to this item:
Title: CMMI-CM compliance checking of formal BPMN models using Maude
Authors: El-Saber, Nissreen A. S.
Supervisors: Boronat, Artur
Heckel, Reiko
Award date: 1-Jan-2015
Presented at: University of Leicester
Abstract: 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.
Type: Thesis
Level: Doctoral
Qualification: PhD
Rights: Copyright © the author. All rights reserved.
Appears in Collections:Leicester Theses
Theses, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
2014ELSABERNPhD.pdfThesis1.22 MBAdobe PDFView/Open
MaudeModules.zipMaude Files43.51 kBUnknownView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.