Advertisement

State Space Representation for Verification of Open Systems

  • Irem Aktug
  • Dilian Gurov
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4019)

Abstract

When designing an open system, there might be no implementation available for certain components at verification time. For such systems, verification has to be based on assumptions on the underspecified components. When component assumptions are expressed in Hennessy-Milner logic (HML), the state space of open systems can be naturally represented with modal transition systems (MTS), a graphical specification language equiexpressive with HML. Having an explicit state space representation supports state space exploration based verification techniques. Besides, it enables proof reuse and facilitates visualization for the user guiding the verification process in interactive verification. As an intuitive representation of system behavior, it aids debugging when proof generation fails in automatic verification.

However, HML is not expressive enough to capture temporal assumptions. For this purpose, we extend MTSs to represent the state space of open systems where component assumptions are specified in modal μ-calculus. We present a two-phase construction from process algebraic open system descriptions to such state space representations. The first phase deals with component assumptions, and is essentially a maximal model construction for the modal μ-calculus. In the second phase, the models obtained are combined according to the structure of the open system to form the complete state space. The construction is sound and complete for systems with a single unknown component and sound for those without dynamic process creation. For establishing open system properties based on the representation, we present a proof system which is sound and complete for prime formulae.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Martinelli, F.: Analysis of security protocols as open systems. Theoretical Computer Science 290, 1057–1106 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Larsen, K.G.: Modal specifications. Automatic Verification Methods for Finite State Systems, 232–246 (1989)Google Scholar
  3. 3.
    Aktug, I., Gurov, D.: Verification of open systems based on explicit state space representation. In: AVIS 2005: Proceedings of Automated Verification of Infinite Systems (to appear, 2005)Google Scholar
  4. 4.
    Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Dam, M.: Fixed points of Büchi automata. In: Shyamasundar, R.K. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 39–50. Springer, Heidelberg (1992)Google Scholar
  6. 6.
    Kaivola, R.: On modal mu-calculus and Büchi tree automata. Information Processing Letters 54, 17–22 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Grumberg, O., Long, D.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)CrossRefGoogle Scholar
  8. 8.
    Kupferman, O., Vardi, M.: An automata-theoretic approach to modular model checking. ACM Transactions on Programming Languages and Systems 22, 87–128 (2000)CrossRefGoogle Scholar
  9. 9.
    Sprenger, C., Gurov, D., Huisman, M.: Compositional verification for secure loading of smart card applets. In: Heitmeyer, C., Talpin, J.P. (eds.) Proc. MEMOCODE 2004, pp. 211–222. IEEE, Los Alamitos (2004)Google Scholar
  10. 10.
    Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: Proceedings of 32nd Annual Symposium on Foundations of Computer Science, pp. 368–377. IEEE Computer Society Press, Los Alamitos (1991)CrossRefGoogle Scholar
  11. 11.
    Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of ACM 47, 312–360 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Dam, M., Fredlund, L., Gurov, D.: Toward parametric verification of open distributed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 150–185. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Dam, M., Gurov, D.: Compositional verification of CCS processes. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol. 1755, pp. 247–256. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  14. 14.
    Christensen, S.: Decidability and Decomposition in Process Algebras. PhD thesis, University of Edinburgh (1993)Google Scholar
  15. 15.
    Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001 and ETAPS 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  16. 16.
    Grumberg, O., Shoham, S.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. Computation Theory 208, 157–168 (1984)MathSciNetGoogle Scholar
  18. 18.
    Bustan, D., Grumberg, O.: Applicability of fair simulation. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 401–414. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  19. 19.
    Aktug, I., Gurov, D.: State space representation for verification of open systems. Technical report, KTH CSC (2006), http://www.nada.kth.se/~irem/sefros/techrep06.ps
  20. 20.
    Bradfield, J., Stirling, C.: Local model checking for infinite state spaces. Theoretical Computer Science 96, 157–174 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, Heidelberg (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Irem Aktug
    • 1
  • Dilian Gurov
    • 1
  1. 1.KTH Computer Science and CommunicationStockholmSweden

Personalised recommendations