FORMAL METHODS AND THEIR APPLICATIONS TO SAFETY-CRITICAL SYSTEMS OF RAILWAYS

This paper describes a formal approach to requirements specifications for railway 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, it is claimed that this system is safe if, and only if, within the formal system, theorems that are equivalent to the safety requirements can be proved. This approach has the following advantages: 1) a specification is so rigorous that any ambiguity may be excluded; 2) specifications can be compared easily so that differences between systems will be clear; and 3) there may be systems or methods to mechanically convert a formal specification into an executable program. Part of an on-going study, this paper looks into the research carried out and seeks to clarify the underlying principle, and, in particular, its safety requirements. Some indications of possible future studies are included.

  • Availability:
  • Corporate Authors:

    Railway Technical Research Institute

    2-8-38, Hikari-cho, Kokubunji-shi
    Tokyo 185,   Japan 
  • Authors:
    • Ogino, T
    • Hirao, Y
  • Publication Date: 1995-12

Language

  • English

Media Info

Subject/Index Terms

Filing Info

  • Accession Number: 00716415
  • Record Type: Publication
  • Files: TRIS
  • Created Date: Feb 21 1996 12:00AM