Introduction

e-Government is a process intensive domain driven by law and regulations and characterized by citizens and inter-administrations interactions. Properties of service delivery processes strongly impact on the use of services by citizens. We think that a suitable way to represent, assess and continuously improve applied processes, according to domain requirements, is needed. BP4PA is a suitable approach that permits to integrate the knowledge of domain experts with the rigor of formal methods. The approach, supported by a user-friendly tool, permits to formally check if a given business process for service delivery, and specified via a graphical language, satisfy given quality properties. The approach is already implemented in an Eclipse plug-in available in this web space.

Implementation

The approach has been implemented as a plug-in of the Eclipse Framework. This result in a fully integrated and user friendly environment that supports the analyst both on the specification and on the verification of a specified process. Our plug-in is integrated with third party Eclipse extensions such as the BPMN editor and the PAT model checker.

The user will specify the BP using the BPMN editor extension and will select the properties he/she desires to be checked using the C2ST framework extension. Then these specification will be translated via the mappings we have defined using the Eclipse Modelling Framework. The resulting specifications will be provided to the PAT Model Checker that will return successfully, in case the property is not violated, or will return a counterexample showing an execution violating the quality level.

We will appreciate any comment, suggestion or involvement about the projects. See the "People" section for contacts.