Program models for compositional verification

Huisman, M. and Aktug, I. and Gurov, D. (2008) Program models for compositional verification. In: 10th International Conference on Formal Engineering Methods, 27-31 Oct 2008.

PDF
Restricted to UT campus only: Request a copy
441Kb

Abstract:	Compositional verification is crucial for guaranteeing the security of systems where new components can be loaded dynamically. In earlier work, we developed a compositional verification principle for control-flow properties of sequential control flow graphs with procedures. This paper discusses how the principle can be generalised to richer program models. We first present a generic program model, of which the original program model is an instantiation, and explicate under what conditions the compositional verification principle applies. We then present two other example instantiations of the generic model: with exceptional and with multi-threaded control flow, and show that for these particular instantiations the conditions hold. The program models we present are specifically tailored to our compositional verification principle; however, they are sufficiently intuitive and standard to be useful on their own. Tool support and practical application of the method are discussed.
Item Type:	Conference or Workshop Item
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/62491
Official URL:	http://dx.doi.org/10.1007/978-3-540-88194-0_11
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 254898