Abstraction Based Verification of a Parameterised Policy Controlled System

  • Peter Ochsenschläger
  • Roland Rieke
Part of the Communications in Computer and Information Science book series (CCIS, volume 1)


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.


Formal analysis of security and liveness properties security modelling and simulation security policies parameterised models 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ochsenschläger, P., Repp, J., Rieke, R.: Abstraction and composition — a verification method for co-operating systems. Journal of Experimental and Theoretical Artificial Intelligence 12, 447–459 (2000) Copyright: ©2000, American Association for Artificial Intelligence All rights reservedzbMATHCrossRefGoogle Scholar
  2. 2.
    Guttman, J.D., Herzog, A.L., Ramsdell, J.D.: Information flow in operating systems: Eager formal methods. In: IFIP WG 1.7 Workshop on Issues in the Theory of Security (2003)Google Scholar
  3. 3.
    Guttman, J.D., Herzog A.L.: Rigorous automated network security management. International Journal of Information Security 4(1–2), 29–48 (2005)CrossRefGoogle Scholar
  4. 4.
    Rieke, R.: Modelling and Analysing Network Security Policies in a Given Vulnerability Setting. In: Lopez, J. (ed.) CRITIS 2006. LNCS, vol. 4347, pp. 67–78: © Springer, Heidelberg (2006)Google Scholar
  5. 5.
    Ochsenschläger, P., Repp, J., Rieke, R., Nitsche, U.: The SH-Verification Tool Abstraction-Based Verification of Co-operating Systems. Formal Aspects of Computing, The International Journal of Formal Method 11, 1–24 (1999)Google Scholar
  6. 6.
    Ip, C.N., Dill, D.L.: Verifying Systems with REplicated Components in Murϕ. Formal Methods in System Design 14(3), 273–310 (1999)CrossRefGoogle Scholar
  7. 7.
    Derepas, F., Gastin, P.: Model checking systems of replicated processes with spin. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol. 2057, pp. 235–251. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 98–112. Springer, Heidelberg (2001)Google Scholar
  9. 9.
    Basu, S., Ramakrishnan, C.R.: Compositional analysis for verification of parameterized systems. Theor. Comput. Sci. 354(2), 211–229 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)Google Scholar
  11. 11.
    Bradfield, J., Stirling, C.: Modal logics and mu-calculi: an introduction (2001)Google Scholar
  12. 12.
    Uribe, T.E.: Combinations of model checking and theorem proving. In: Kirchner, H. (ed.) Frontiers of Combining Systems. LNCS, vol. 1794, pp. 151–170, Sprigner, Heidelberg (2000)CrossRefGoogle Scholar
  13. 13.
    Moses, T.: eXtensible Access Control Markup Language (XACML), Version 2.0. Technical report, OASIS Standard (2005)Google Scholar
  14. 14.
    Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Nitsche, U., Ochsenschläger, P.: Approximately satisfied properties of systems and simple language homomorphisms. Information Processing Letters 60, 201–206 (1996)CrossRefMathSciNetGoogle Scholar
  16. 16.
    Ochsenschläger, P.: Verification of cooperating systems by simple homomorphisms using the product net machine. In: Desel, J., Oberweis, A., Reisig, W. (eds.) Workshop: Algorithmen und Werkzeuge, für Petrinetze, Humboldt Universität Berlin, pp. 48–53 (1994)Google Scholar
  17. 17.
    Gürgens, S., Ochsenschläger, P., Rudolph, C.: On a formal framework for security properties. International Computer Standards & Interface Journal (CSI), Special issue on formal methods, techniques and tools for secure and reliable applications (2004)Google Scholar
  18. 18.
    Gürgens, S., Ochsenschläger, P, Rudolph, C.: Abstractions preserving parameter confidentiality. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 418–437 Copyright: ©Springer, Heidelberg (2005)Google Scholar
  19. 19.
    Eilenberg, S.: Automata, Languages and Machines, vol. A. Academic Press, New York (1974)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Peter Ochsenschläger
    • 1
  • Roland Rieke
    • 1
  1. 1.Fraunhofer Institute for Secure Information Technology SITDarmstadtGermany

Personalised recommendations