Analyzing the Light Control System with PVS
Дата
Авторы
De Groot,Adriaan
Hooman,Jozef
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
requirements engineering , specification , PVS