zbMATH — the first resource for mathematics

FMona: A tool for expressing validation techniques over infinite state systems. (English) Zbl 0971.68601
Graf, Susanne (ed.) et al., Tools and algorithms for the construction and analysis of systems. 6th international conference, TACAS 2000. Held as part of the joint European conferences on theory and practice of software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1785, 204-219 (2000).
Summary: 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.
For the entire collection see [Zbl 0935.00048].

68U99 Computing methodologies and applications
68Q60 Specification and verification (program logics, model checking, etc.)
FMona; PVS