Formal Methods to Improve Public Administration Business Processes
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) no. 2, pp. 203-229.

Starting from late 90's the public administration has started to employ a quite relevant amount of its budget in developing ICT solutions to better deliver services to citizens. In spite of this effort many statistics show that the mere availability of ICT based services does not guarantee per se their usage. Citizens have continued to largely access services through “traditional” means. In our study we suggest that the highlighted situation is partly due to the fact that relevant domain dependent requirements, mainly related to the delivery process of e-government digital services, are often ignored in the development of e-government solutions. We provide here a domain related quality framework and encoded it in a set of formal statements, so that we can apply automatic verification techniques to assess and improve ICT solutions adopted by public administrations. The paper discusses both the defined quality framework and the tool chain we developed to enable automatic assessment of ICT solutions. The tool chain is based on a denotational mapping of business process modeling notation elements into process algebraic descriptions and to the encoding of quality requirements in linear temporal logic formulas. The resulting approach has been applied to real case studies with encouraging results.

DOI : https://doi.org/10.1051/ita/2012002
Classification : 68
Mots clés : business process formal verification, business process quality assessment, domain dependent property checking, e-government quality framework
@article{ITA_2012__46_2_203_0,
     author = {Polini, Andrea and Polzonetti, Andrea and Re, Barbara},
     title = {Formal {Methods} to {Improve} {Public} {Administration} {Business} {Processes}},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {203--229},
     publisher = {EDP-Sciences},
     volume = {46},
     number = {2},
     year = {2012},
     doi = {10.1051/ita/2012002},
     zbl = {1252.68195},
     language = {en},
     url = {http://www.numdam.org/articles/10.1051/ita/2012002/}
}
TY  - JOUR
AU  - Polini, Andrea
AU  - Polzonetti, Andrea
AU  - Re, Barbara
TI  - Formal Methods to Improve Public Administration Business Processes
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2012
DA  - 2012///
SP  - 203
EP  - 229
VL  - 46
IS  - 2
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita/2012002/
UR  - https://zbmath.org/?q=an%3A1252.68195
UR  - https://doi.org/10.1051/ita/2012002
DO  - 10.1051/ita/2012002
LA  - en
ID  - ITA_2012__46_2_203_0
ER  - 
Polini, Andrea; Polzonetti, Andrea; Re, Barbara. Formal Methods to Improve Public Administration Business Processes. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) no. 2, pp. 203-229. doi : 10.1051/ita/2012002. http://www.numdam.org/articles/10.1051/ita/2012002/

[1] C. Bavec, On stimulus for citizens' use of e-government services, in International Multiconference on Computer Science and Information Technology. Wisia (2008) 391-395.

[2] E.M. Clarke, O. Grumberg and D.A. Peled, Model Checking. Hardcover (2000).

[3] G. Colclough, The user challenge benchmarking the supply of online public services - 7th measurement. Technical report, prepared by Capgemini for European Commission Directorate General for Information Society and Media (2007).

[4] G. Colclough and D. Tinholt, Smarter, faster, better e-government - 8th benchmarking measurement. Technical report, prepared by Capgemini, RAND Europe, IDC, SOGETI and DTi. For European Commission Directorate General for Information Society and Media (2009).

[5] Communication from the Commission to the Council, the European Parliament, the European Economic, Social Committee, and the Committee of the Regions, The Role of eGovernment for Europe's Future. Technical report, Commission of the European Communities, Brussels (2003).

[6] F. Corradini, D. Falcioni, A. Polini, A. Polzonetti and B. Re, From bpmn to csp - toward business process verification for e-government service delivery. Technical report, University of Camerino (2009).

[7] F. Corradini, A. Polini, A. Polzonetti and B. Re, Business processes verification for e-government service delivery. IS Management 27 (2010) 293-308.

[8] J. Davies, T. Janowski, A.K. Ojo and A. Shukla, Technological foundations of electronic governance, in Proc. of ICEGOV, edited by T. Janowski and T.A. Pardo. ACM Int. Conf. Proc. Ser. 232 (2007) 5-11.

[9] R.M. Dijkman, M. Dumas and C. Ouyang, Formal semantics and analysis of BPMN process models using petri nets. Online (2007).

[10] W. Ebbers and W. Pieterson, The multi-channel citizen : a study of the use of service channels by citizens in the Netherlands, in Electronic Government, 6th International Conference, EGOV Proceedings (2007).

[11] E.A Emerson, Temporal and modal logic, in Handbook of theoretical computer science formal models and semantics B. Cambridge, MA, USA (1990). | MR 1127201 | Zbl 0900.03030

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

[13] A. Forster, G. Engels, T. Schattkowsky and R. Van Der Straeten, Verification of business process quality constraints based on visual process patterns, in TASE '07 : Proc. of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering. IEEE Computer Society, Washington, DC, USA (2007) 197-208.

[14] X. Fu, T. Bultan and J. Su, Analysis of interacting BPEL web services, in WWW '04 : Proc. of the 13th international conference on World Wide Web. ACM, New York, NY, USA (2004) 621-630.

[15] R. Hamadi and B. Benatallah, A petri net-based model for web service composition, in ADC '03 : Proc. of the 14th Australasian database conference. Australian Computer Society, Inc., Darlinghurst, Australia, Australia (2003) 191-200.

[16] P. Harmon, Business Process Change - A guide tor Business Manager and BPM and Six Sigma Professionals. Horgan Kaufmann (2004).

[17] A.R. Hevner, S.T. March, J. Park and S. Ram, Design science in information systems research. Manage. Inf. Syst. Q. 28 (2004) 75-105.

[18] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall (2004). | Zbl 0637.68007

[19] M. Janssen and G. Kuk, E-government business models for public service networks. Int. J. Electron. Govern. Res. 3 (2007) 54-71.

[20] W. Janssen, R. Mateescu, S. Mauw, P. Fennema and P. Van Der Stappen, Model checking for managers, in Proc. of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking. Springer-Verlag, London, UK (1999) 92-107.

[21] M. Janssen, G. Kuk and R.W. Wagenaar, A survey of web-based business models for e-government in the netherlands. Gov. Inf. Q. 25 (2008) 202-220.

[22] K. Layne and J. Leeb, Developing fully functional e-government : a four stage model. Gov. Inf. Q. 18 (2001) 122-136.

[23] A. Lindsay, D. Downs and K. Lunn, Business processes-attempts to find a definition. Special Issue on Modelling Organisational Processes. Inf. Softw. Technol. 45 (2003) 1015-1019.

[24] G. Lowe, Specification of communicating processes : temporal logic versus refusals-based refinement. Form. Asp. Comput. 20 (2008) 277-294. | Zbl 1149.68056

[25] J. Mendling, Metrics for Process Models. Springer (2008).

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

[27] S. Narayanan and S.A. Mcilraith, Simulation, verification and automated composition of web services, in WWW '02 : Proc. of the 11th international conference on World Wide Web. ACM, New York, NY, USA (2002) 77-88.

[28] P. Norris, Digital Divide Civic Engagement, Information Poverty and the Internet Worldwide. Cambridge University Press (2001).

[29] OMG, Business process model and notation (bpmn) 2.0. Technical report, Object Management Group (2009).

[30] W. Pieterson and J. Van Dijk, Channel choice determinants; an exploration of the factors that determine the choice of a service channel in citizen initiated contacts, in dg.o '07 : Proc. of the 8th annual international conference on Digital government research. Digital Government Research Center (2007) 173-182.

[31] G. Salaün, L. Bordeaux and M. Schaerf, Describing and reasoning on web services using process algebra, in ICWS '04 : Proc. of the IEEE International Conference on Web Services. IEEE Computer Society Washington, DC, USA (2004) 43.

[32] M. Solar, G. Valdés, H. Astudillo and M. Iribarren, G. Concha and M. Visconti, Conception, development and implementation of an e-government conception, development and implementation of an e-government maturity model in public agencies. Elsevier in Government Information Quarterly (2011).

[33] C. Stefansen, SMAWL : a SMAll Workflow Language based on CCS, in Proc. of CAiSE Short Paper Proceedings (2005).

[34] J. Sun, Y. Liu and J. Song Dong, Model checking CSP revisited : introducing a Process Analysis Toolkit, in Proc. of ISoLA, edited by T. Margaria and B. Steffen. Commun. Comput. Inform. Sci. 17 (2008) 307-322.

[35] W.M.P. van der Aalst, and A. H.M. ter Hofstede, YAWL : yet another workflow language. Inf. Syst. 30 (2005) 245-275.

[36] P. Wauters and G. Colclough, On-line availability of public services : How is europe progressing? Web based survey on electronic public services report of the 6th measurement. Technical report (2006). Prepared by Capgemini for European Commission Directorate General for Information Society and Media (2006).

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

[38] P. Wohed, W.M.P. van der Aalst, M. Dumas and A.H.M. ter Hofstede, Analysis of web services composition languages : the case of BPEL4WS, in ER, edited by I.-Y. Song, S.W. Liddle, T.W. Ling and P. Scheuermann. Lect. Notes Comput. Sci. 2813 (2003) 200-215.

[39] P.Y.H. Wong and J. Gibbons, A process-algebraic approach to workflow specification and refinement, in Proc. of 6th International Symposium on Software Composition. Lect. Notes Comput. Sci. 4829 (2007).

[40] P.Y.H. Wong and J. Gibbons, Verifying business process compatibility (short paper), in QSIC '08 : Proc. of the 2008 The Eighth International Conference on Quality Software. IEEE Computer Society, Washington, DC, USA (2008) 126-131.

[41] P.Y.H. Wong and J. Gibbons, A Process Semantics for BPMN, in Proc. of 10th International Conference on Formal Engineering Methods. Lect. Notes Comput. Sci. 5256 (2008). Extended version available at http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/bpmnsem.pdf.

[42] P.Y.H. Wong and J. Gibbons, Formalisations and applications of bpmn. Special issue on FOCLASA (2008). Sci. Comput. Program. (2009). | Zbl 1213.68212

[43] P. Wong and J. Gibbons, Property specifications for workflow modelling, in Integrated Formal Methods, edited by M. Leuschel and H. Wehrheim. Lect. Notes Comput. Sci. 5423 (2009) 56-71. | Zbl 1211.68258

[44] M.T. Wynn, H.M.W. Verbeek, W.M.P. Van Der Aalst, A.H.M. ter Hofstede, and D. Edmond, Bus. Process Manag. J. 15 (2009) 74-92.

[45] J. Ye, S. Sun, W. Song and L. Wen, Formal semantics of BPMN process models using YAWL. Intelligent Information Technology Applications, 2007 Workshop on 2 (2008) 70-74.

[46] L. Zhao, Q. Li, X. Liu and N. Du, A modeling method based on CCS for workflow (2009) 376-384.

[47] M. zur Muehlen and J. Recker, How much language is enough? Theoretical and practical use of the business process modeling notation, in Proc. of CAiSE, edited by Z. Bellahsene and M. Léonard. Lect. Notes Comput. Sci. 5074 (2008) 465-479.

Cité par Sources :