@inproceedings{39061,
  abstract     = {{This article presents an approach, which combines theorem proving-based refinement with model checking for state based real-time systems. Our verification flow 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, refined state diagrams are verified against their abstract representation. The approach is presented by means of the refinement of a digital echo cancellation unit.}},
  author       = {{Krupp, Alexander and Müller, Wolfgang and Oliver, Ian}},
  booktitle    = {{Proceedings of DATE’04 Designers' Forum}},
  isbn         = {{0-7695-2085-5}},
  keywords     = {{Echo cancellers, Logic, Unified modeling language, Automata, Data structures, Boolean functions, Electronic design automation and methodology, Prototypes, Specification languages, Constraint theory}},
  title        = {{{Formal Refinement and Model Checking of An Echo Cancellation Unit}}},
  doi          = {{10.1109/DATE.2004.1269214}},
  year         = {{2004}},
}