Bersani M. M., Distefano S., Ferrucci L., Mazzara M.
Recovery framework Semantics Workflow Formal methods Temporal logic
We formalize timed workflow with abnormal behavior management (i.e. recovery) and demonstrate how temporal logics and model checking are methodologies to iteratively revise the design correct-by construction system. We define a formal semantics by compiling generic workflow patterns into an extension of LTL with dense time clocks (CLTLoc). CLTLoc allows us to define the first logical formalization of workflows that can be practically employed in verification tools and to avoid the use of well-known automata based formalisms dealing with real-time. We use an ad-hoc bound model checker to prove requirements validity on a business process. The working assumption is that lightweight approaches easily fit into processes that are already in place so that radical change of procedures, tools and people's attitudes are not needed. 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.
Source: 9th International Joint Conference on Software Technologies, ICSOFT 2014, pp. 365–383, Vienna, Austria, 29-31 August, 2014
@inproceedings{oai:it.cnr:prodotti:424451, title = {A timed semantics of workflows}, author = {Bersani M. M. and Distefano S. and Ferrucci L. and Mazzara M.}, doi = {10.1007/978-3-319-25579-8_21}, booktitle = {9th International Joint Conference on Software Technologies, ICSOFT 2014, pp. 365–383, Vienna, Austria, 29-31 August, 2014}, year = {2015} }
Национальный агрегатор открытых репозиториев российских университетов (HOPA)
RE.PUBLIC@POLIMI Research Publications at Politecnico di Milano
Национальный агрегатор открытых репозиториев российских университетов (HOPA)
Национальный агрегатор открытых репозиториев российских университетов (HOPA)
Национальный агрегатор открытых репозиториев российских университетов (HOPA)
re.public.polimi.it
link.springer.com