From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ
スポンサーリンク
概要
- 論文の詳細を見る
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.
- Information and Media Technologies 編集運営会議の論文
著者
-
Ogata Kazuhiro
Nec Software Hokuriku Ltd.
-
Kong Weiqiang
School Of Information Science Japan Advanced Institute Of Science And Technology (jaist)
-
Xiang Jianwen
School Of Information Science Japan Advanced Institute Of Science And Technology
-
FUTATSUGI Kokichi
School of Information Science
-
Kong Weiqiang
School of Information Science, Japan Advanced Institute of Science and Technology
-
Ogata Kazuhiro
NEC Software Hokuriku, Ltd./Research Center for Trustworthy e-Society, Japan Advanced Institute of Science and Technology
関連論文
- Proof Score Approach to Verification of Liveness Properties
- Analysis of membership sharing in digital subscription services
- Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
- A Specification Translation from Behavioral Specifications to Rewrite Specifications
- Algebraic approaches to formal analysis of the mondex electronic purse system
- Formal analysis of the iKP electronic payment protocols
- A Behavioral Specification of Imperative Programming Languages
- Concurrent Reflective Computations in Rewriting Logic(Theory of Rewriting Systems and Its Applications)
- A Family of License Languages
- A Scenario-based Object-Oriented Modeling Method with Algebraic
- A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity"
- A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity"
- From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ