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.
References in zbMATH (referenced in 1 article , 1 standard article )
Showing result 1 of 1.
- Bodeveix, J.-P.; Filali, M.: FMona: A tool for expressing validation techniques over infinite state systems (2000)