University of Hertfordshire


  • P.N. Taylor
  • C. Britton
View graph of relations
Original languageEnglish
PublisherUniversity of Hertfordshire
Publication statusPublished - 1994

Publication series

NameUH Computer Science Technical Report
PublisherUniversity of Hertfordshire


This paper addresses three main issues. Firstly, the combination of formal specification languages to model proposed systems. For this paper we introduce the dual specification of a case study system using the formal languages LOTOS and the Z notation to capture the behaviour of the complete system, including the modelling of data abstraction, information hiding and modularisation. Secondly, the production of an industrial-strength specification using a mechanical, automated CASE tool to verify the syntax of the formal specification. It is hoped that specifications which are verified mechanically will be more widely acceptable to industry because of the consistency enforced by the CASE tools used to check them. Finally, the transition from formal specification to implementation using the dual formal specification approach introduced in this paper.

ID: 96002