EXPERIENCES USING FORMAL METHODS WITHIN THE TMST PROJECT

A specification is supposed to describe what a system is required to do without giving details as to how this should be achieved. Many people think that natural languages are sufficient for this purpose but such languages are inherently ambiguous. A formal specification language is based on mathematics and, as such, should provide a specification that is clear, concise and, perhaps most importantly, unambiguous. The Trans Manche Super Train (Channel Tunnel Train) will have a computerized information system that will comprise a number of programmable logic controllers and real-time computers distributed along its length. The train will be made up of two power cars (one at each end) with eighteen trailer couches. The formal specification language Z was used within the TMST project. This paper outlines how Z was used, both to write parts of the specification and to validate parts of the specification written in English. The paper concludes by discussing the usefulness of Z within the TMST project.