Increasing the usability of formal specification techniques through a combination of complementary formal languages and automated verification tools

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.