loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Design, Automation and Test in Europe Conference and Exhibition Designers? Forum (DATE'04)
Formal Refinement and Model Checking of an Echo Cancellation Unit
Paris, France
February 16-February 20
ISBN: 0-7695-2085-5
ASCII Text
x 
 
Alexander Krupp, Wolfgang Mueller, Ian Oliver, "Formal Refinement and Model Checking of an Echo Cancellation Unit," Design, Automation and Test in Europe Conference and Exhibition, vol. 3, pp. 30102, Design, Automation and Test in Europe Conference and Exhibition Designers? Forum (DATE'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/DATE.2004.1269214,
author = {Alexander Krupp and Wolfgang Mueller and Ian Oliver},
title = {Formal Refinement and Model Checking of an Echo Cancellation Unit},
journal ={Design, Automation and Test in Europe Conference and Exhibition},
volume = {3},
year = {2004},
issn = {1530-1591},
pages = {30102},
doi = {http://doi.ieeecomputersociety.org/10.1109/DATE.2004.1269214},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Design, Automation and Test in Europe Conference and Exhibition
TI - Formal Refinement and Model Checking of an Echo Cancellation Unit
SN - 1530-1591
SP
EP
A1 - Alexander Krupp,
A1 - Wolfgang Mueller,
A1 - Ian Oliver,
PY - 2004
KW - null
VL - 3
JA - Design, Automation and Test in Europe Conference and Exhibition
ER -
 
Alexander Krupp, Paderborn University
Wolfgang Mueller, Paderborn University
Ian Oliver, Nokia Research Center
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.
Citation:
Alexander Krupp, Wolfgang Mueller, Ian Oliver, "Formal Refinement and Model Checking of an Echo Cancellation Unit," date, vol. 3, pp.30102, Design, Automation and Test in Europe Conference and Exhibition Designers? Forum (DATE'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.