Workflow Nets Verification: SMT or CLP?
| Affiliation auteurs | !!!! Error affiliation !!!! |
| Titre | Workflow Nets Verification: SMT or CLP? |
| Type de publication | Conference Paper |
| Year of Publication | 2016 |
| Auteurs | Bride H, Kouchnarenko O, Peureux F, Voiron G |
| Editor | TerBeek MH, Gnesi S, Knapp A |
| Conference Name | CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION |
| Publisher | European Res Consortium Informat & Math; Formal Methods Europe; Springer Intl Publishing AG |
| Conference Location | GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND |
| ISBN Number | 978-3-319-45943-1; 978-3-319-45942-4 |
| Mots-clés | Constraint solving problem, Experimental comparison, Modal specifications, Satisfiability modulo theory, Verification method, Workflow nets |
| Résumé | The design and the analysis of business processes commonly relies on workflow nets, a suited class of Petri nets. This paper evaluates and compares two resolution methods-Satisfiability Modulo Theory (SMT) and Constraint Logic Programming (CLP)-applied to the verification of modal specifications over workflow nets. Firstly, it provides a concise description of the verification methods based on constraint solving. Secondly, it presents the experimental protocol designed to evaluate and compare the scalability and efficiency of both resolution approaches. Thirdly, the paper reports on the obtained results and discusses the lessons learned from these experiments. |
| DOI | 10.1007/978-3-319-45943-1_3 |