研究者情報 | 神奈川大学

キノシタ　ヨシキ Kinoshita Yoshiki 木下　佳樹所属神奈川大学情報学部計算機科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	日本語
発行・発表の年月	2013/03
形態種別	著書
査読	査読あり
標題	Assurance Case as a Proof in a Theory: towards Formulation of Rebuttals, in "Assuring the Safety of Systems, Proceedings of the Twenty-first Safety-Critical Systems Symposium, Bristol, UK, 5-7th February 2013"
執筆形態	共著
出版社・発行元	Safety-Critical Systems Club on Amazon (http://www.amazon.co.uk/Assuring-Safety-Systems-Twenty-first-Safety-critical/dp/1481018647), ISBN 978-1481018647
巻・号・頁	205-230頁
著者・共著者	Yoshiki Kinoshita and 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.