From fault tree analysis to formal system specification and verification with OTS/CafeOBJ

Jianwen Xiang, Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi

    Research output: Contribution to journalArticlepeer-review

    3 Citations (Scopus)

    Abstract

    The aim of this work is to provide a common semantic model for safety analysis and requirements formulation and verification. This paper investigates how the results of one safety analysis technique, fault trees, are interpreted as safety requirements and transformed into formal system specifications written in CafeOBJ, a formal algebraic language. We propose a common semantic model for both formal fault tree analysis and formal system specification by using observational transition systems (OTSs). The method not only can solve the informal problem of traditional fault trees, but more importantly, makes it possible to use the results of fault tree analysis directly, when specifying and verifying the system.

    Original languageEnglish
    Pages (from-to)134-146
    Number of pages13
    JournalComputer Software
    Volume23
    Issue number3
    Publication statusPublished - Oct 30 2006

    All Science Journal Classification (ASJC) codes

    • Software

    Fingerprint Dive into the research topics of 'From fault tree analysis to formal system specification and verification with OTS/CafeOBJ'. Together they form a unique fingerprint.

    Cite this