Developing reactive systems in a VDM framework

摘要

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.