組込みアセンブリプログラムのモデル構築によるモデル検査

IPSJ

Bibliographic Information

Other Title
  • Model Checking by Modeling for Embedded Assembly Programs

Abstract

組込みシステムは，広く利用されており，徐々に複雑化している．複雑化している組込みシステムを安全に運用するためには，システムの安全性を保証することが重要である．複雑なシステムに対する検証手法として，モデル検査が有効である．我々は，組込みシステムのアセンブリプログラムの全振る舞いから，モデルを自動的に生成するツールを開発した．ツールによって生成されたモデルを，モデル検査器に入力することで，システムの安全性を保証する．また，状態爆発に対応するため，Delayed NonDeterminism をベースとした，不定値と呼ぶ抽象化手法を導入する．

Embedded systems have been widely used. In addition, embedded systems have been gradually complicated. It is important to ensure the safety for complex systems. Model checking is effective to ensure the safety for complex systems. We have developed Behavior Extractor to automatically model all behaviors of embedded assembly programs. Then, we ensure the safety by model checkers. In addition, we have introduced the undefined value to reduce the number of states. The undefined value is based on the Delayed NonDeterminism.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

  • CRID
    1050292572119752448
  • NII Article ID
    170000087146
  • Web Site
    http://id.nii.ac.jp/1001/00106380/
  • Text Lang
    ja
  • Article Type
    conference paper
  • Data Source
    • IRDB
    • CiNii Articles
    • KAKEN

Report a problem

Back to top