Fromal Methods and their Applications to Safety-Critical Systems of Railways


Takahiko OGINO, Shingo MATSUMOTO
This paper describes a formal approach to requirements specifications for railways safety-critical software systems and their formal safety definitions. Considering the programs and the data in a software system as the axioms and the inference rules in a formal system, we can claim that the system is safe if and only if, within the formal system, we can prove theorems that equivalent to safety requirements. This approach has many advantages. First, a specification is rigorous so that any ambiguity may be excluded. Secondly, specifications can be compared easily so that differences between systems will be clearer than in a natural language. This would be very useful for confirming interoperability for two systems. Thirdly there may be systems or methods to mechanically convert a formal specification into an executable programme. These are the reasons why we started this investigative study. As our study is under way at this stage, in this paper we clarify the underlying principle among results done by excellent researches by overseas railways with each credentials, particularly safety requirements. Some comments of our study plan are also mentioned.