Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Abstraction based verification of a parameterised policy controlled system

 
: Ochsenschläger, P.; Rieke, R.

:

Gorodetsky, V.:
Computer network security. Fourth International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security, MMM-ACNS 2007 : St. Petersburg, Russia, September 13-15, 2007; Proceedings
Berlin: Springer, 2007 (Communications in computer and information science 1)
ISBN: 3-540-73985-8
ISBN: 978-3-540-73985-2
S.228-241
International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security (MMM-ACNS) <4, 2007, St. Petersburg>
Englisch
Konferenzbeitrag
Fraunhofer SIT ()

Abstract
Safety critical and business critical systems are usually controlled by policies with the objective to guarantee a variety of safety, liveness and security properties. Traditional model checking techniques allow a verification of the required behaviour only for systems with very few components. To be able to verify entire families of systems, independent of the exact number of replicated components, we developed an abstraction based approach to extend our current tool supported verification techniques to such families of systems that are usually parameterised by a number of replicated identical components. We demonstrate our technique by an exemplary verification of security and liveness properties of a simple parameterised collaboration scenario. Verification results for configurations with fixed numbers of components are used to choose an appropriate property preserving abstraction that provides the basis for an inductive proof that generalises the results for a family of systems with arbitrary settings of parameters.

: http://publica.fraunhofer.de/dokumente/N-69181.html