Published: Jun 6, 2013
The following paper has been accepted at the International Symposium on Frontiers of Combining Systems (FroCoS 2013):
- Title: Verification of Composed Array-based Systems with Applications to Security-Aware Workflows
- Author: Clara Bertolissi, Silvio Ranise
- 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.
- DOI: 10.1007/978-3-642-40885-4_4
About the conference
- Name: International Symposium on Frontiers of Combining Systems (FroCoS 2013)
- Date: from September 18, 2013 to September 20, 2013
- Location: Nancy, France
- Website: https://frocos2013.loria.fr/