2024-03-28T20:49:16Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000619932023-04-27T10:00:04Z01164:01384:05667:05668
軽量形式手法を用いた車載電子システムの安全性分析に関する研究Analyzing Safety Properties of Automotive Electronic Systems with a Lightweight Formal Methodjpnhttp://id.nii.ac.jp/1001/00061993/Technical Reporthttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=61993&item_no=1&attribute_id=1&file_no=1Copyright (c) 2009 by the Information Processing Society of Japan北九州市立大学大学院国際環境工学研究科アイシン・コムクルーズ株式会社北九州市立大学アイシン精機株式会社 アイシン・コムクルーズ株式会社押川, 倫憲武藤, 嘉伸豊島, 真澄鈴村, 延保鬼頭, 正広本稿では,車載電子システムの信頼性や安全性を高めるために,仕様書を基に軽量形式手法 Alloy で記述及び解析を行った.Alloy を用いた記述及び解析は,ドメイン分析や要求分析工程においてトップダウンに行われることが多いが,本研究では,リバースエンジニアリングの道具として Alloy を用い,対象システムの分析を支援する.実際に,車体系製品を想定した仕様書を基に Alloy で記述及び解析を行うことによって,制約の顕在化やドメイン知識の習得,要求仕様を踏まえた仕様の安全性分析などを行うことができた.結果,開発の早期において抜け漏れを防ぎ,信頼性や安全性の向上に寄与すると考えられる.In this article, we report our experience of applying a lightweight formal method called Alloy to Automobile Electronic Systems(AES). Usually, Alloy model-finding method is used as a top-down approach in domain analysis or requirement analysis phase. Unlike it, we regard Alloy as a reverse engineering tool and apply Alloy model-finding method onto specification and design model. Actually, we constructed Alloy models and analyzed it based on a specification of case study application to an virtual body system in AES. As a result, we could reveal constrains, acquire domain knowledge, and analyze safety properties of designs based on requirement specifications. Hence it can prevent oversights and help to construct high-safety systems. AN10112981研究報告ソフトウェア工学(SE)200931(2009-SE-163)1771842009-03-112009-08-18