Analyzing the Light Control System with PVS.

Adriaan de Groot and Jozef Hooman

Journal of Universal Computer Science, Special Issu"Requirements Engineering: The Light Control Case Study", Volume 6, Number 7, pages 621 - 649, 2000.
Technical Report, Computing Science Institute Nijmegen, Number CSI-R0017, pp 39, 2000.

ABSTRACT

The interactive theorem prover PVS is used to formalize the user needs of the Light Control system. First the system is modeled at a high level of abstraction, in terms of properties the user can observe. After resolving ambiguities and conflicts, a refinement is defined, using dimmable light actuators. Correctness of the refinement has been proved in PVS, under the assumption that there are no internal delays. Next these internal delays are taken into account, leading to a new notion of delay-refinement which allows abstraction from delays such that systems with delays can be seen as an approximation of an undelayed specification.

Postscript

See the additional information , including original problem description and PVS files.