Modeling and Verification of Business Processes for the Public Administration

A successful aspect in today's organization is the integration and cooperation among Business Processes (BPs) of heterogeneous and disperse organizations. In such a way different organizations have to logically integrate each others to provide higher value services to users and to improve their efficiency and overall effectiveness. Moving toward an inter-organizational scenarios suitable to strive cooperation in order to provide integrated functionalities is a need. The integration passes thought the coordination of organizations objectives. It is need a clear perspective on local and global views on Business Process in order to contribute to the definition of inter-organizational Business Processes stressing the role of messages exchange. The scenario previously introduced is a typical scenario in Public Administration (PA) where several organizations have to cooperate to provide public service that is the result of inter-administration Business Process. In particular, according to the European Interoperability Framework and its adoptions in the European member states one of the main challenges in PA is to cope with large collections of interconnected Business Processes. According to the Business Process Management life cycle modeling and analysis of inter-organizational BP are critical activities. This is particularly true in e-government domain. For what concern the modeling the thesis introduces a Domain Specific Language, eGAML, based on standards such as BPMN 2.0 and UML 2.0 to support the design of e-government services focusing on process component and enabling the explicit representation of related elements. The main scope is not to build a Domain Specific Language that fit every aspect of the Enterprise Architecture in egovernment, but the thesis aim to define a methodology and a practical approach that drive domain experts to model only specifics views impacting on the Business Process definition, execution and acceptance and to make clear the relations among them. For what concern the analysis phase the thesis discuss an approach for formal verification of PA inter-organizational BPs. The approach uses state evaluation techniques with an optimized unfolding algorithm based on BPMN 2.0 specific semantic. In this way after BP modeling using BPMN 2.0 the analyst can run our algorithm to check if the BP includes bad traces. In such a case he/she can re-engineer the BP in order to remove the bad traces so to derive an improved BP. Result are supported by a user-friendly and web based tool named ''HawkEye'' that has been successfully applied to real scenarios. It permits to have an integrated environment in which to design and to automatically verify the BP model via the proposed algorithm. The approach and the prototype have been successfully applied to real scenarios thanks to a close collaboration with local PA offices, with encouraging results. In particular, subject of the investigation are three cases studies from the e-government domain: (i) family reunion, (ii) grant citizenship, and (iii) bouncer registration