• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2016 Fiscal Year Research-status Report

次世代車載オペレーティングシステムにおける先進機能の形式検証に関する研究

Research Project

Project/Area Number 15K00094
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

青木 利晃  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)

Project Period (FY) 2015-04-01 – 2018-03-31
Keywords車載システム / 形式仕様 / 形式検証
Outline of Annual Research Achievements

平成28年度は,1.AUTOSAR OSの保護機能の形式検証,および,2.マルチコア機能の形式検証を実施した.
1.AUTOSAR OSの保護機能の形式検証:平成27年度は,Event-Bを用いてAUTOSAR OSの保護機能を形式的に記述した.Event-Bでは,証明課題(proof obligation)と呼ばれる証明しなければならない事実を自動生成する.この証明課題はEvent-BのツールRODINの証明器を用いて対話的に証明を行う.平成27年度において,証明課題の証明を試みたが,それら全部は証明することができなかった.そこで,今年度も,証明を引き続き行ったが,RODINの証明器の信頼性や機能の問題により,それらすべてについて証明を行うことが困難になった.そこで,AlloyとAlloy Analyzerを用いて自動的に証明を行うことにした.Alloyは集合や関係に基づいた仕様を記述するための言語であり,Alloy Analyzerはその検証ツールである.これらは,Event-Bで記述したものと同等のものを扱うことができる.今年度はAlloyで保護機能を記述し,Alloy Analyzerを用いて自動検証を実施することができた.
2.マルチコア機能の形式検証:マルチコアプロセッサ上で動作するプログラムでは,複数のコア間でハードウェアレベルの複雑な動作が実行されるため,検証対象のプログラムだけでなく,ハードウェアの振る舞いを含めて検証する必要がある.そこで,平成27年度に,ハードウェアの振る舞いの分析と形式化を行った.そして,今年度は,その分析と形式化に基づいたプログラムの検証法を提案した.この手法では,自動定理証明器(SMTソルバ)を用いて検証を行う.また,提案手法を,Linuxカーネルにおけるスピンロックのプログラムに適用し,実際に検証を行うことができた.

Current Status of Research Progress
Current Status of Research Progress

1: Research has progressed more than it was originally planned.

Reason

今年度は,1.保護機能の形式検証と2.マルチコア機能の形式検証を行った.1については,当初の予定どおり,形式検証を実施することができたため,おおむね予定どおりに進展していると考えている.2については,以下の理由から,当初の計画以上に進展していると考えている.当初の計画では,今年度は,AUTOSAR OSの実装の分析を行う予定であった.しかしながら,その大半は,昨年度実施することができ,今年度は,マルチコア機能の形式検証の仕組みについて提案することができた.この手法では,自動定理証明器(SMTソルバ)を用いて,自動的に検証を行うことができる.当初は,定理証明による対話的な証明を想定していたが,自動的な検証が可能になったことは,大きな成果である.さらに,提案手法により,SPARC用のLinuxカーネルにおけるスピンロックプログラムの検証に成功し,また,すでにバグがあることがわかっているプログラム(このプログラムは当該分野のベンチマークのように使われている)の検証を実施し,バグを検出することにも成功した.すでに,実践的に使える手法を提案することができたのである.これらのことから,当初の計画以上に進展していると判断した.

Strategy for Future Research Activity

平成29年度は,実際の車載OSを対象として,1.保護機能の検証,および,2.マルチコア機能の検証を実施し,提案手法の評価を行う.
1.保護機能の検証:平成28年度に,Alloyによる保護機能の形式仕様を作成し,その正しさの検証を実施した.平成29年度は,この形式仕様に基づいて,車載OSの検証を行う手法を提案する.この検証では,形式仕様から網羅的なテストケースおよび期待値を自動生成し,それらを用いたテストを実施することを考えている.ここで,保護機能の仕様は,静的な制約として規定されており,形式仕様も同様である.テストケースを自動生成するためには,車載OSを実行する手順を規定する情報が必要である.そこで,テストする手順を規定するモデルを追加し,形式仕様からテストケースを自動生成する手法を提案する予定である.
2.マルチコア機能の検証
平成28年度に,すでに,SPARC用のLinuxカーネルの検証には成功している.一方,対象とする車載OSはARMプロセッサを用いているが,その挙動はSPARCとは異なる.SPARCはTSOと呼ばれるメモリモデルを採用しているが,ARMプロセッサは,それとは異なるメモリモデルを採用しているためである.そこで,提案手法をARMプロセッサが扱えるように拡張し,検証を実施する.

  • Research Products

    (5 results)

All 2016

All Journal Article (1 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 1 results,  Open Access: 1 results) Presentation (4 results) (of which Int'l Joint Research: 2 results)

  • [Journal Article] A spiral process of formalization and verification: A case study on verification of the scheduling mechanism of OSEK/VDX2016

    • Author(s)
      Min Zhang, Toshiaki Aoki, Yueying He
    • Journal Title

      Journal of Information Security and Applications

      Volume: 31 Pages: 41-53

    • DOI

      10.1016/j.jisa.2016.05.002

    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Presentation] Simulinkモデルに対するテストスイート自動生成2016

    • Author(s)
      冨田尭, 石井大輔,青木利晃
    • Organizer
      第14回ディペンダブルシステムワークショップ
    • Place of Presentation
      花びしホテル(北海道函館市)
    • Year and Date
      2016-12-14 – 2016-12-15
  • [Presentation] Java Pathfinder における弱公平性条件の実装2016

    • Author(s)
      太田十字光, 田辺良則, 青木利晃
    • Organizer
      日本ソフトウェア科学会第33回全国大会
    • Place of Presentation
      東北大学片平キャンパス(宮城県仙台市)
    • Year and Date
      2016-09-06 – 2016-09-09
  • [Presentation] Verifying OSEK/VDX OS Design using Its Formal Specification2016

    • Author(s)
      Dieu Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
    • Organizer
      International Symposium on Theoretical Aspects of Software Engineering
    • Place of Presentation
      Shanghai, China
    • Year and Date
      2016-07-17 – 2016-07-19
    • Int'l Joint Research
  • [Presentation] Dissolution of the Gap between Safety Requirements Written in a Natural Language and Formal Notations2016

    • Author(s)
      Masahiro Matsubara, Fumio Narisawa, Atsuhiro Ohno, Toshiaki Aoki, Yuki Chiba
    • Organizer
      SAE 2016 World Congress and Exhibition
    • Place of Presentation
      Detroit, USA
    • Year and Date
      2016-04-12 – 2016-04-14
    • Int'l Joint Research

URL: 

Published: 2018-01-16  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi