Abstract
As shown above, verification of temporal properties on behaviour abstractions is suitable for detecting service interactions. In the example that we briefly explained the abstraction step was not really necessary, for the example itself is small enough to check temporal properties directly on the behaviour.
A complete analysis of the BCSM model already leads to a behaviour representation having several thousand states. Including services, we expect several tenthousand states. This reaches an order of magnitude of the number of states that makes abstraction techniques absolutely necessary. Here, even the analysis of the specification can become difficult with respect to complexity. Hence, a compositional analysis technique of specifications that allows to compute a representation of an abstract behaviour without exhaustive construction of the complete state space is currently developed [Och95]. We expect that our approach will allow us to check several combinations of services for undesired interactions where any direct verification approach without abstractions would be intractable.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Pierre Combes, Max Michel, and Béatrice Renard. Formal verification of telecommunication service interactions using SDL methods and tools. In O. Faergemand and A. Sarma, editors, SDL'93: Using Objects, pages 441–452. Elsevier, 1993.
Ulrich Nitsche. Propositional linear temporal logic and language homomorphisms. In Anil Nerode and Yuri V. Matiyasevich, editors, Logical Foundations of Computer Science '94-Logic at St. Petersburg, volume 813 of Lecture Notes in Computer Science, pages 265–277. Springer Verlag, 1994.
Ulrich Nitsche. A verification method based on homomorphic model abstraction. In Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing, page 393, Los Angeles, 1994. ACM Press.
Ulrich Nitsche and Peter Ochsenschläger. Approximately satisfied properties of systems and simple language homomorphisms. Arbeitspapiere der GMD 965, Gesellschaft für Mathematik und Datenverarbeitung (GMD), Darmstadt, December 1995.
Peter Ochsenschläger. Verification of cooperating systems by simple homomorphisms using the product net machine. In Jörg Desel, Andreas Oberweis, and Wolfgang Reisig, editors, Workshop: Algorithmen und Werkzeuge für Petrinetze, pages 48–53. Humboldt Universität Berlin, 1994.
Peter Ochsenschläger. Compositional verification of cooperating systems using simple homomorphisms. In Jörg Desel, Hans Fleischhack, Andreas Oberweis, and Sonnenschein Michael, editors, Workshop: Algorithmen und Werkzeuge für Petrinetze, pages 8–13. Universität Oldenburg, 1995.
Peter Ochsenschläger and Rainer Prinoth. Modellierung verteilter Systeme — Konzeption, Formale Spezifikation und Verifikation mit Produktnetzen. Vieweg, Wiesbaden, 1995.
Draft Revised ITU-T Recommendation Q.1214: Distributed Functional Plane for Intelligent Network CS-1. March 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Capellmann, C., Demant, R., Fatahi-Vanani, F., Galvez-Estrada, R., Nitsche, U., Ochsenschläger, P. (1996). Verification by behaviour abstraction. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_104
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_104
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive