Application of Formal Methods to Signalling Systems Using Techniques Based on Stepwise Refinement
Natsuki Terada · Quarterly Report of RTRI · 2008
Benefits can be expected from the use of formal methods in increasing the reliability of software. In preparing the formal specifications of complicated systems from a preliminary draft text, stepwise revisions are very useful in creating specifications that are easily understandable and in producing verified code that satisfies the specifications. In this report, we first explain the concept of gradual revision, which involves initially writing abstract specifications with minimal conditions and then refining them until they are serviceable. Next, we present an example in which the permissive speed of a train is calculated from a given stop distance.