Title :
Developing reactive systems in a VDM framework
Author_Institution :
Unite d´´Inf., Univ. Catholique de Louvain, Louvain-La-Neuve, Belgium
Abstract :
The detailed validation of reactive systems, using an extension of VDM, is studied. The specification and proof of behavioural aspects is added to VDM by using traces of the input/output activities. The major objective of the work is to progress in the comprehension of the practical implications of the specification, design, and symbolic validation of machine-checked reactive systems
Keywords :
Vienna development method; formal specification; program verification; VDM framework; behavioural aspects; detailed validation; input/output activities; machine-checked reactive systems; practical implications; symbolic validation; Explosions; Formal specifications; Protocols; Software systems;
Conference_Titel :
Software Specification and Design, 1991., Proceedings of the Sixth International Workshop on
Conference_Location :
Como
Print_ISBN :
0-8186-2320-9
DOI :
10.1109/IWSSD.1991.213068
