日時 2004年２月１３日（金）
場所 SRA先端技術研究所会議室
当日の資料
後日の資料
講師 柳生孝昭さん
講演題：
工業製品と組込みSoftwareの形式的要求仕様
--暦時計と自動航空Systemを題材として--
内容要約：
暦時計と自動航空Systemを題材として，要求仕様記述の
形式的方法を工業製品の組込みsoftwareに適用する際の，
特徴的な問題を考察する．記述のための言語は，部分的に
解釈された１階述語論理を用いた．工業製品の振舞いは
一般に，状態遷移の因果的連鎖として捉えられ，組込み
softwareは言わば人工的な因果法則の役割を果たす．
従って状態遷移という動的な側面の，(通常，静的側面のみ
有効と見なされている)述語論理による記述と，古来難題と
されて来た因果関係の定式化が，問題の核心に在る．これは
適切な状態空間と，その上での２項または３項述語の定義，
及び因果法則を現す公理の設定によって，これらの問題の解決
を試みるものである．更に，完成した仕様の分析を通して，
因果連鎖の並列性やfeedbackの存在を顕にし得ることを示す．
これらは仕様の実現（詳細設計）を考案する，また予め製品の
異常な振舞いを見出すために有効であろう．
場所 SRA先端技術研究所会議室
--------------------------------------------------
SEA 月例会 (Feb. 2003) 参加申込用紙
氏名(ふりがな)：
組織名：
部門・役職：
住所： (〒 − )
Tel:
E-Mail:
種別(該当欄にチェック):□ 社会人 1000円
□ 学生 500円
--------------------------------------------------
ｓｓ＠ｓｈｉｎｓａｈａｒａ．ｃｏｍ