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.