Formal methods to improve public administration business processes

Starting from late 90’s the public administration has started to employ a quite relevant amount of its budget in develop ing 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.