# Designing Quality Business Processes for E-Government Digital Services

Flavio Corradini, Damiano Falcioni, Andrea Polini, Alberto Polzonetti, Barbara Re

► To cite this version:

Flavio Corradini, Damiano Falcioni, Andrea Polini, Alberto Polzonetti, Barbara Re. Designing Quality Business Processes for E-Government Digital Services. 9th IFIP WG 8.5 International Conference on Electronic Government (EGOV), Aug 2010, Lausanne, Switzerland. pp.424-435, 10.1007/978-3-642-14799-9_36. hal-01056569

HAL Id: hal-01056569

https://inria.hal.science/hal-01056569

Submitted on 20 Aug 2014

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Designing Quality Business Processes for e-Government Digital Services

Flavio Corradini, Damiano Falcioni, Andrea Polini,
Alberto Polzonetti, Barbara Re

Computer Science Division – School of Science and Technologies
University of Camerino
62032 – Camerino (MC), ITALY
{firstname.lastname}@unicam.it

**Abstract.** Research works and surveys focusing on e-Government Digital Services availability and usage, reveal that often services are available but ignored by citizens. In our hypothesis this situation can be justified since defined service delivery processes do not sufficiently take into account social aspects and mainly focus just on technical aspects. Domain knowledge, related to how delivering high quality e-Government Digital Services, remains in most of the case in the mind of e-government stakeholders.

To address these issues we have developed a quality framework to assess delivery process strategies of services. Moreover we have introduced a user-friendly approach permitting to assess, using formal verification techniques, a delivery process with respect to the defined quality framework. The approach has been also implemented in a plug-in for the Eclipse platform and it has been applied to real case scenarios from the Public Administration domain.

In this paper we report and discuss the results we obtained from the conducted experiments. First of all the experiments provided encouraging results confirming that the approach we developed is applicable to the e-government domain. Moreover we discovered that delivery processes, defined for the services under study, reach low quality marks with respect to the framework.

## 1 Introduction

The e-government domain is characterized by the involvement of many stakeholders with different interests and competences. Among the others we can list citizens, civil servants, managers and politicians. Each of them provides multiple viewpoints on Public Administrations (PAs) needs, objectives and qualities. So for a politicians the objective is to maximize PA efficiency providing services that are highly used at minimum costs, where for citizens the objective would be to maximize service availability and usability leaving aside possible costs. Nevertheless if we consider the current situation of e-Government Digital Services (GDSs) we can say that services are available but not highly used. So the effort
of the politicians toward the introduction of ICT technologies in the PA did not
get really good results.

Our opinion here is that, in the development of GDSs, the focus has been
put too much on technological aspects, where requirements coming from social
and antropological domains have been too often ignored. As a result services
are available and often they rely on advanced technologies, nevertheless they are
not used since citizens do not grasp the advantage of using it, and in particu-
lar in less urbanized areas, they feel more confortable in accessing services via
traditional channels. Certainly the digital divide contributes to such a situation.
Nevertheless our impression, corroborated by an informal investigation among
the people working in our department and with high ICT skills, is that other
important factors strongly contribute to the underlined scenario.

In our view it is important to concentrate on aspects and requirements that
are not only technological. Therefore, structuring the delivery process of a GDS
just replicating the process already in place in the PA could pose some issues,
not leading to the expected results. For instance it is necessary to consider that
interacting with the PA via an eletronic mean does not bring the same level of
trustworthiness with respect of an interaction mediated by the civil servant. This
aspect should be certainly considered when structuring the delivery process of a
GDS.

Therefore in the delivery of a GDS at least two different kinds of knowledge
need to be codified. The first concerns the specific service to be provided to the
citizens. This is may be less critical since directly relates to the service that is
under development. The second knowledge is instead more general and refers to
any kind of service developed within the domain and in particular it can relate
to social and anthropological aspects. Both aspects are equally important to
derive highly used services. In this line we have defined a quality framework [1]
which classifies the delivery process of a GDS. The framework intends to codify
properties that a general delivery process of a GDS should satisfy. So in order to
increase trustworhiness the framework requires that some kind of transparency
on the process execution evolution is implemented. This functionality would
permit to the citizen requiring the service to obtain feedbacks and to observe
how the service he/she requested is progressing. This will obviously result in an
increased trust.

Certainly the codification of domain and quality requirements can per se pro-
vide a useful tool to Business Process (BP) analysts. Nevertheless it turned out
that the requirements constituting the framework could be translated in tempo-
ral properties. Therefore we implemented a tool [2] permitting to automatically
verify and classify, applying model checking techniques, that a designed GDS
delivery process satisfies the properties defined in the quality framework. Cor-
respondingly it ranks the process with respect to the different levels defined in
the framework.

In this paper we discuss on the importance of codifying the different kinds
of knowledge and at the same time of having tools supporting such an activity.
Moreover we report on experiments we conducted applying the framework and
using the corresponding tools on real GDS delivery processes implemented by
a local administration. In particular in the next section we report on related
works, and then in Section 3 we discuss about knowledge codification in the
e-Government domain. Section 4 introduces a tool supporting BP analysis and
Section 5 shows how the approach and the tool have been applied in practice.
Finally Section 6 draws some conclusions and opportunity for future work.

## 2 Related Works

The importance of fully functional e-government characterized by vertical and
horizontal integration is clearly discussed in [3]. From our point of view the real
benefits which e-government promises can be reached when system integration
is implemented. The introduction of BP specification can contribute to such
integration. Indeed BP potentialities and capabilities are relatively unexplored in
e-government. An interesting survey dealing with issues in the application of BPs
to e-government can be found in [4]. As far as we know the most comprehensive
discussion on e-government business models is proposed by Janssen and Kuk [5].
In this work the authors address the importance of cross-organizational service
delivery and propose a framework for studying e-government business model
which involves design and implementation of digital services toward the delivery
to citizens. Our contribution considers the role of business model as addressed by
Jansen and Kuk and it introduces characteristics that are directly process related
considering an automatic and systematic approach toward BP improvement and
e-government integration.

For what concern the application of mature formal techniques in applied
fields of study such as e-government literature shows a quite wide interest. A
first discussion on the topic can be found in [6]. This paper is the result of a
tutorial-workshop event on technological foundations of e-governance. Our paper
contributes to the outcome of the event exploring and validating how model
checking can be applied to evaluate service quality.

Other proposals provide user-friendly techniques hiding the complexity of
formal languages and tools. A recent survey on Business Process verification
provides an interesting classification of proposed techniques [7]. There are for
instance interesting approaches aiming at making model checking accessible to
a large audience even for people that are not trained in formal techniques [8] [9]
[10] [11] [12] [13]. However in most of the case they lack of a domain-dependent
requirements framework for BP evaluation and the verification step just consid-
ers typical properties such as deadlock, and liveness. Moreover, in most of the
case proposed approaches need stand alone tools (for BP modelling, mapping
and verification). Such tools can be used only by people with wide technical
background. Our contribution provides an integrated development environment
for GDS design so that such issues can be solved.

To the best of our knowledge our approach is the first attempt, within the
e-government domain, that tries to provide an easy to use environment both
for BP design and BP evaluation with respect to a precisely defined quality
framework.

3 Domain Knowledge Codification and Verification

Providing successful GDS is a quite complex task. Requirements come from
many different sources and the implementation often foresee the interactions
of many different PAs. Technically GDS are modeled and implemented using
notations and tools based on the Business Process concept. "A Business Process
is a collection of related and structured activities undertaken by one or more
organizations in order to pursue some particular goal. Within an organization
a BP results in the provisioning of services or in the production of goods for
internal or external stakeholders. Moreover BPs are often interrelated since the
execution of a BP often results in the activation of related BPs within the same
or other organizations" [14]. In addition to the BP concept Business Process
Management (BPM) supports BP experts providing methods, techniques, and
software to model, implement, execute and optimize BPs which involve humans,
software applications, documents and other sources of information [15].

Unfortunately too often BP analysts in the e-governement domain mainly focus on requirements concerning the specific service under development and forget to consider general requirements coming from the e-government application domain. Moreover, modeling BPs is in general a time-consuming and error-prone activity. Therefore, techniques which help organizations to implement high-quality BPs, and to increase process modeling efficiency have become an highly attractive topic both for industries and for the academy. As illustrated in the following our approach contributes to this topic providing a method, and supporting tools, to codify domain knowledge and to use such knowledge in the verification of a defined BP.

**3.1 Domain and Quality Requirements**

Domain requirements intend to highlight aspects of a particular application do-
main that are tipically not know to BP and technical experts, and that are in-
stead quite obvious for domain experts. Missing to report domain requirements
generally results in a project failure or in low quality systems. The discovery of
domain requirements is particularly critical in the e-government domain where
the software to implement is directed to citizens with ample differences in the ca-
pability of operating with Information and Communication Technologies (ICT),
and in the distrust they have with respect to such technologies. In developing
services for the PA becomes then mandatory to consider and codify require-
ments aiming at removing such possible hurdles in service acceptance. Never-
theless such knowledge is not in the mind of BP or technical experts. Instead
it can be provided by people with expertise in social and anthropological fields,
that then have to be involved in the requirements discovery phase, and helped
in expressing the requirements they think the software system should satisfy.
The framework we have defined have been developed taking into account these
aspects. For further detail on its definition we refer to [1].

The defined framework considers the following dimensions:

1. *Coordination* is a four level requirement concerning the capability of two or more Public Administrations to work together to accomplish common goals, through the delivery of a service to a citizen and using ICT technologies.

2. *Control* is a four level requirement concerning the activation policies suitable to drive the GDS delivery from its start to the final fulfillment.

3. *Sharing* is a two level requirement that refers to the way in which the PA handles and shares citizen data with other administrations in order to participate in the delivery of a specific GDS.

4. *Transparency* is a three level requirement able to drive the ability of the administration to make citizens aware of the delivery process, improving citizens' perceived trust.

5. *Inclusion* is a three level requirement that considers the ability of the administration to provide service to the citizens considering the diversity.

The framework we defined can be considered just a possible example and certainly other set of general domain requirements for GDS can be identified.

## 3.2 e-Government Digital Service Specification

The knowledge related to the delivery, as for other aspects, of a specific e-Government Digital Service should codified via a participative approach where every stakeholder contributes with his/her viewpoint. In fact in the general case a GDS can involve many different PAs that will assume different roles within the resulting BP. Furthermore there are many stakeholders, such as politicians, that are interested in the GDS development even though they do not directly participate to its execution. Collecting all the requirements can be a quite difficult task and the requirements directly related to the specific GDS under development have to be complemented with those related to the domain as we discussed above.

Given the inherent complexity of GDS related BPs, it becomes particularly important to provide and set up mechanisms and tools permitting to support the various BP design activities. Particularly interesting is the possibility of applying automatic verification approaches to assess if high level requirements are satisfied by the BP specification.

As it will be illustrated in the next section for the case of GDS delivery processes, we provide a tool encompassing different BPM activities. In particular the domain quality framework described above has been codified as assertions and it is possible to automatically check their validity on BPs under development.

# 4 Quality of GDS Delivery Processes

Starting from domain knowledge, the introduction of an approach and a supporting tool permitting to formally and automatically assess the quality of a
designed BP, with respect to the defined quality requirements, is an interest-
ing challenge to be addressed. In this section we outline the main elements of
the defined user-friendly approach permitting to assess, using formal verification
techniques, a GDS delivery process with respect to the defined quality frame-
work.

## 4.1 Technical Background

Different classes of languages to express BPs have been investigated and defined. Among the others Business Process Modeling Notation (BPMN) [16] is certainly the most used language in practical context also given its intuitive graphical notation. Nevertheless BPMN does not have a precisely defined semantic. For this reason, and in order to permit formal verification we defined a mapping of BPMN constructs to CSP processes [17].

CSP is an event based notation primarily aimed at describing the sequenc-
ing of activities within a process and the synchronization (or communication)
between different processes. Events represent a form of co-operative synchro-
nization between CSP processes and the environment. Both the processes and
the environment may influence the behavior of the other by enabling or refusing
certain events or sequences of events.

Formal verification is the act of proving or disproving the correctness of a
system with respect to given properties. Many different approaches are available,
nevertheless our interest is mainly in model checking techniques [18], which con-
sist in a systematic, and when possible exhaustive, exploration of an operational
model to verify if it satisfies a set of given properties. Many model checking tools
have been proposed and developed in the literature. In our work we integrate
the PAT model checking [19] due to its flexibility and since it uses the CSP
formalism as input language.

## 4.2 BP4PA From An Approach to a Tool Chain

The use of formal mechanisms to verify properties of complex BPs has been al-
ready advocated by other authors (see for instance [11]). Our work aims at pro-
viding to BP and domain experts the power of formal verification techniques still
allowing the use of graphical notation with which they are already acquainted.
The approach, which is sketched in Figure 1, relies on the following three main
steps: (i) Business Process *specification* and quality requirements selection via a
user-friendly notation as already introduced in the Section 3; (ii) *Mapping* of a
process specification and of a set of quality requirements to CSP processes and
to a set of goals, respectively; (iii) Formal *verification* of defined processes with
respect to specified set of requirements (goals).

In case the verification phase ends highlighting some problems, i.e. at least
one of the property defined by domain experts results to be violated, the process
should be restarted.

For what concerns the precise semantic a GDS specification we have defined
a mapping of BPMN elements to CSP processes. Our mapping covers all the
<figure><img src="image_2.png" /><figcaption>Fig. 1. BP4PA - The Proposed Approach</figcaption></figure>

core BPMN elements and almost all the elements introduced by the OMG no-
tation. Few constructs dealing with transactions, such as compensation events
and cancel events, or time have been kept outside. Main reason for this choice is
that they are seldom used in practice [20] at least in the e-Government domain.
The mapping has been defined according to the following general principles:

- Each BPMN graphical object included within a pool is formally represented by a CSP process or a parallel execution of generated CSP processes - we name such process *Element CSP*.

- Each pool is mapped to a parallel composition of *Element CSP* processes with barrier synchronization. In this case no message exchange will be observable - we name such process *Private CSP*.

- The whole process results from the parallel execution of the *Private CSP*
processes including their interactions implemented via messages exchange -
we name such processes *Abstract CSP*.

Due to lack of space we do not detail each mapping rule and we refer to [21] for
a wider discussion.

Moreover we defined additional constraints on the definition of the BP both
to make the verification step easier, and to make BP specifications clearer. So
for instance loops can be introduced only using the specific BPMN constructs.
Implicit loops are not admitted. Somehow this constraints ban sort of *goto*
statements from the specification. Moreover another constraint requires that
tasks receive or send messages but they cannot do both things. BPs modeled
according to the defined constraints can be mapped into CSP models to be
successively processed by the model checker.

In addition to the BPMN constructs also the quality framework described
in Section 3 has been mapped to a formal notation. All the qualities, in the
framework we have defined, turned to be expressible as temporal properties. The
verification phase is based on model checking techniques. Reachability analysis is applied in order to assess whether the goals that are generated from the properties specification are fulfilled or not.

The formal verification approach is supported by a plug-in (Business Processes for Public Administrations - BP4PA) available for the Eclipse Framework that can be freely downloaded at the BP4PA web page. The plug-in permits to have a fully integrated and user friendly environment which supports domain experts both in the BP specification phase, and in the verification phase. In particular our plug-in is integrated in an Eclipse extension such as the BPMN modeler, and it uses the functionalities of the PAT model checker [19]. The CSP model is derived taking advantage of the Eclipse Modeling Framework (EMF) which is a powerful mechanism available within the Eclipse platform to define meta-models. EMF, together with other frameworks enabling the graphical rendering of the BPMN constructs, is at the base of BPMN modeler. Therefore through EMF, and its API, it is possible to interact with the defined BPMN model to retrieve the list of elements which have been included within a BPMN specification. In this way it is possible to implement a simple parser that for each BPMN element generates the corresponding CSP code, using in our case the syntax of the PAT model checker, and according to the mapping rules. Similarly the code generation includes the specification of variables enabling the checking of relevant quality requirements. After that the transformation of the BPMN specification to the corresponding CSP model has been carried on the verification step can take place. To make also this step easier we integrated the PAT model checker within the Eclipse framework. As a result the whole tool-chain is integrated in a unique integrated development environment. The techniques we used to implement the framework make easy its extension with new properties.

# 5 BP4PA in Place

Thanks to a close cooperation between our research group and a local Public Administration we applied our approach as well as the tool in practice.

## 5.1 General Considerations

As for any approach using model checking techniques it is important to check if the state explosion phenomenon could hinder its applicability to real case study. In our case we experimented with ten real processes and all of them have generated relatively small state sets. In particular the experiments we have conducted using a desktop PC equipped with a Core 2 Duo 2,20GHz and 4GB RAM, have highlighted that defined BP can be checked with respect to the properties included in the framework in less than 60 minutes, for the most complex BP scenarios. Moreover the most complex BP generated a state space of around three millions states. This data seems to support the idea that in the current status (i.e. complexity of BP processes in the e-government domain, mapping we have defined and quality properties to be checked) the approach is applicable in real
scenarios and can be a useful support for the BP designer. In Table 1 we report a part of the conducted experimental results. It refers to EU based service in line with Italian law and our local scenario.

<table><caption>Table 1. Experimental Results</caption><thead><tr><th>Service Name</th><th>Num. of States</th><th>BPMN elem.</th><th>Coord. (sec)</th><th>Control (sec)</th><th>Sharing (sec)</th><th>Transp. (sec)</th><th>Inclusiv. (sec)</th></tr></thead><tbody><tr><td>Car registration</td><td>3.065.595</td><td>66</td><td>1629,18</td><td>3254,22</td><td>3280,48</td><td>1631,28</td><td>4896,25</td></tr><tr><td>Passport Request</td><td>735.785</td><td>68</td><td>594,28</td><td>596,08</td><td>2368,12</td><td>590,17</td><td>1777,94</td></tr><tr><td>Enrollment in education</td><td>44.963</td><td>45</td><td>33,88</td><td>100,85</td><td>67,75</td><td>33,50</td><td>100,59</td></tr><tr><td>Declaration to police</td><td>32.333</td><td>43</td><td>14,14</td><td>19,60</td><td>27,60</td><td>13,70</td><td>41,17</td></tr><tr><td>Social Contribution</td><td>19.398</td><td>42</td><td>18,59</td><td>19,51</td><td>38,35</td><td>10,37</td><td>28,68</td></tr><tr><td>Social security benefits</td><td>14.295</td><td>43</td><td>10,12</td><td>9,89</td><td>9,93</td><td>4,90</td><td>14,69</td></tr><tr><td>Job search</td><td>4.044</td><td>31</td><td>3,36</td><td>4,68</td><td>3,03</td><td>1,50</td><td>4,52</td></tr><tr><td>Health-related services</td><td>2.451</td><td>36</td><td>1,98</td><td>1,84</td><td>1,78</td><td>0,88</td><td>2,62</td></tr><tr><td>Public libraries</td><td>333</td><td>18</td><td>0,28</td><td>0,12</td><td>0,07</td><td>0,06</td><td>0,17</td></tr><tr><td>Customs declaration</td><td>204</td><td>20</td><td>0,20</td><td>0,11</td><td>0,10</td><td>0,05</td><td>0,14</td></tr></tbody></table>

The study has also highlighted that all the defined BPs reach low quality levels for all the quality dimensions in the framework. Given that the studied services are seldom used by citizens the defined framework does not contradict itself. Considering transparency, that may be the most intuitive dimension in the framework, the tool reported that no information were provided, through a message flowing from the PA to the citizen, between the start and the end of the process.

Starting from the evaluation of the processes reported by BP4PA we started to revise the various BPs in order to derive BPs getting higher marks.

## 5.2 Moving Service

The approach has been used to improve the delivery process associated to the moving service. This is part of the wide area of cooperation among civil registration services. The service permits to an Italian citizen, which has to move to a different municipality, to be registered, to get updated certificates and any other service regardless of its new geographical location. In particular the service under analysis supports in the most comfortable way the registration of a new address, delivering at the same time the request for updating relevant information reported in the driving license. Moreover such service supports the alignment of the information in all the Public Administration offices dedicated to trace moving of citizens.

As many other GDSs, the moving service foresees the interactions of many stakeholders. In particular: (i) The municipality where citizens has to be registered. This can be further decomposed in registry office, local police office and tax office (ii) The Home Affairs Minister deputed to collect and to maintain up to date the information related to citizens using the INA/SAIA infrastructure (iii) Tax Office is the national organization in charge of controlling the status of the
Italian citizens with respect to tax obbligations (iv) CISIS (Italian inter-regional center for information, statistical and geographical systems) is the association of regional authorities which, among a list of several activities, has to collect all the information requested for statistical purposes (v) INPS is responsible of the pension system. It is deputed to collect and maintain up to date the information related to the social citizens status (vi) Transport Office is the national association devoted to control the traffic for what concerns driving licenses and policies.

The GDS is implemented roughly applying a six-steps process: (i) The citizen asks for activating and accessing the moving service. It is worth mentioning that the access can be provided at the municipality office or via Web when suitable authorizations and authentications mechanisms are set; (ii) The registration municipality collects the information from the citizen; (iii) The registration municipality sends such data to the Home Affair Minister via the SAIA infrastructure; (iv) The Home Affairs Minister is deputed to collect and to maintain up-to-date the information related to citizens; (v) The Home Affair Minister communicates the updating data to de-registration municipality the Tax and Transport Office, and INPS so that citizens data are updated; (vi) The Home Affair Minister communicates the data, relevant for statistical purpose, to the CISIS.

After the first codification the BP4PA tool has been applied, and it returned low marks with respects to the different dimensions of the quality framework. Based on the resulting feedbacks the moving service has been improved and the resulting BP is shown in Figure 2 (for space reason we report only an excerpt of the BP to give an idea of its complexity). Improvements are based on the interpretation of the framework properties as implementation patterns to follow in order to get higher evaluation marks. Nevertheless we have to consider that in general higher level of the quality framework subsume higher investments from the PA. In general terms the starting BP reached bad quality levels in all the dimensions but the sharing one. The improvement intervention aimed at introducing, feedback messages directed to the citizens, messages between the involved administrations to improve their ability to cooperate via electronic means, the possibility of activating the service as result of the access to related services such as request to services related to marriage life events, and finally the provisioning of the service through different channels, profile and languages in order to improve inclusiveness.

# 6 Conclusions and Future Work

Exploiting domain knowledge in this paper we have introduced a user-friendly approach implemented in a plug-in for the Eclipse platform. It permits to assess, using formal verification techniques, a delivery process with respect to a defined quality framework. A discussion on the results we obtained from the conducted experiments is also reported. The general outcome is that (i) formal verification is mature enough to be introduced and applied in the field of study; (ii) delivery processes, defined for the services under study, reach low quality marks with
<figure><img src="image_3.png" /><figcaption>Fig. 2. BP excerpt for the Moving Service - improved version</figcaption></figure>

respect to the defined framework; and (iii) proposed approach can be a useful mean to improve the quality of BP related to GDS delivery.

For the future we intend to continue the evaluation applying the framework to other scenarios. Moreover the extension of the framework is one of the research line in which we have started to work trying to identify additional interesting requirements related to the delivery of GDSs. We also intend to extend the study to BPs related to other GDS aspects and PA activities. In particular we started to investigate how to automatically assess if a BP can be put in place given constraints related to the resources available within a public office.

## Acknowledgements

The authors would like to thank Regione Marche local public administration for the cooperation and for partially funding this research. A particular thanks to the offices of “P.F. Sistemi Informativi e Telematici”.

## References

1. Corradini, F., Hinkelmann, K., Polini, A., Polzonetti, A., Re, B.: C2ST: a quality framework to evaluate e-government service delivery. In: 8th International Conference EGOV 2009, Proceedings of ongoing research, project contributions and workshops, Linz (Austria) (2009) 74–84
2. Corradini, F., Polini, A., Polzonetti, A., Re, B.: Business processes verification for e-gov service delivery. Information Systems Management journal (to appear)

3. Layne, K., Leeb, J.: Developing fully functional e-government: a four stage model. Government Information Quarterly **18**(2) (2001) 122–136

4. Janssen, M., Kuk, G., Wagenaar, R.W.: A survey of web-based business models for e-government in the netherlands. Government Information Quarterly **25**(2) (2008) 202–220

5. Janssen, M., Kuk, G.: E-government business models for public service networks. International Journal of Electronic Government Research **3**(3) (2007) 54–71

6. Davies, J., Janowski, T., Ojo, A.K., Shukla, A.: Technological foundations of electronic governance. In Janowski, T., Pardo, T.A., eds.: ICEGOV. Volume 232 of ACM International Conference Proceeding Series., ACM (2007) 5–11

7. Morimoto, S.: A survey of formal verification for business process modeling. In: ICCS '08: Proceedings of the 8th international conference on Computational Science, Part II, Berlin, Heidelberg, Springer-Verlag (2008) 514–522

8. Wong, P.Y.H., Gibbons, J.: A process-algebraic approach to workflow specification and refinement. In: Proceedings of 6th International Symposium on Software Composition. Volume 4829 of LNCS. (2007)

9. Dijkman, R.M., Dumas, M., Ouyang, C.: Formal semantics and analysis of BPMN process models using petri nets. On-line (2007)

10. Ye, J., Sun, S., Song, W., Wen, L.: Formal semantics of BPMN process models using YAWL. Intelligent Information Technology Applications, 2007 Workshop on **2** (2008) 70–74

11. Wynn, M., Verbeek, H., van der Aalst, W., ter Hofstede, A., Edmond, D.: Business process verification finally a reality! Business Process Management Journal **15**(1) (2009) 74 – 92

12. Farrell, A.D., Sergot, M.J., Bartolini, C.: Formalising workflow: a CCS-inspired characterisation of the YAWL workflow patterns. Group Decision and Negotiation **16**(3) (2007) 213–254

13. Zhao, L., Li, Q., Liu, X., Du, N.: A modeling method based on CCS for workflow. (2009) 376–384

14. Lindsay, A., Downs, D., Lunn, K.: Business processes–attempts to find a definition. Information and Software Technology **45**(15) (2003) 1015 – 1019 Special Issue on Modelling Organisational Processes.

15. Harmon, P.: Business Process Change - A guide for Business Manager and BPM and Six Sigma Professionals. Horgan Kaufmann (2004)

16. White, S.A., Miers, D.: BPMN Modeling and Reference Guide Understanding and Using BPMN. Future Strategies Inc. (2008)

17. Hoare, C.A.R.: Communicating Sequential Processes. Prentis (2004)

18. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. Hardcover (2000)

19. Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: introducing a Process Analysis Toolkit. In Margaria, T., Steffen, B., eds.: ISOLA. Volume 17 of Communications in Computer and Information Science., Springer (2008) 307–322

20. zur Muehlen, M., Recker, J.: How much language is enough? Theoretical and practical use of the business process modeling notation. In Bellahsene, Z., Léonard, M., eds.: CAiSE. Volume 5074 of Lecture Notes in Computer Science., Springer (2008) 465–479

21. Re, B.: Quality of Digital e-Government Services. PhD thesis, School of Advances Studies – University of Camerino (2010)