---
_id: '39061'
abstract:
- lang: eng
  text: 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:
- first_name: Alexander
  full_name: Krupp, Alexander
  last_name: Krupp
- first_name: Wolfgang
  full_name: Müller, Wolfgang
  id: '16243'
  last_name: Müller
- first_name: Ian
  full_name: Oliver, Ian
  last_name: Oliver
citation:
  ama: 'Krupp A, Müller W, Oliver I. Formal Refinement and Model Checking of An Echo
    Cancellation Unit. In: <i>Proceedings of DATE’04 Designers’ Forum</i>. ; 2004.
    doi:<a href="https://doi.org/10.1109/DATE.2004.1269214">10.1109/DATE.2004.1269214</a>'
  apa: Krupp, A., Müller, W., &#38; Oliver, I. (2004). Formal Refinement and Model
    Checking of An Echo Cancellation Unit. <i>Proceedings of DATE’04 Designers’ Forum</i>.
    Proceedings Design, Automation and Test in Europe Conference and Exhibition. <a
    href="https://doi.org/10.1109/DATE.2004.1269214">https://doi.org/10.1109/DATE.2004.1269214</a>
  bibtex: '@inproceedings{Krupp_Müller_Oliver_2004, place={Paris}, title={Formal Refinement
    and Model Checking of An Echo Cancellation Unit}, DOI={<a href="https://doi.org/10.1109/DATE.2004.1269214">10.1109/DATE.2004.1269214</a>},
    booktitle={Proceedings of DATE’04 Designers’ Forum}, author={Krupp, Alexander
    and Müller, Wolfgang and Oliver, Ian}, year={2004} }'
  chicago: Krupp, Alexander, Wolfgang Müller, and Ian Oliver. “Formal Refinement and
    Model Checking of An Echo Cancellation Unit.” In <i>Proceedings of DATE’04 Designers’
    Forum</i>. Paris, 2004. <a href="https://doi.org/10.1109/DATE.2004.1269214">https://doi.org/10.1109/DATE.2004.1269214</a>.
  ieee: 'A. Krupp, W. Müller, and I. Oliver, “Formal Refinement and Model Checking
    of An Echo Cancellation Unit,” presented at the Proceedings Design, Automation
    and Test in Europe Conference and Exhibition, 2004, doi: <a href="https://doi.org/10.1109/DATE.2004.1269214">10.1109/DATE.2004.1269214</a>.'
  mla: Krupp, Alexander, et al. “Formal Refinement and Model Checking of An Echo Cancellation
    Unit.” <i>Proceedings of DATE’04 Designers’ Forum</i>, 2004, doi:<a href="https://doi.org/10.1109/DATE.2004.1269214">10.1109/DATE.2004.1269214</a>.
  short: 'A. Krupp, W. Müller, I. Oliver, in: Proceedings of DATE’04 Designers’ Forum,
    Paris, 2004.'
conference:
  name: Proceedings Design, Automation and Test in Europe Conference and Exhibition
date_created: 2023-01-24T08:53:26Z
date_updated: 2023-01-24T08:53:31Z
department:
- _id: '672'
doi: 10.1109/DATE.2004.1269214
keyword:
- Echo cancellers
- Logic
- Unified modeling language
- Automata
- Data structures
- Boolean functions
- Electronic design automation and methodology
- Prototypes
- Specification languages
- Constraint theory
language:
- iso: eng
place: Paris
publication: Proceedings of DATE’04 Designers' Forum
publication_identifier:
  isbn:
  - 0-7695-2085-5
status: public
title: Formal Refinement and Model Checking of An Echo Cancellation Unit
type: conference
user_id: '5786'
year: '2004'
...