A tool for visual and formal modelling of software designs

Amalio, Nuno and Glodt, Christian (2014) A tool for visual and formal modelling of software designs. Science of Computer Programming, 98 (1). pp. 52-79. ISSN 0167-6423

Full text not available from this repository. (Request a copy)


Diagrams are ubiquitous in software engineering and widely used for software modelling. The visual contract language (VCL) enables an approach to software design modelling that is entirely graphical and has a mathematical basis. VCL’s main novelties lie in its capacity to describe predicates visually and in its graphical front-end to formal modelling. VCL is brought to life in the visual contract builder (VCB) tool presented in this paper. VCB provides diagram editors for the whole VCL suite, it type-checks diagrams and generates Z formal specifications from them; the Z specification enables formal verification and validation using Z theorem provers. The paper evaluates VCB based on the results of a survey carried out in the context of a controlled experiment. The work presented here is a contribution to the area of visual design modelling: the paper presents a state of the art tool supporting the novel VCL language and concrete empirical results on the usefulness and effectiveness of tool and language in particular, suggesting benefits of visual modelling in general.

Item Type: Article
Identification Number: https://doi.org/10.1016/j.scico.2014.05.002
7 May 2014Accepted
21 May 2014Published Online
Uncontrolled Keywords: Visual modelling languages MDE Formal methods Tool-support Empirical evaluation
Subjects: CAH11 - computing > CAH11-01 - computing > CAH11-01-01 - computer science
Divisions: Faculty of Computing, Engineering and the Built Environment
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology
Depositing User: Ian Mcdonald
Date Deposited: 05 Jan 2017 15:41
Last Modified: 22 Mar 2023 12:02
URI: https://www.open-access.bcu.ac.uk/id/eprint/3768

Actions (login required)

View Item View Item


In this section...