Abstract
The paper presents an approach to the formal verification of a complete software system intended to support the flagship product of Perfecto Technologies which enforces application security over an open communication net.
Based on initial experimentation, it was decided that the verification method will be based on a combination of model-checking using spin with deductive verification which handles the more data-intensive elements of the design. The analysis was that only such a combination can cover by formal verification all the important aspects of the complete system.
In order to enable model checking of large portions of the design, we have developed an assume-guarantee approach which supports compositional verification. We describe how this general approach was implemented in the spin framework.
Then, we explain the need to split the verification activity into the modelchecking part which deals with the control issues such as concurrency or deadlocking and a deductive part which handles the data-intensive elements of the design.
Chapter PDF
Similar content being viewed by others
Keyword
References
M. Abadi and L. Lamport. Composing specifications. ACM Trans. Prog. Lang. Sys., 15:73–132, 1993.
M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. Prog. Lang. Sys., 17(3):507–534, 1995.
N. Bjørner, I.A. Browne, E. Chang, M. Coón, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover, User’s Manual. Technical Report, Stanford University, 1995.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
H. Barringer and R. Kuiper. Hierarchical development of concurrent systems in a temporal logic framework. In Proc. of Seminar on Concurrency, LNCS 197, 1985.
P. Collete and A. Cau. Parallel composition of assumption-commitment specifications: A unifying approach for shared variables and distributed message passing concurrency. Acta Informatica, 1995.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking. In Model Checking, Abstraction and Composition, volume 152 of Nato ASI Series F, pages 477–498. Springer-Verlag, 1996.
K.M. Chandy and J. Misra. Proofs of networks of processes. IEEE Trans. Software Engin., 7(4):417–426, 1981.
W.-P. de Roever. The quest for compositionality-a survey of assertion-based proof systems for concurrent programs, part i: Concurrency based on shared variables. In The Role of Abstract Models in Computer Science, pages 181–206. IFIP, North Holland, 1985.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1984.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Engelwood Clis, NJ, 1991.
C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Trans. Prog. Lang. Sys., 5(4):596–619, 1983.
B. Jonsson. Compositional specification and verification of distributed systems. ACM Trans. Prog. Lang. Sys., 16(2):259–303, 1994.
R.P. Kurshan and K.L. McMillan. A structural induction theorem for processes. Information and Computation, 117:1–11, 1995.
Y. Kesten and A. Pnueli. Deductive verification of fair discrete systems. Technical report, Weizmann Institute, 1998.
Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. In ICALP’98 pages 1–16.
L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Engin., 3:125–143, 1977.
Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proc. 9th ACM Symp. Princ. of Dist. Comp., pages 377–408, 1990.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
S. Owre, N. Shankar, and J.M. Rushby. User guide for the PVS specification and verification system. SRI International, Menlo Park, CA, 1993.
P.K. Pandya and M. Joseph. P-A logic-a compositional proof system for distributed programs. Dist. Comp., 5:37–54, 1991.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, sub-series F: Computer and System Science, pages 123–144. Springer-Verlag, 1985.
Q.W. Xu, W.-P. de Roever, and J.-F. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149–174, 1997.
J. Zwiers. Compositionality Concurrency and Partial Correctness, volume 321 of Lect. Notes in Comp. Sci. Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kesten, Y., Klein, A., Pnueli, A., Raanan, G. (1999). A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_12
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive