Skip to the content

Experience with mural in formalising Dust-Expert

Vadera, S, Meziane, F and Huang, MLL 2001, 'Experience with mural in formalising Dust-Expert' , Information and Software Technology, 43 (4) , pp. 231-240.

[img]
Preview
PDF (Author version)
Download (216kB) | Preview

    Abstract

    The mural system was an outcome of a significant effort to develop a support tool for the effective use of a full formal methods development cycle. Experience with it, however, has been limited to a small number of illustrative examples that have been carried out by those closely associated with its development and implementation. This paper aims to remedy this situation by describing the experience of using mural for specifying Dust-Expert, an expert system for the relief venting of dust explosions in chemical processes. The paper begins by summarising the main requirements for Dust-Expert, and then gives a ¯avour of the VDM speci®cation that was formalised using mural. The experience of using mural is described with respect to users' expectations that a formal methods tool should: (i) spot any inconsistencies; (ii) help manage and organise the specifications and allow one to easily add, access, update and delete specifications; (iii) help manage and carry out the refinement process; (iv) help manage and organise theories; (v) help manage and carry out proofs. The paper concludes by highlighting the strengths and weaknesses of mural that could be of interest to those developing the next generation of formal methods development tools.

    Item Type: Article
    Uncontrolled Keywords: Mural, VDM, formal methods, safety, tools
    Themes: Subjects / Themes > Q Science > QA Mathematics > QA075 Electronic computers. Computer science
    Subjects outside of the University Themes
    Schools: Colleges and Schools > College of Science & Technology
    Colleges and Schools > College of Science & Technology > School of Computing, Science and Engineering
    Colleges and Schools > College of Science & Technology > School of Computing, Science and Engineering > Data Mining and Pattern Recognition Research Centre
    Journal or Publication Title: Information and Software Technology
    Publisher: Elsevier
    Refereed: Yes
    ISSN: 09505849
    Related URLs:
    Depositing User: H Kenna
    Date Deposited: 07 Jan 2009 15:12
    Last Modified: 20 Aug 2013 16:51
    URI: http://usir.salford.ac.uk/id/eprint/945

    Actions (login required)

    Edit record (repository staff only)

    Downloads per month over past year

    View more statistics