講演抄録/キーワード |
講演名 |
2015-03-06 15:25
モデル検査を用いたユースケースモデルに基づくソースコード検証 ~ ASP.NETアプリケーションを事例として ~ ○青木善貴(芝浦工大)・小形真平(信州大)・谷沢智史(ボイスリサーチ)・松浦佐江子(芝浦工大) KBSE2014-64 |
抄録 |
(和) |
モデル検査はシステムの振る舞いを検証するためには有効な技術である.我々はモデル検査技術を利用して仕様書とソースコードの振る舞いの不一致を発見する手法を提案してきたが,非機能要件に関する性質についてはシステムの状態の遷移が捉えにくく,検査モデルに表すことが難しいため適用が困難であった.ただし、セキュリティに関しては,機密性(confidentiality)のアクセス制御のようなシステムの振舞いに関係する部分については適用可能と考えられる.本論文では業務系ソフトウェアを対象にCommon Criteria によるセキュリティ要求の検証を目標として,大学で実稼動する授業支援ASP.NET アプリケーションを事例にモデル検査技術によるソースコード検証を行いその有効性について考察する. |
(英) |
Model checking is an effective technique in order to verify the behavior of the system. We have proposed a method to find the
discrepancy between the behavior of the source code and the pecifications by using model checking technology. Transition of the state of the system is elusive for properties related to non-functional requirements.
Its application for it is difficult to represent the test model for itwas difficult. However, for security, such as access control, I considered to be applicable to the portion related to the behavior of the system.
This paper was aimed at verification of security request by the Common Criteria to target the business system software.
We have to case the tuition support ASP.NET application that production at the university.
And we make the source code verification by model checking technology, I consider its validity. |
キーワード |
(和) |
モデル検査 / 不具合 / UPPAAL / / / / / |
(英) |
Model Checking / Defect / UPPAAL / / / / / |
文献情報 |
信学技報, vol. 114, no. 501, KBSE2014-64, pp. 71-76, 2015年3月. |
資料番号 |
KBSE2014-64 |
発行日 |
2015-02-26 (KBSE) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
KBSE2014-64 |