Show simple item record

dc.contributor.authorWang, Xiaoliang
dc.contributor.authorRutle, Adrian
dc.description.abstractWorkflows are used to organize business processes, and workflow management tools are used to guide users in which order these processes should be performed. These tools increase organizational efficiency and enable users to focus on the tasks and activities rather than complex processes. Workflow models represent real life workflows and consist mainly of a graph-based structure where nodes represent tasks and arrows represent the flows between these tasks. From workflow models, one can use model transformations to generate workflow software. The correctness of the software is dependent on the correctness of the models, hence verification of the models against certain properties like termination, liveness and absence of deadlock are crucial in safety critical domains like healthcare. In previous works we presented a formal diagrammatic framework for workflow modelling and verification which uses principles from model-driven engineering. The framework uses a metamodelling approach for the specification of workflow models, and a transformation module which creates DiVinE code used for verification of model properties. In this paper, in order to improve the scalability and efficiency of the verification, we introduce a new encoding of the workflow models using the Alloy specification language, and we present a bounded verification approach for workflow models based on relational logic. We automatically translate the workflow metamodel into a model transformation specification in Alloy. Properties of the workflow can then be verified against the specification; especially, we can verify properties about loops. We use a running example to explain the metamodelling approach and the encoding to Alloy.en_US
dc.relation.ispartof<a href=""target="blank">Towards Correct Modelling and Model Transformation in DPF</a>en_US
dc.rightsAttribution CC BY-NC-ND 3.0eng
dc.subjectWorkflow modellingeng
dc.subjectEfficient verificationeng
dc.titleModel Checking Healthcare Workflows Using Alloyen_US
dc.typeJournal article
dc.typePeer reviewed
dc.rights.holderCopyright 2014 The Authorsen_US
dc.source.journalProcedia Computer Science
dc.subject.nsiVDP::Matematikk og Naturvitenskap: 400en_US

Files in this item


This item appears in the following Collection(s)

Show simple item record

Attribution CC BY-NC-ND 3.0
Except where otherwise noted, this item's license is described as Attribution CC BY-NC-ND 3.0