Istituto di Scienza e Tecnologie dell'Informazione     
Ferrucci L., Bersani M. M., Mazzara M. An LTL semantics of business working rows with recovery. In: ICSOFT-PT 2014 - 9th International Conference on Software Paradigm Trends (Wien, Austria, 29-31 August 2014). Proceedings, pp. 29 - 40. ScitePress, 2014.
We describe a business workflow case study with abnormal behavior management (i.e. recovery) and demonstrate how temporal logics and model checking can provide a methodology to iteratively revise the design and obtain a correct-by construction system. To do so we define a formal semantics by giving a compilation of generic workflow patterns into LTL and we use the bound model checker Zot to prove specific properties and requirements validity. The working assumption is that such a lightweight approach would easily fit into processes that are already in place without the need for a radical change of procedures, tools and people's attitudes. The complexity of formalisms and invasiveness of methods have been demonstrated to be one of the major drawback and obstacle for deployment of formal engineering techniques into mundane projects.
URL: http://www.scitepress.org/DigitalLibrary/Link.aspx?doi=10.5220/0005110000290040
DOI: 10.5220/0005110000290040
Subject Temporal logic
Business workflows
Recovery framework
Formal methods
F.3.1 LOGICS AND MEANINGS OF PROGRAMS. Specifying and Verifying and Reasoning about Programs

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional