PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Meolic R., Gnesi S., Trentanni G. WCS: a Witness and Counterexample Server. Technical report, 2011.
 
 
Abstract
(English)
Witness and Counterexample Server (WCS) is planned to be a suite of tools designed to asses the ability of model hecking techniques to increase effectiveness of hardware/software testing activities. It is focused on witnesses and counterexamples produced by model checkers. Currently, a BDD-based model checker with the ability of generating linear witnesses and counterexamples, and witness and counterexample automata is available. Witness and counterexample automata are finite automata recognizing a set of all finite linear witnesses and counterexamples for a given formula over a given model, respectively. WCS is organized as a web service, in order to provide public access to the functionality of verification tools.
Subject Model checking
Automata
D.2.4 Software/Program Verification
D.4 Operating Systems


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional