Using UML-B and U2B for formal refinement of digital components

  • Snook C
  • Sandstrom K
  • 5


    Mendeley users who have this article in their library.
  • N/A


    Citations of this article.


In this paper we look at using formal methods to verify
the transformation of a digital design from abstract functional
specification to bit level implementation. As both authors are
in-experienced in formal proof we saw this as a test of the
practicality of introducing proof tools in an industrial setting
rather than an exemplar of such methods Rigorous verification is
desirable in digital design because mistakes can be extremely
costly. However, there are drawbacks and barriers to introducing
formal notations. Formal notations are abstraction hungry, viscous
and require insight, experience and look-ahead. Hence we specialise
the UML to alleviate these problems by providing a semi-graphical
form of the formal notation B based on existing visual modelling
tools. With a small case study, we show the use of B-UML using an
event style of modelling to refine a macro level function into a
cascade of single bit cells. We attempt to prove the refinement with
the assistance of available proof tools but find that the problem is
deceptively difficult

Author-supplied keywords

  • B method
  • B-UML
  • UML

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

There are no full text links


  • C Snook

  • K Sandstrom

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free