Application name:

DUST-EXPERT

Organisation:

Adelard, for the UK Health and Safety Executive

Method:

VDM-SL

Tools:

The IFAD VDM-SL Toolbox

Domain:

Knowledge-based systems, advisory system, safety-related

Period:

July 1995 - April 1997

Size:

Approx. 20K lines VDM-SL and similar size of implementation (in Prolog)

Description:

DUST-EXPERT is a safety-related knowledge-based system, running on PCs under Microsoft Windows 3.1, to advise on the protection of vessels that contain potentially explosive dusts. The system, which is called DUST-EXPERT, includes: decision trees on venting, suppression, containment, inerting and exclusion of ignition sources, which enable users to select the best approach to dealing with potential dust explosions; several methods for calculating the size of vents to limit the pressure rise in the event of a dust explosion; a data base of explosible dust properties , a new method for the estimation of the strength of equipment, and context-sensitive, hypertext help covering precaution techniques, explosion violence factors, explosibility tests, and using the system.

A full Safety Case is being produced to justify the development. This is based on: a formal specification using the Vienna Development Method (VDM); hand proofs of safety properties on the VDM specification; execution of the VDM specification using the IFAD Toolbox; implementation in Prolog; and a statistically significant quantity of testing of the integrated system.

Conclusions:

At the top level VDM was used for the specification, and it is translated almost one-for-one into Prolog. Since the software has to run in a standard Windows environment, a software Hazops was performed and defensive checks were included (e.g. numbers typed in are redisplayed by the receiving software so the user can detect unintended values).

Considering the management aspects; as in 00-56, an independent safety auditor (ISA) is used to examine the safety claims and safety case arguments. The development is also integrated into our standard ISO 9000/TickIT quality management system - around 50 reviews have been performed (around one per week) so there is a high level of traceability. The development involves many thousands of lines of VDM, so tools support was essential and the IFAD Toolbox was used to ensure clean VDM - it could also be used as an animation tool for the statistical tests. Such tool support is essential for any significant software development, together with appropriate configuration management software.

Publications:

None.

Contact:

Name:	-
Organisation:	Adelard
Address:	Coborn House, 3 Coborn Road, London E3 2DA
Country:	UK
Phone number:	+44 (181) 9831708
Fax:	+44 (181) 9831845
Personal website:	http://www.adelard.co.uk

Remarks:

DUST-EXPERT is a trade mark of the HSE and the BMHB.

© copyright 2004 | Formal Methods Europe