Abstract
In this paper, we present a generic tool, called FMona, for expressing validation methods. we illustrate its use through the expression of the abstraction technique and its application to infinite or parameterized space problems. After a review of the basic results concerning transition systems, we show how abstraction can be expressed within FMona and used to build a reduced system with decidable properties. The FMona tool is used to express the validation steps leading to synthesis of a finite abstract system;then SMV and/or Mona validate its properties.
Chapter PDF
References
J. Archibald and J.-L. Baer. Cache coherence protocols: Evaluation using a multiprocessor simulation model. ACM Transactions on Computer Systems, 4(4):273–298, November 1986. 214
Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, and Marcus Nilsson. Handling Global Conditions in Parameterized System Verification. In Proc. 11th Int. Conf. on Computer Aided Verification, volume 1633 of Lecture Notes in Computer Science, pages 134–145. Springer Verlag, 1999. 217
A. Ayari, D. Basin, and A. Podelski. Lisa: A specification language based on ws2s. In 11th International Conference of the European Association for Computer Science Logic (CSL’ 97), volume 1414 of LNCS, pages 18–34. Springer-Verlag, 1997. 209
A. Arnold. Systèmes de transitions finis et sémantiques des processus communicants. Etudes et recherches en informatique. MASSON, 1992. 206
BBC+97._B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual — Version V6.1. Technical Report 0203, INRIA, August 1997. 204
J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Symbolic model checking: 10E20 states and beyond. In 5th Symposium on Logic in Computer Science, June 1990. 204, 209
J.-P. Bodeveix and M. Filali. Reduction and quantifier elimination techniques for program validation. Formal Methods in System Design, to appear, 1999. 215
J.-P. Bodeveix and M. Filali. The FMONA tool. Technical Report http://www.irit.fr/ACTIVITES/EQ_COS/MF/FMONA, IRIT, may 1999. 206, 214
J.-P. Bodeveix and M. Filali. Experimenting acceleration methods for the validation of infinite state systems. In Dr. Pao-Ann Hsiung, editor, International Workshop on Distributed System Validation and Verification, Institute of Information Science, Academia Sinica, Taiwan, R.O.C., april 2000. to appear. 217
S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionnaly and automatically. In Computer-Aided Verification (CAV’98), volume 1427 of Lecture Notes in Computer Science, pages 319–331, Vancouver, BC, Canada, june 1998. Springer-Verlag. http://www.csl.sri.com/~owre/cav98.html. 208, 212
E.M. Clarke, O. Grumber, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, september 1994. 208
E. W. Dijkstra, W. H. J. Feijen, and A. J. M. van Gasteren. Derivation of a termination detection algorithm for distributed computations. Information Processing Letters, 16(5):217–219, june 1983. 217
M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, 1994. 204
HJJ+95._J.G. Henriksen, J.L. Jensen, M.S. Jorgensen, N. Klarlund, R. Paige, T. Rauhe, and A.B. Sandholm. Mona: Monadic second-order logic in practice. In Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 58–73, Aarhus, May 1995. 204, 206
G.J. Holzmann. Design and validation of computer protocols. Prentice Hall, 1991. 204
Lessens, D. and Saïdi, H. Abstraction of parameterized networks. Electronic notes in theoretical computer science, 9:12, 1997. http://www.elsevier.nl/locate/entcs/volume9.html. 211
A.J. Martin. Distributed mutual exclusion on a ring of processes. Science of Computer Programming, 5(3):265–276, October 1985. 217
S. Owre, J.M. Rushby, and N. Shankar. PVS: A prototype verification system. Lecture Notes in Computer Science, 607, 1992. 204
J.L. Peterson and A. Silberschatz. Operating system concepts. Addison-Wesley, 1985. 214
P. Stenstrom. A survey of cache coherence schemes for multiprocessors. Computer, 23(6):11–25, June 1990. 214
B.K. Szymanski. Mutual exclusion revisited. In fifth Jerusalem conference on information technology, pages 110–117. IEEE Computer Society Press, 1990. 217
W. Thomas. Automata on infinite objects. In J.v. Leeuwen, editor, Handbook of Theoretical Computer Science, pages 133–192. MIT Press, 1990. 205, 209
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodeveix, JP., Filali, M. (2000). FMona: A Tool for Expressing Validation Techniques over Infinite State Systems. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_15
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive