大規模システムソフトウェアのモデル検査器の設計と実装

IPSJ

Bibliographic Information

Other Title
  • Design and Implementation of a Model Checker for Large-scale System Software

Search this article

Abstract

本発表では，デペンダブル組み込みOSに対する静的プログラム解析の一部として開発中のモデル検査器の概要を報告する．一般に述語抽象をベースにするモデル検査方式が有望であるが，適用規模がOS等のシステムソフトウェアに及ばない．そこで規模の大きなソフトウェアにモデル検査器を適用するため，検証項目はアサーション等の基本な性質に限るが，効率や規模を重視するモデル検査器の開発を行っている．処理規模の拡大にはクラスタ計算機による分散処理を念頭に，並列化が可能な構成を選択する．また，抽象状態の遷移計算には近年性能向上の著しいSMTソルバを利用できる方式を選択する．モデル検査器に与えるアサーションの記述には，デペンダブル組み込みOSで提案されている記述方法を利用する．P-Busと呼ばれるOS内部のレイヤ間で抽象化インタフェースが定義されており，それに対するアサーション記述が提案されている．その記述に対してモデル検査を行う．

A model checker is under development as one of the static program verifiers for the forthcoming Dependable Embedded Operating System. Our model checker is designed with priority for scalability, because model checking based on predicate abstraction is promising, but it is not yet applicable to large system software like operating systems. A trade-off is taken not for verifiable properties, but for efficiency and scalability, and verifiable properties are currently simple assertions. Our model checker is designed for parallel processing with cluster computers, and utility of recently advanced SMT solvers. Assertions are described based on the P-Bus interface, which is a proposed abstract interface internal to the kernel that cleanly separates functionalities in operating systems. Our model checker works on the properties attached to the interface.

Journal

Keywords

Details

Report a problem

Back to top