Home // International Journal On Advances in Software, volume 4, numbers 3 and 4, 2011 // View article

Simulation and Test-Case Generation for PVS Specifications of Control Logics

Authors:
Cinzia Bernardeschi
Luca Cassano
Andrea Domenici
Paolo Masci

Keywords: simulation; validation; test-case generation; control logics

Abstract:
We describe a framework for the simulation of 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 defines a system architecture by composing its model out of library modules, possibly introducing new module definitions, and simulates the behaviour of the system model by providing its input waveforms, which are given as functions from time to logic levels. The generation of simulation scenarios (test cases) can be automated by using parametric waveforms that can be instantiated through universal and existential quantifiers. We demonstrate the simulation capabilities of our framework on two simple case studies from a nuclear power plant application. The main feature of this approach is that our formal specifications are executable. Moreover, once the simulation experiments give developers sufficient confidence in the correctness of the specification, the logic models can serve as the basis for its formal verification.

Pages: 327 to 341

Copyright: Copyright (c) to authors, 2011. Used with permission.

Publication date: April 30, 2012

Published in: journal

ISSN: 1942-2628