JUCS - Journal of Universal Computer Science 6(7): 621-649, doi: 10.3217/jucs-006-07-0621
Analyzing the Light Control System with PVS
expand article infoAdriaan De Groot‡, Jozef Hooman‡
‡ Computing Science Institute, University of Nijmegen, University of Nijmegen, Netherlands

Corresponding author: Adriaan De Groot ( adridg@cs.kun.nl )

© Adriaan De Groot, Jozef Hooman.
This article is freely available under the J.UCS Open Content License.
Citation: De Groot A, Hooman J (2000) Analyzing the Light Control System with PVS. JUCS - Journal of Universal Computer Science 6(7): 621-649. https://doi.org/10.3217/jucs-006-07-0621
Open Access
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.
Keywords
requirements engineering, specification, PVS