モデル検査を用いたユースケースモデルに基づくソースコード検証 : ASP.NETアプリケーションを事例として (知能ソフトウェア工学)  [in Japanese] Verifying Source Code with a Use Case Model using Model Checking : A Case of an ASP.NET Application  [in Japanese]

Search this Article

Author(s)

Abstract

モデル検査はシステムの振る舞いを検証するためには有効な技術である.我々はモデル検査技術を利用して仕様書とソースコードの振る舞いの不一致を発見する手法を提案してきたが,非機能要件に関する性質についてはシステムの状態の遷移が捉えにくく,検査モデルに表すことが難しいため適用が困難であった.ただし、セキュリティに関しては,機密性(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 specifications 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 it was 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.

Journal

  • Technical report of IEICE. KBSE

    Technical report of IEICE. KBSE 114(501), 71-76, 2015-03-05

    The Institute of Electronics, Information and Communication Engineers

Codes

  • NII Article ID (NAID)
    110010021528
  • NII NACSIS-CAT ID (NCID)
    AN10386841
  • Text Lang
    JPN
  • ISSN
    0913-5685
  • NDL Article ID
    026329866
  • NDL Call No.
    Z16-940
  • Data Source
    NDL  NII-ELS 
Page Top