Analyzing the Light Control System with PVS.
Adriaan de Groot and
Journal of Universal Computer Science,
Special Issu"Requirements Engineering: The Light Control Case Study",
Volume 6, Number 7, pages 621 - 649, 2000.
Computing Science Institute Nijmegen,
Number CSI-R0017, pp 39, 2000.
The interactive theorem prover
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.
See the additional information