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

Research on Specification and Verification of real-time software

Research Project

Project/Area Number 07680341
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionTokyo Institute of Technology

Principal Investigator

YONEZAKI Naoki  Tokyo Institute of Technology Graduate School of Information Science and Technology, Professor, 大学院・情報理工学研究科, 教授 (00126286)

Co-Investigator(Kenkyū-buntansha) TOMOISHI Masahiko  Tokyo Institute of Technology Graduate School of Information Science and Technol, 大学院・情報理工学研究科, 助手 (60262284)
Project Period (FY) 1995 – 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥2,300,000 (Direct Cost: ¥2,300,000)
Fiscal Year 1997: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 1996: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 1995: ¥700,000 (Direct Cost: ¥700,000)
KeywordsReal-time Software / Secification / Verification / Temporal Logic / Real-time Logic / Linear Logic / Relevant Logic
Research Abstract

It became crucial issue to build correct software with real time feature for safe critical systems e.g.embedded software in control systems. In order to make these software safer and securer, we need a new software construction method based on verification technique. In this research project we had the following results.
1) Proof systems of temporal logic for various time domains
First we developed connection calculus for temporal logic with discrete time domain. To prove the validity of a formula in discrete frames, we have to check the unsatisfiability for infinite frames. This means that we need substituion for infinite length of modal operators in connection calculus. In our approach we allows self substitution for modal operators so that we can solve the problem.
Then next we studied axiomatic systems for a temporal logic with real number timed domain. We showed that it is neither possible to construct complete axiomatic system nor to give decision procedure for the validity of a formula. We restricted it to rational domain where the number of the charge of state is bounded, as a result we had decidable logic.
2) Various aspects of software verification
2-1) Differential verification method for temporal specification
We developed new tableau method for differential verification, where the verification result for the previous specification is reused with the difference between a new specification and the previous one.
2-2) Level of realizabilities of a specification and its decision procedure
We defined several concepts approaching realizability. The classification of specifications based on these concepts gives us useful information for making a specification realizable. We gave the decision procedure for the membership of the classes and also we had an idea to identify a set of the parts of the specification which is the cause of un-realizability.

Report

(4 results)
  • 1997 Annual Research Report   Final Research Report Summary
  • 1996 Annual Research Report
  • 1995 Annual Research Report
  • Research Products

    (36 results)

All Other

All Publications (36 results)

  • [Publications] 森 亮靖、友石 正彦、米崎 直樹: "時相論理によるリアクティブシステム仕様の実現可能性に関する分類" 日本ソフトウェア科学会論文誌. (採録決定). (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Yoshiaki Minamisawa, Masahiko Tomoishi and Naoki Yonezaki: "A New semantics for Linear Logic and its Completeness" Information modeling and knowledge bases. VIII. 155-166 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Shigeki Hagihara and Naoki Yonezaki: "A Connection based proof method for Modal logic restricted to Discrete frames" Poster Session Abstracts,Fifteenth International Joint Conference on Artificial Intelligence. 43-43 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 友石 正彦、米崎 直樹: "合成可能な時間論理タブロ-の構成法" 電子情報通信学会技術研究報告97. 390. 17-22 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 須藤 忠祐、米崎 直樹: "実時間論理RTL^Qの公理化に関する研究" 日本ソフトウェア科学会第14回大会論文集. 381-384 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 南澤 吉昭、米崎 直樹: "線形論理CLL_eのモデルを用いた意味論" 情報処理学会第55回全国大会論文集(2). 547-548 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Ryosei Mori, Masahiko Tomoishi and Naoki Yonezaki: "Classification of Reactive System Specifications in Temporal Logic" Journal of Japan Society for Software Science and Technology. (to be appeared). (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Yoshiaki Minamisawa, Masahiko Tomoishi and Naoki Yonezaki: "A New semantics for Linear Logic and its Completeness" Information modeling and knowledge bases. VIII. 155-166 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Shigeki Hagihara and Naoki Yonezaki: "A Connection based proof method for Modal logic restricted to Discrete frames" Poster Session Abstracts, Fifteenth International Joint Conference on Artificial Intelligence. 43-43 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Masahiko Tomoishi and Naoki Yonezaki: "Consistency Checking on Composite Specification by Tableau Composition" ICICE Technical Report 97. 390. 17-22 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Tadasuke Sudo and Naoki Yonezaki: "Axiomatization for real-time logic RTL^Q" 14th Conference Proceedings Japan Society for Software Science and Technology. 381-384 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Yoshiaki Minamisawa and Naoki Yonezaki: "Model based semantics for linear logic CLLe" 55th Conference Proceedings Information Processing Society of Japan. 547-548 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Noriaki Yoshiura and Naoki Yonezaki: "Relevant Inference and Reliability Dependent on Implication" Information modelling and knowledge bases. VII. 154-172 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Miyoko Kawamura and Naoki Yonezaki: "Non Clausal Linear Resolution for Propositional Linear Logic" Information Modelling and Knowledge Bases. VI. 215-229 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Yonezaki Minamisawa and Naoki Yonezaki: "Proof Strategies in Linear logic (CLL_e) on Non Clausal Linear Resolution (NCLR)" 50th Conference Proceedings Information Processing Society of Japan. 3-4. (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Shigeki Hagihara and Naoki Yonezaki: "Improving efficiency of modal theorem prover by informations from the failure of the past proof process" 12th Conference Proceedings Japan Society for Software Science and Technology. 105-108 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Naoki Yonezaki, Yasuto Suzuki and Tadasuke Sudo: "Real-time Logic RTL" 12th Conference Proceedings Japan Society for Software Science and Technology. 137-140 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Kazuhide Miki, Masahiko Tomoishi and Naoki Yonezaki: "Stepwise verification of reactive system specifications" 12th Conference Proceedings Japan Society for Software Science and Technology. 141-144 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 森亮靖、友石正彦、米崎直樹: "時相論理によるリアクティブシステム仕様の実現可能性に関する分類" 日本ソフトウェア科学会論文誌(採録決定). (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Yoshiaki Minamisawa, Masahiko Tomoishi and Naoki Yonezaki: "A New semantics for Linear Logic and its Completeness" Information modeling and knowledge bases. VIII. 155-166 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Shigeki Hagihara and Naoki Yonezaki: "A Connection based proof method for Modal logic restricted to Discrete frames" Poster Session Abstracts,Fifteenth International Joint Conference on Artificial Intelligence. 43-43 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 友石正彦、米崎直樹: "合成可能な時間論理タブロ-の構成法" 電子情報通信学会技術研究報告97. 390. 17-22 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 須藤忠祐、米崎直樹: "実時間論理RTL^Qの公理化に関する研究" 日本ソフトウェア科学会第14回大会論文集. 381-384 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 南澤吉昭、米崎直樹: "線形論理CLL_eのモデルを用いた意味論" 情報処理学会第55回全国大会論文集(2). 547-548 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Noriaki Yoshiura,Naoki Yonezaki: "Relevant Inference and Reliability Dependent on Implication" Information modelling and knowledge bases. VII. 154-172 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Yoshiaki Minamisawa,Masahiko Tomoishi,Naoki Yonezaki: "Semantics for Linear Logic and its Completeness" The 6th European-Japanese Conference on Information Modelling and Knowledge Bases. (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 吉浦紀晃、米崎直樹: "知識推論のための適切さの論理" 日本ソフトウェア科学会第13回大会論文集. 437-440 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 南澤吉昭、米崎直樹: "モデルを用いた線形論理の意味論" 日本ソフトウェア科学会第13回大会論文集. 425-428 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 伊藤裕、友石正彦、米崎直樹: "マルチエージェントプランニングにおけるサブゴールの設定" 第5回マルチエージェントと協調計算ワークショップオンライン論文集http://www.csl.sony.co:jp/personal/nagao/Macc95. (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 渡辺治、米崎直樹: "計算論入門" 日本評論社, 211 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 米崎直樹,鈴木康人,須藤忠祐: "実時間論理RTL" 日本ソフトウェア科学会第12回大会論文集. 137-140 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] Miyoko Kawamura,Naoki Yonezaki: "Non Clausal Linear Resolution for Propositional Linear Logic" Information Modelling and Knowledge Bases. VI. 215-229 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 三木一秀,友石正彦、米崎直樹: "リアクティブシステム仕様の段階的記述プロセスに対応した検証法" 日本ソフトウェア科学会第12回大会論文集. 141-144 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 森亮靖、米崎直樹: "実時間論理によるリアクティブシステム仕様の外部イベント制約式" 日本ソフトウェア科学会第12回大会論文集. 177-180 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 南沢吉昭、米崎直樹: "導出法による線形論理CLLeの自動証明戦略" 情報処理学会第50回全国大会講演論文集. 3-3-3-4 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 萩原茂樹、米崎直樹: "様相論理証明における失敗情報の利用" 日本ソフトウェア科学会第12回大会論文集. 105-108 (1995)

    • Related Report
      1995 Annual Research Report

URL: 

Published: 1995-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi