In this paper, we present a framework aimed at simulating control logics specified in the higher-order logic of the Prototype Verification System. The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer simulates the specified system by providing its input waveforms as functions from time to logic levels. Once the simulation experiments give sufficient confidence in the correctness of the specification, the model can serve as a basis for the formal verification of desired properties of interest. A simple case study from a nuclear power plant application is shown. This paper is a contribution to research aimed at improving the development process of safety-critical systems by integrating simulation and formal specification methods.

Debugging PVS specifications of control logics via event-driven simulation

BERNARDESCHI, CINZIA;CASSANO, LUCA MARIA;DOMENICI, ANDREA;MASCI, PAOLO MANUEL
2010

Abstract

In this paper, we present a framework aimed at simulating control logics specified in the higher-order logic of the Prototype Verification System. The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer simulates the specified system by providing its input waveforms as functions from time to logic levels. Once the simulation experiments give sufficient confidence in the correctness of the specification, the model can serve as a basis for the formal verification of desired properties of interest. A simple case study from a nuclear power plant application is shown. This paper is a contribution to research aimed at improving the development process of safety-critical systems by integrating simulation and formal specification methods.
9781612080017
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.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11568/194201
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact