Paper Info
Title
Automatic Compositional Verification of Probabilistic Safety Properties for Inter-organisationalWorkflow Processes.
Abstract
For many complex systems, it is important to verify formally their correctness; the aim is to guarantee the reliability and the correctness of such systems before their effective deployment. Several methods have been proposed to this effect using different formal tools such as Probabilistic Automata (PA). In this paper we focus on verification of service-based inter-organizational workflow (IOWF) processes which support collaboration and cooperation between WF processes attached to several partners, and specified using the business process execution language (BPEL4WS). Then, IOWF processes are translated to Probabilistic Automata (PA) models. More than verification support, PA provides a numerical evaluation of the IOWF process. We also propose the use of compositional verification to cope with the state space explosion problem. The IOWF behavior is checked against probabilistic safety properties. The verification and the analysis are performed in an automated way using the PRISM model checker and based on the assume-guarantee reasoning rule.
Year
DOI
Venue
2016
10.5220/0005978602440253
SIMULTECH
Field
DocType
Citations 
Model checking,Software engineering,Computer science,Correctness,PRISM model checker,Real-time computing,Theoretical computer science,Business Process Execution Language,Probabilistic logic,Workflow,State space,Probabilistic automaton
Conference
1
PageRank 
References 
Authors
0.35
0
3
Name
Order
Citations
PageRank
Redouane Bouchekir110.35
Saïda Boukhedouma263.12
Mohand Cherif Boukala3122.64