[comp.specification] Formal Methods Tools from HP Labs

pcg@hplb.hpl.hp.com (Patrick Goldsack) (03/12/91)

Here at Hewlett-Packard labs in Bristol, England, we have been working
on a dialect of VDM together with supporting tools and documentation,
including course and reference material.
These are currently in use here at labs and in various
divisions around the company on product developments.

The notation is essentially a small and regular VDM dialect (uses pre/post specification,
relational modelling of state, type invariants and so on) with certain
extensions notably polymorphism and a module system similar in concept to that
available in algebraic languages such as CLEAR.

The tools (an early version was demonstrated at VDM-90 in Kiel) consist of
   - a serverised database for holding specification components
      (allows distributed network transparent access to specifiations,
       multiple documents with multiple references to a specification
       component without textual copying, etc)
   - a type checker which can deal with equally well with
        * individual declarations (such as a single function) even 
          in the presence of free identifiers,
        * complex module combinations
   - document formatting tools which generate the latex source
     for the specification components embedded in doucment source
   - an emacs-based interface for the above

The notation and tools are designed to support the incremental development of
specifications (Z-style) using a VDM-like notation. Thus, for example,
individual functions or types may be developed incrementally in a
document embedded in textual descriptions. These may then be combined
in a module to create the final `closed' specification.

Having received some interest from third parties,
we are now considering making the notation and tools available to a wider
audience, both educational and industrial.

We are looking initially for a limited number of beta-test sites
for these tools amongst users of formal specification notations.
The only requirement from the beta-sites would be a report after some
agreed period (e.g. 6 months) on the tools and notation, their usability,
bugs and so on.

If you are interested in the tools, notation or documentation
could you please mail me letting me know

   1) who you are

   2) how you might use the tools/notation

   3) if you are interested in becoming a beta-test site
      for the tools or notation

      or

      if you are not interested in beta-test but would
      be interested in the tools or notation in the longer-term

   4) platforms on which the software would be required

Note that this software is a `labs prototype' not an HP product, hence support
would not be via normal HP channels, nor of the level expected for a product.
Support will be on an informal basis via e-mail/phone direct with us
with no guarantees or liability on our part - although it is generally
in our interest to fix bugs and carry out enhancements.

We hope that the beta sites would be sufficiently familiar with specification
notations such as Z and VDM that formal training would not be required.
A course might be arranged if necessary, but would have to be
charged for at an appropriate consultancy rate (the course material itself
is not part of the beta-release).

For the beta-release there would be no charge from HP, although we
do currently rely on one piece of third party software for which a small
license fee may have to be paid.

Patrick Goldsack
Software Engineering Laboratory
Hewlett-Packard Labs,
Filton Road,
Bristol,
UK
+44-272-799910 x24176
pcg@hplb.hpl.hp.co.uk
--
_____________________________________________

Patrick Goldsack

HP Labs