/KMO04/
Alexander Krupp, Wolfgang Müller, Ian Oliver:
Formal Refinement and Model Checking of an Echo Cancellation Unit

In Proceedings of DATE04 Designers' Forum, Paris, IEEE CS Press, Los Alamitos, USA, 2004

+ Download

Abstract:
This article presents an approach, which combines theorem proving-based renement with model checking for state based real-time systems. Our verication ow starts from UML state diagrams, which are translated to the formal B language and are model checked for real-time properties. By means of the B language and a B theorem prover, re- ned state diagrams are veried against their abstract representation. The approach is presented by means of the re- nement of a digital echo cancellation unit.