近年,組込みシステムの分野では,システムが大規模化・複雑化してきている.このため,検証の重要性が増すと同時に,検証の工数が増加してきており,検証の効率化が課題となっている.
検証手法には,動的検証と静的検証があるが,組込みシステム開発の分野では,第3の検証手法としてアサーションベース検証が注目されている.アサーションベース検証は,プログラムが満たすべき性質の宣言 (アサーション) にプログラムが違反しないかどうかをチェックする検証手法である.アサーションベース検証は,検証の効率化を図ることができるという利点がある.
一方,組込みシステム開発における設計では,実行可能UMLが用いられ始めている.実行可能UMLではUMLダイアグラムを用いて作成したモデルを実行することができ,モデルの検証が可能である.今後は実行可能UMLを用いた設計が一般的になると言われている.
したがって,今後は実行可能UMLにおける検証の効率化が課題となると考えられる.検証の効率化を図る方法としては,誤り箇所を特定しやすくなるという理由で,アサーションベース検証を行う方法がある.実行可能UMLにおけるアサーションベース検証に関する研究としては,アサーションベースの静的検証があるが,アサーションベースの動的検証も必要だと考えられる.その理由は,アサーションベースの動的検証には,一般的な動的検証と同時に行うことで,一般的な動的検証で不具合が発見された場合に誤りの原因となる箇所を特定しやすくするという効果があり,一般的な動的検証の効率化を図れるからである.
そこで,本研究では,実行可能UMLにおけるアサーションベースの動的検証の実装に取り組んだ.具体的には,実行可能UMLにおけるアサーションの記述方式とチェック方法を定め,アサーションのチェックが正しく行えることを実験により確認した.