In this paper we present an event-driven simulation engine for executing formal specifications of digital systems in the Prototype Verification System (PVS). The engine is intended to be used as an efficient debugging mechanism to validate PVS models. Once the simulation experiments give sufficient confidence in the correctness of the formal specifications, the theorem prover of PVS can be used to verify desired properties of interest.
Event-driven simulation of control logics from logical specifications, Technical Report DIIEIT-2010-05-01
BERNARDESCHI, CINZIA;CASSANO, LUCA MARIA;DOMENICI, ANDREA;MASCI, PAOLO MANUEL
2010-01-01
Abstract
In this paper we present an event-driven simulation engine for executing formal specifications of digital systems in the Prototype Verification System (PVS). The engine is intended to be used as an efficient debugging mechanism to validate PVS models. Once the simulation experiments give sufficient confidence in the correctness of the formal specifications, the theorem prover of PVS can be used to verify desired properties of interest.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
