| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 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 |
|
| 研究会情報 | |
| 研究会 | KBSE |
| 開催期間 | 2015-03-05 - 2015-03-06 |
| 開催地（和） | 電通大(調布, 東3号館) |
| 開催地（英） | The University of Electro-Communications |
| テーマ（和） | 一般 |
| テーマ（英） | Genaral session |
| 講演論文情報の詳細 | |
| 申込み研究会 | KBSE |
| 会議コード | 2015-03-KBSE |
| 本文の言語 | 日本語 |
| タイトル（和） | モデル検査を用いたユースケースモデルに基づくソースコード検証 |
| サブタイトル（和） | ASP.NETアプリケーションを事例として |
| タイトル（英） | Verifying Source Code with a Use Case Model using Model Checking |
| サブタイトル（英） | A Case of an ASP.NET Application |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | 不具合 / Defect |
| キーワード(3)（和/英） | UPPAAL / UPPAAL |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 青木 善貴 / Yoshitaka Aoki / アオキ ヨシタカ |
| 第1著者 所属（和/英） | 芝浦工業大学 (略称： 芝浦工大) Shibaura Institute of Technology (略称： Shinshu Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 小形 真平 / Shinpei Ogata / オガタ シンペイ |
| 第2著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 谷沢 智史 / Satoshi Yazawa / ヤザワ サトシ |
| 第3著者 所属（和/英） | 株式会社ボイスリサーチ (略称： ボイスリサーチ) Voice Research, Inc. (略称： VR) |
| 第4著者 氏名（和/英/ヨミ） | 松浦 佐江子 / Saeko Matsuura / マツウラ サエコ |
| 第4著者 所属（和/英） | 芝浦工業大学 (略称： 芝浦工大) Shibaura Institute of Technology (略称： SIT) |
| 講演者 | 第1著者 |
| 発表日時 | 2015-03-06 15:25:00 |
| 発表時間 | 45分 |
| 申込先研究会 | KBSE |
| 資料番号 | KBSE2014-64 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | no.501 |
| ページ範囲 | pp.71-76 |
| ページ数 | 6 |
| 発行日 | 2015-02-26 (KBSE) |
[研究会発表申込システムのトップページに戻る]