Formal Methods to Improve Public Administration Business Processes

Andrea Polini; Andrea Polzonetti; Barbara Re

RAIRO - Theoretical Informatics and Applications (2012)

  • Volume: 46, Issue: 2, page 203-229
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Polini, Andrea, Polzonetti, Andrea, and Re, Barbara. "Formal Methods to Improve Public Administration Business Processes." RAIRO - Theoretical Informatics and Applications 46.2 (2012): 203-229. <http://eudml.org/doc/221949>.

@article{Polini2012,
abstract = {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.},
author = {Polini, Andrea, Polzonetti, Andrea, Re, Barbara},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Business process formal verification; business process quality assessment; domain dependent property checking; e-government quality framework; verification of business process models; CSP models},
language = {eng},
month = {4},
number = {2},
pages = {203-229},
publisher = {EDP Sciences},
title = {Formal Methods to Improve Public Administration Business Processes},
url = {http://eudml.org/doc/221949},
volume = {46},
year = {2012},
}

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
DA - 2012/4//
PB - EDP Sciences
VL - 46
IS - 2
SP - 203
EP - 229
AB - 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.
LA - eng
KW - Business process formal verification; business process quality assessment; domain dependent property checking; e-government quality framework; verification of business process models; CSP models
UR - http://eudml.org/doc/221949
ER -

References

top
  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 Management27 (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).  
  12. A.D. Farrell, M.J. Sergot and C. Bartolini, Formalising workflow : a CCS-inspired characterisation of the YAWL workflow patterns. Group Decision and Negotation16 (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).  
  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.  
  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 .  URIhttp://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).  
  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.  
  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 on2 (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.  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.