Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



+44 (0)20 7594 8414a.lomuscio Website




504Huxley BuildingSouth Kensington Campus






BibTex format

author = {Gonzalez, P and Griesmayer, A and Lomuscio, A},
doi = {10.1109/ICWS.2012.31},
pages = {25--32},
title = {Verifying GSM-based business artifacts},
url = {},
year = {2012}

RIS format (EndNote, RefMan)

AB - Business artifacts allow to manage operations of business processes by capturing the key concepts and relevant information to guide their work flow. The Guard-Stage- Milestone (GSM) meta-model is a novel formalism for designing business artifacts that features declarative description of the intended behaviour without requiring an explicit specification of the control flow. Its concept of hierarchical structures of stages and explicit rules for the fulfilment of their guards and milestones supports the designing process but poses a challenge for formal verification. We show here how to approach the verification problem by developing a symbolic representation amenable to model checking. The feasibility of the approach is demonstrated by presenting a case study on the direct verification of a GSM model using a tool implementation. © 2012 IEEE.
AU - Gonzalez,P
AU - Griesmayer,A
AU - Lomuscio,A
DO - 10.1109/ICWS.2012.31
EP - 32
PY - 2012///
SP - 25
TI - Verifying GSM-based business artifacts
UR -
ER -