![]() ![]() |
|
タケヤマ マコト
Takeyama Makoto 武山 誠 所属 神奈川大学 理学部 情報科学科 神奈川大学大学院 理学研究科 理学専攻(情報科学領域) 職種 教授 |
|
言語種別 | 英語 |
発行・発表の年月 | 2013 |
形態種別 | その他論文 |
査読 | 査読あり |
標題 | Assurance Case as a Proof in a Theory - towards formulation of rebuttals |
執筆形態 | 共著 |
掲載誌名 | Assuring the Safety of Systems: Proceedings of the Twenty-first Safety-critical Systems Symposium |
掲載区分 | 国外 |
巻・号・頁 | pp.205-230 |
著者・共著者 | Yoshiki Kinoshita, Makoto Takeyama |
概要 | A framework is given to formulate an assurance case as a pair of a formal theory (vocabulary and basic assumptions; a formal model) and a proof in it, thus objectifying ontological presumptions separately from reasoning based on it. Our formulation is given in Agda, a programming and proof description language based on constructive type theory. Emphasis on explicit presumptions improves upon currently prevailing structured-argument notations such as GSN and CAE. Changes and vagueness in modern complex systems must be reflected by rebuttals to their assurance cases. We sketch our approach to formulate rebuttals to that end, where objectification of ontological presumptions works effectively. |