Abstract
Formal refinement as offered by the B method has been shown to be applicable in practice and to scale up. However, it has been recognised that it is difficult communicate a formal B model with customers. Recently, as an interface to rigorous formal B models the UML has been investigated to facilitate this communication. The UML is generally accepted as being a communicating models of systems. Availability of this good vehicle for co g interface to the B method addresses a major problem faced by most formal methods: How to validate a formal model with a customer who is not formal methods expert?
In this chapter we present an approach to the development of a formally verified circuit implementing a Hamming encoder/decoder. The UML-B is used as a formal specification language and the B method is used to prove refinements until the implementation level at which we can translate into VHDL
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J.-R. Abrial. The B-Book — Assigning Programs to Meanings. 1996.
J.-R. Abrial. B#: Toward a synthesis between z and b. In D. Bert and M. Walden, editors, 3nd International Conference of B and Z Users - ZB 2003, Turku, Finland, Lectures Notes in Computer Science, June 2003.
J.-R. Abrial and L. Mussat. Introducing Dynamic Constraints in B. In D. Bert, editor, B’98: Recent Advances in the Development and Use of the B- Method, volume 1393 of LNCS, pages 83–128,1998.
Jean-Raymond Abrial. Event Driven Sequential Program Construction, 2000. http://www.matisseqinetiq.com/links.htm.
Jean-Raymond Abrial and D. Cansell. Click’n’prove: Interactive proofs within set theory. In David Basin and Burkhart Wolff, editors, 16th Intl. Conf Theorem Proving in Higher Order Logics (TPHOLs’2003), volume 2758 of Lecture Notes in Computer Science, pages 1–24. Springer Verlag, September 2003.
J.R. Abrial. Extending B without changing it (for developing distributed systems). In H. Habrias, editor, 1st Conference on the B method, 11 1996.
J.R. Abrial. Formal construction of proved circuits. Technical report, 08 2001. Internal Note.
R. J. R. Back. On correct refinement of programs. Journal of Computer and System Sciences, 23(1):49–68,1979.
R. J. R. Back and J. von Wright. Trace refinement of action systems. In Bengt Jonsson and Joachim Parrow, editors, CONCUR’ 94: Concurrency Theory, 5th International Conference, volume 836 of Lecture Notes in Computer Science, pages 367–384, Uppsala, Sweden, 1994. Springer-Verlag.
D. Cansell and D. M’ery. Integration of the proof process in the system development through refinement steps. In Eugenio Villar, editor, 5th Forum on Specification & Design Language - Workshop SFP in FDL’02 , Marseille, France, Sep 2002.
D. Cansell, Camel Tanougast, Yves Berviller, D. M’ery, Cyril Proch, Hassan Rabah, and Serge Weber. Proof-based design of a microelectronic architecture for mpeg-2 bit-rate measurement. In Forum on specification and Design Languages - FDL’03, Frankfurt, Germany, Sep 2003.
K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0–201-05866–9.
ClearSy — Systems Engineering, Aix-en-Provence, France. Atelier B. Software.
ClearSy— SystemsEngineering. http://www.atelierb.societe.comidocuments.htm. evt2B. Software.
E. W. Dijkstra. A Discipline of Programming. Prenctice-Hall, 1976.
Bruce Powel Douglas. Doing Hard Time. Developing Real-Time Systems with UML, Objects, Frameworks and Patterns. Addison-Wesley, 1999. 0–201-49837–5.
ECS, University of Southampton, http://www.ecs.soton.ac.uk/cfs/U2Bdownloads/U2Bdownloads.htm. U2B Tool. Software.
KeesDA S.A., Grenoble, France. BHDL User Guide.
Hung Ledang and Jeanine Souqui’ eres. Contributions for modelling UML state-charts in B. Lecture Notes in Computer Science, 2335:109—??, 2002.
Michael Leuschel and Michael Butler. ProB: A model checker for B. In Keijiro Araki, Stefania Gnesi, and Dino Mandrioli, editors, FME 2003: Formal Methods, LNCS 2805, pages 855–874. Springer-Verlag, 2003.
Ian Oliver. Experiences of model driven architecture in real-time embedded systems. In Proceedings of FDL02, Marseille, France, Sept 2002., 2002.
Ian Oliver. Model driven embedded systems. In Johan Lilius, Felice Balarin, and Ricardo J. Machado, editors, Proceedings of Third International Conference on Application of Concurrency to System Design ACSD2003, Guimar-aes, Portugal. IEEE Computer Society, June 2002.
Juha Plosila and Tiberiu Seceleanu. Synchronous action systems. Technical Report TUCS TR-192, Turku Centre for Computer Science, Finland, 1998.
Bran Selic, Garth Gullekson, and Paul T. Ward. Real-Time Object- Oriented Modelling. Wiley, 1994.
Colin Snook. Combining UML and B. In Proceedings of FDL ’02, 2002.
Colin Snook and Michael Butler. Using a Graphical Design Tool for Formal Specification. In Dumke and Abran, editors, Proceedings 13th Annual Workshop of the Psychology of Programming Interest Group, 2001.
Colin Snook and Rachel Harrison. Practitioners’ Views on the Use of Formal Methods: An Industrial Survey by Structured Interview. Information and Software Technology, 43(4):275–283, 2001.
Colin Snook, Ian Oliver, and Michael Butler. Towards a UML Profile for UML-B. Technical report, University of Southampton, 2003.
VSI Working Group. IEEE P1076.6/D2.01 — Draft Standard For VHDL Register Transfer Level Synthesis. Unapproved Draft, IEEE, 2001.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science+Business Media New York
About this chapter
Cite this chapter
Cansell, D., Hallerstede, S., Oliver, I. (2004). UML-B Specification and Hardware Implementation of a Hamming Coder/Decoder. In: Mermet, J. (eds) UML-B Specification for Proven Embedded Systems Design. Springer, Boston, MA. https://doi.org/10.1007/978-1-4020-2867-0_16
Download citation
DOI: https://doi.org/10.1007/978-1-4020-2867-0_16
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-5256-1
Online ISBN: 978-1-4020-2867-0
eBook Packages: Springer Book Archive