A perfecto verification: Combining model checking with deductive analysis to verify real-life software

7Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

This article is free to access.

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 model-checking 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.

Cite

CITATION STYLE

APA

Kesten, Y., Klein, A., Pnueli, A., & Raanan, G. (1999). A perfecto verification: Combining model checking with deductive analysis to verify real-life software. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1708, pp. 173–194). Springer Verlag. https://doi.org/10.1007/3-540-48119-2_12

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free