Brandin, B., Malik, R. & Malik, P. (2004). Incremental verification and synthesis of discrete-event systems guided by counter-examples. IEEE Transactions on Control Systems Technology, 12(3), 387-401.
Permanent Research Commons link: http://hdl.handle.net/10289/1300
This article presents new approaches to system verification and synthesis based on subsystem verification and the novel combined use of counterexamples and heuristics to identify suitable subsystems incrementally. The scope of safety properties considered is limited to behavioral inclusion and controllability. The verification examples considered provide a comparison of the approaches presented with straightforward state exploration and an understanding of their applicability in an industrial context.
Institute of Electrical and Electronics Engineers, Inc. (IEEE Inc.)
Copyright IEEE 2004