Loading...
Thumbnail Image
Publication

Incremental system verification and synthesis of minimally restrictive behaviours

Abstract
An incremental approach to system verification is proposed, for system behaviours and safety properties described by means of finite-string languages and finite-state automata. Properties are verified with respect to subsystems of the overall system, nevertheless allowing assertions to be made about the entire system satisfying such properties. The proposed approach considers satisfaction of properties, controllability, and synthesis as successive verification steps. Furthermore, it allows the incremental augmentation of the system to be verified: after each verification step, either the desired property is verified, or a counter example is obtained, which, together with heuristics, provides the basis for the augmentation of a given subsystem for the next verification step.
Type
Conference Contribution
Type of thesis
Series
Citation
Malik, Robi (2000). Incremental system verification and synthesis of minimally restrictive behaviours. Proceedings of the 2000 American Control Conference, 6, 4056-4061.
Date
2000
Publisher
IEEE
Degree
Supervisors
Rights
Copyright IEEE 2000.