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.
Keywords for this software
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Havlena, Vojtěch; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Automata terms in a lazy (\mathrmWSk\mathrmS) decision procedure (2021)
- Havlena, Vojtěch; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Automata terms in a lazy (\mathrmWSk\mathrmS) decision procedure (2019)
- Bodeveix, J.-P.; Filali, M.: FMona: A tool for expressing validation techniques over infinite state systems (2000)