Paolo Masci

Citation:

Bernardeschi C, Cassano L, Domenici A, Masci P.  2010.  Debugging PVS Specifications of Control Logics via Event-driven Simulation. Proc. 1st Intl. Conf. on Computational Logics, Algebras, Programming, Tools, and Benchmarking (ComputationTools2010), copy at www.tinyurl.com/jmx9bu8

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.

Citation Key: