Home // COMPUTATION TOOLS 2010, The First International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article

Debugging PVS specifications of control logics via event-driven simulation

Authors:
Cinzia Bernardeschi
Luca Cassano
Andrea Domenici
Paolo Masci

Keywords: PVS; simulation; formal specification; validation

Abstract:
In this paper, we present a framework aimed at simulating control logics specified in the higher-order logic of the emph{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.

Pages: 1 to 7

Copyright: Copyright (c) IARIA, 2010

Publication date: November 21, 2010

Published in: conference

ISSN: 2308-4170

ISBN: 978-1-61208-112-0

Location: Lisbon, Portugal

Dates: from November 21, 2010 to November 26, 2010