• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2018 年度 実績報告書

ソフトウェア開発の高信頼アジャイル形式工学手法に関する研究

研究課題

研究課題/領域番号 26240008
研究機関法政大学

研究代表者

劉 少英  法政大学, 情報科学部, 教授 (90264960)

研究分担者 児玉 靖司  法政大学, 経営学部, 教授 (30266910)
緒方 和博  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
研究期間 (年度) 2014-06-27 – 2019-03-31
キーワードアジャイル開発 / 形式工学手法 / 仕様アニメーション / テストに基づく形式検証 / モデル検査 / 形式仕様に基づくテスト / 形式仕様記述手法
研究実績の概要

本年度の研究では、次の活動に集中して努力してきた。
(1)自動テストに基づくアルゴリズム関数定理の形式検証理論と技術の確立。アジャイル形式工学手法を実現するためには、形式仕様に基づくプログラムの自動検証が不可欠である。従来のホーア論理によりプログラムの正しさの検証技術ではバグがあるプログラムに対応し難いし、自動化もほとんど不可能である。本研究では、形式仕様に基づく自動テスト技術とホーア論理を適切に統合して、プログラムの正しさを自動的に検証する理論と手法を確立した。但し、現在の手法では、基本データ型のみを使用するプログラムに限られており、複合データ型の対応には課題がまだ残っている。(2)形式仕様のシステムレベルの一致性を検証するために、形成された論理式のテストプロセスのアニメーション手法と支援ツールの開発。この中で、有効なテストデータの自動生成支援ツールと論理式のアニメーション支援ツールの研究が含まれている。(3)プロセス仕様のアニメーションのために、入出力を表すGUIの自動生成する支援ツールの開発。SOFL仕様記述言語の様々なデータ型を対応するプロセスの入出力のGUIを自動的に生成するプロトタイプが開発された。これによって形式仕様の分かりやすいアニメーションを実現できる。(4)モデル検査プロセスのアニメーション技術を確立、プロトコールの性質の形式検証に適用、その効果を調べた。(5)SOFL仕様記述言語に基づくアジャイル形式工学手法のフレームワークを確立、その中の各段階の技術の協力関係と役割を明らかにした。(6)研究成果を反映する多数の論文を作成し、ACM Transactions on Software Engineering MethodologyやIEEE Transactions on Software Engineeringなど論文誌と国際会議に投稿又は公表した。

現在までの達成度 (段落)

平成30年度が最終年度であるため、記入しない。

今後の研究の推進方策

平成30年度が最終年度であるため、記入しない。

  • 研究成果

    (19件)

すべて 2019 2018

すべて 雑誌論文 (15件) (うち国際共著 1件、 査読あり 14件、 オープンアクセス 1件) 学会発表 (3件) (うち国際学会 1件) 図書 (1件)

  • [雑誌論文] Software Construction Monitoring and Predicting for Human-Machine Pair Programming2019

    • 著者名/発表者名
      Shaoying Liu
    • 雑誌名

      Proceedings of 8th International Workshop on SOFL +MSVL 2018 for Reliability and Security

      巻: - ページ: 3-20

    • 査読あり
  • [雑誌論文] Verification of SysML Activity Diagrams using Hoare Logic and SOFL2019

    • 著者名/発表者名
      Yufei Yin, Shaoying Liu, Yixiang Chen
    • 雑誌名

      Proceedings of 8th International Workshop on SOFL +MSVL 2018 for Reliability and Security

      巻: - ページ: 71-88

  • [雑誌論文] A Divide & Conquer Approach to Liveness Model Checking under Fairness & Anti-fairness Assumptions2019

    • 著者名/発表者名
      Kazuhiro Ogata
    • 雑誌名

      Frontiers of Computer Science (FCS)

      巻: 13(1) ページ: 51-72

    • 査読あり
  • [雑誌論文] TBFV-SE: Testing-Based Formal Verification with Symbolic Execution2018

    • 著者名/発表者名
      Rong Wang, Shaoying Liu
    • 雑誌名

      proceedings of 2018 IEEE International Conference on Software Quality, Reliability and Security (QRS 2018)

      巻: - ページ: 59-66

    • DOI

      10.1109/QRS.2018.00019

    • 査読あり
  • [雑誌論文] Automated Visualization of Input / Output for Processes in SOFL Formal Specifications2018

    • 著者名/発表者名
      Yu Chen, Shaoying Liu
    • 雑誌名

      Proceedings of The 7th International Conference on Software Engineering and Applications (SEAS 2018)

      巻: - ページ: 33-48

    • 査読あり
  • [雑誌論文] TBFV-M: Testing Based Formal Verification for Sysml Activity Diagrams2018

    • 著者名/発表者名
      Yufei Yin, Shaoying Liu, Yixiang Chen
    • 雑誌名

      Proceedings of The 7th International Conference on Software Engineering and Applications (SEAS 2018)

      巻: - ページ: 49-68

    • 査読あり
  • [雑誌論文] autoC: an Efficient Translator for Model Checking Deterministic Scheduler based OSEK/VDX Applications2018

    • 著者名/発表者名
      Haitao Zhang, Zhuo Cheng, Guoqiang Li, Shaoying Liu
    • 雑誌名

      Science China Information Sciences

      巻: 61 ページ: 1-15

    • 査読あり / 国際共著
  • [雑誌論文] VALIDATION AND VERIFICATION OF SYSML ACTIVITY DIAGRAMS USING HOARE LOGIC2018

    • 著者名/発表者名
      Yufei Yin, Shaoying Liu, Yixiang Chen
    • 雑誌名

      International Journal of Software Engineering & Applications (IJSEA)

      巻: 9(4) ページ: 101-117

    • 査読あり
  • [雑誌論文] DESIGN AND IMPLEMENTATION OF AUTOMATED VISUALIZATION FOR INPUT / OUTPUT FOR PROCESSES IN SOFL FORMAL SPECIFICATIONS2018

    • 著者名/発表者名
      Yu Chen, Shaoying Liu
    • 雑誌名

      International Journal of Software Engineering & Applications (IJSEA)

      巻: 9(4) ページ: 139-157

    • 査読あり
  • [雑誌論文] Agile Formal Engineering Method for Software Productivity and Reliability2018

    • 著者名/発表者名
      Shaoying Liu
    • 雑誌名

      Proceedings of the 14th Central and Eastern European Software Engineering Conference Russia (CEE-SECR 2018)

      巻: - ページ: 64-69

    • DOI

      10.1145/3290621.3290634

    • 査読あり
  • [雑誌論文] Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores2018

    • 著者名/発表者名
      Adrian Riesco, Kazuhiro Ogata
    • 雑誌名

      ACM Transactions on Software Engineering and Methodology

      巻: 27(2) ページ: 6:1-6:32

    • 査読あり / オープンアクセス
  • [雑誌論文] Formal Analysis of a Security Protocol for e-Passports based on Rewrite Theory Specifications2018

    • 著者名/発表者名
      Manjukeshwar Reddy Mandadi, Varuneshwar Reddy Mandadi, Kazuhiro Ogata
    • 雑誌名

      Journal of Information Security and Applications (JISA)

      巻: 42 ページ: 71-86

    • 査読あり
  • [雑誌論文] Analysis of Some Variants of the Anderson Array-Based Queuing Mutual Exclusion Protocol with Model Checking and Graphical Animations2018

    • 著者名/発表者名
      Yati Phyo, Kazuhiro Ogata
    • 雑誌名

      Proceedings of the 5th International Conference on Dependable Systems and Their Applications

      巻: - ページ: 126-135

    • 査読あり
  • [雑誌論文] Model Checking of the Suzuki-Kasami Distributed Mutual Exclusion Algorithm with SPIN2018

    • 著者名/発表者名
      Shouki Sakamoto, Kazuhiro Ogata
    • 雑誌名

      Proceedings of the 5th International Conference on Dependable Systems and Their Applications

      巻: - ページ: 136-141

    • 査読あり
  • [雑誌論文] Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks2018

    • 著者名/発表者名
      Yati Phyo, Kazuhiro Ogata
    • 雑誌名

      Proceedings of the 25th Asia-Pacific Software Engineering Conference (APSEC 2018)

      巻: - ページ: -

    • 査読あり
  • [学会発表] An Efficient Approach for Verifying Automobile Distributed Application Systems on Timing Property2018

    • 著者名/発表者名
      Haitao Zhang, Guoqiang Li, Li Xiaohong, Zhuo Cheng, Jinyun Xue, Shaoying Liu
    • 学会等名
      International Conference on Software Engineering ( ICSE 2018 )
    • 国際学会
  • [学会発表] ソースコードからCDFDへの変換によるSOFL仕様記述の支援ツールの提案2018

    • 著者名/発表者名
      新城汐里、劉少英
    • 学会等名
      ソフトウェアシンポジウム2018 (ss2018)
  • [学会発表] SOFL形式仕様に基づくC#プログラムのテストツール2018

    • 著者名/発表者名
      網谷拓海、劉少英
    • 学会等名
      ソフトウェアシンポジウム2018 (ss2018)
  • [図書] Structured Object-Oriented Formal Language and Method - 8th International Workshop, SOFL+MSVL 20182019

    • 著者名/発表者名
      Zhenhua Duan and Shaoying Liu, Cong Tian, Fumiko Nagoya (eds)
    • 総ページ数
      197
    • 出版者
      Springer
    • ISBN
      978-3-030-13650-5

URL: 

公開日: 2019-12-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi