Formal Refinement and Model Checking of An Echo Cancellation Unit
A. Krupp, W. Müller, I. Oliver, in: Proceedings of DATE’04 Designers’ Forum, Paris, 2004.
Download
No fulltext has been uploaded.
Conference Paper
| English
Author
Krupp, Alexander;
Müller, WolfgangLibreCat;
Oliver, Ian
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.
Keywords
Publishing Year
Proceedings Title
Proceedings of DATE’04 Designers' Forum
Conference
Proceedings Design, Automation and Test in Europe Conference and Exhibition
ISBN
LibreCat-ID
Cite this
Krupp A, Müller W, Oliver I. Formal Refinement and Model Checking of An Echo Cancellation Unit. In: Proceedings of DATE’04 Designers’ Forum. ; 2004. doi:10.1109/DATE.2004.1269214
Krupp, A., Müller, W., & Oliver, I. (2004). Formal Refinement and Model Checking of An Echo Cancellation Unit. Proceedings of DATE’04 Designers’ Forum. Proceedings Design, Automation and Test in Europe Conference and Exhibition. https://doi.org/10.1109/DATE.2004.1269214
@inproceedings{Krupp_Müller_Oliver_2004, place={Paris}, title={Formal Refinement and Model Checking of An Echo Cancellation Unit}, DOI={10.1109/DATE.2004.1269214}, booktitle={Proceedings of DATE’04 Designers’ Forum}, author={Krupp, Alexander and Müller, Wolfgang and Oliver, Ian}, year={2004} }
Krupp, Alexander, Wolfgang Müller, and Ian Oliver. “Formal Refinement and Model Checking of An Echo Cancellation Unit.” In Proceedings of DATE’04 Designers’ Forum. Paris, 2004. https://doi.org/10.1109/DATE.2004.1269214.
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: 10.1109/DATE.2004.1269214.
Krupp, Alexander, et al. “Formal Refinement and Model Checking of An Echo Cancellation Unit.” Proceedings of DATE’04 Designers’ Forum, 2004, doi:10.1109/DATE.2004.1269214.
Google Scholar
ISBN Search