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.
@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},
volume = {46},
year = {2012},
pages = {203-229},
doi = {10.1051/ita/2012002},
zbl = {1252.68195},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2012__46_2_203_0}
}
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) pp. 203-229. doi : 10.1051/ita/2012002. http://gdmltest.u-ga.fr/item/ITA_2012__46_2_203_0/
[1] , On stimulus for citizens' use of e-government services, in International Multiconference on Computer Science and Information Technology. Wisia (2008) 391-395.
[2] , and , Model Checking. Hardcover (2000).
[3] , 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] and , 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] , , , and , From bpmn to csp - toward business process verification for e-government service delivery. Technical report, University of Camerino (2009).
[7] , , and , Business processes verification for e-government service delivery. IS Management 27 (2010) 293-308.
[8] , , and , 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] , and , Formal semantics and analysis of BPMN process models using petri nets. Online (2007).
[10] and , 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] , 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] , and , Formalising workflow : a CCS-inspired characterisation of the YAWL workflow patterns. Group Decision and Negotation 16 (2007) 213-254.
[13] , , and , 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] , and , 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] and , 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] , Business Process Change - A guide tor Business Manager and BPM and Six Sigma Professionals. Horgan Kaufmann (2004).
[17] , , and , Design science in information systems research. Manage. Inf. Syst. Q. 28 (2004) 75-105.
[18] , Communicating Sequential Processes. Prentice Hall (2004). | Zbl 0637.68007
[19] and , E-government business models for public service networks. Int. J. Electron. Govern. Res. 3 (2007) 54-71.
[20] , , , and , 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] , and , A survey of web-based business models for e-government in the netherlands. Gov. Inf. Q. 25 (2008) 202-220.
[22] and , Developing fully functional e-government : a four stage model. Gov. Inf. Q. 18 (2001) 122-136.
[23] , and , Business processes-attempts to find a definition. Special Issue on Modelling Organisational Processes. Inf. Softw. Technol. 45 (2003) 1015-1019.
[24] , Specification of communicating processes : temporal logic versus refusals-based refinement. Form. Asp. Comput. 20 (2008) 277-294. | Zbl 1149.68056
[25] , Metrics for Process Models. Springer (2008).
[26] , 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] and , 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] , 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] and , 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] , and , 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] , , and , 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] , SMAWL : a SMAll Workflow Language based on CCS, in Proc. of CAiSE Short Paper Proceedings (2005).
[34] , and , 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] and , 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] and , 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] and , 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] and , 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] and , 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] and , Formalisations and applications of bpmn. Special issue on FOCLASA (2008). Sci. Comput. Program. (2009). | Zbl 1213.68212
[43] and , 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] , , , A.H.M. ter Hofstede, and D. Edmond, Bus. Process Manag. J. 15 (2009) 74-92.
[45] , , and , Formal semantics of BPMN process models using YAWL. Intelligent Information Technology Applications, 2007 Workshop on 2 (2008) 70-74.
[46] , , and , 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.