We introduce a class of symbolic transition systems capable of representing collections of security-aware workflows and we study the verification of reachability properties of such systems. More precisely, we define composed array-based systems as an extension of array-based systems in which array variables are indexed over more than one type. For an application relevant sub-class of these systems we show how to mechanize a symbolic backward reachability procedure by modularly re-using the techniques developed for array-based systems. Finally, and most importantly, we find sufficient conditions for the termination of the procedure and we apply this result to derive the decidability of the reachability problems of two important classes of security-aware workflow systems.

Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows / Bertolissi, C; Ranise, S. - 8152:(2013), pp. 40-55. (Intervento presentato al convegno International Symposium on Frontiers of Combining Systems (FroCoS 2013) tenutosi a Francia nel 18-20/09/2013).

Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows

Ranise, S
2013-01-01

Abstract

We introduce a class of symbolic transition systems capable of representing collections of security-aware workflows and we study the verification of reachability properties of such systems. More precisely, we define composed array-based systems as an extension of array-based systems in which array variables are indexed over more than one type. For an application relevant sub-class of these systems we show how to mechanize a symbolic backward reachability procedure by modularly re-using the techniques developed for array-based systems. Finally, and most importantly, we find sufficient conditions for the termination of the procedure and we apply this result to derive the decidability of the reachability problems of two important classes of security-aware workflow systems.
2013
International Symposium on Frontiers of Combining Systems (FroCoS 2013)
HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY
SPRINGER-VERLAG BERLIN
Bertolissi, C; Ranise, S
Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows / Bertolissi, C; Ranise, S. - 8152:(2013), pp. 40-55. (Intervento presentato al convegno International Symposium on Frontiers of Combining Systems (FroCoS 2013) tenutosi a Francia nel 18-20/09/2013).
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333152
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact