%0 Conference Paper %1 krupp_04_formal %A Krupp, Alexander %A Mueller, Wolfgang %A Oliver, Ian %B Design, Automation and Test in Europe Conference and Exhibition, 2004. Proceedings %D 2004 %J Design, Automation and Test in Europe Conference and Exhibition, 2004. Proceedings %K refinement 2004 b statecharts model_checking uml %P 102--107 Vol.3 %R 10.1109/DATE.2004.1269214 %T Formal refinement and model checking of an echo cancellation unit %U http://dx.doi.org/10.1109/DATE.2004.1269214 %V 3 %X 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.

@inproceedings{krupp_04_formal, 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.}, added-at = {2009-02-12T11:38:45.000+0100}, author = {Krupp, Alexander and Mueller, Wolfgang and Oliver, Ian}, biburl = {https://www.bibsonomy.org/bibtex/2cc2b181cfebf65a7689009bcb060f46c/leonardo}, booktitle = {Design, Automation and Test in Europe Conference and Exhibition, 2004. Proceedings}, citeulike-article-id = {2083417}, doi = {10.1109/DATE.2004.1269214}, interhash = {0144666608a3bfdec14e34b55f8d1e3f}, intrahash = {cc2b181cfebf65a7689009bcb060f46c}, journal = {Design, Automation and Test in Europe Conference and Exhibition, 2004. Proceedings}, keywords = {refinement 2004 b statecharts model_checking uml}, pages = {102--107 Vol.3}, posted-at = {2007-12-09 19:30:40}, priority = {4}, timestamp = {2009-02-12T11:38:45.000+0100}, title = {Formal refinement and model checking of an echo cancellation unit}, url = {http://dx.doi.org/10.1109/DATE.2004.1269214}, volume = 3, year = 2004 }