A study on a reliable automatic verification tool for concurrent systems

一种可靠的并发系统自动验证工具的研究

基本信息

项目摘要

This work aims at developing tools which analyze concurrent systems automatically like model-checkers and symbolically like theorem-provers, in order to support designs of the systems. Then, we have studied on such analysis-tools from two points of views : (1) automatizing proofs in theorem-provers and (2) introducing symbolic computation to model-checkers. In the former (1), we showed that proofs in CSP-Prover, which is a theorem-prover for a concurrency theory called CSP, can be automatized by implementing a model-checking algorithm to CSP-Prover. In the latter (2), we presented a method for automatically analyzing the whole behaviors from structures of concurrent systems and behaviors of component-processes by symbolic computation, and we implemented the analysis-method in a prototype-tool called CONPASU. For example, CONPASU can automatically generate symbolic-labeled transition graphs, which are useful for understanding the behaviors, from concurrent systems with infinite-states.
这项工作的目的是开发工具,分析并发系统自动像模型检查器和象征性的定理证明器,以支持系统的设计。然后,我们从两个角度对这类分析工具进行了研究:(1)在定理证明器中实现自动化证明;(2)在模型检查器中引入符号计算。在前一个(1)中,我们证明了CSP-Prover中的证明,这是一个称为CSP的并发理论的定理证明器,可以通过对CSP-Prover实现模型检查算法来自动化。在后者(2)中,我们提出了一种通过符号计算自动分析并发系统结构和组件进程行为的方法,并在一个原型工具CONPASU中实现了该分析方法。例如,CONPASU可以自动生成符号标记的转移图,这是有用的理解的行为,从并发系统的无限状态。

项目成果

期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
CONPASU-tool : A Concurrent Process Analysis Support Tool based on Symbolic Computation
CONPASU-tool :基于符号计算的并发过程分析支持工具
  • DOI:
  • 发表时间:
    2011
  • 期刊:
  • 影响因子:
    0
  • 作者:
    宗崎良太;田尻達郎;田中桜;木下義晶;古賀友紀;住江愛子;松崎彰信;原寿郎;田口智章;Zhi-Zhong Chen;山田貴志;磯部祥尚
  • 通讯作者:
    磯部祥尚
プロセス代数の基本と関連ツールの紹介
过程代数基础知识和相关工具简介
  • DOI:
  • 发表时间:
    2010
  • 期刊:
  • 影响因子:
    0
  • 作者:
    田尻達郎;他;Y.Kawano;磯部祥尚
  • 通讯作者:
    磯部祥尚
CONPASUのホームページ
康帕苏主页
  • DOI:
  • 发表时间:
  • 期刊:
  • 影响因子:
    0
  • 作者:
  • 通讯作者:
並行システムを解析するための逐次化と状態削減機能の実装 ~仕様の自動生成を目指して~
实现用于分析并行系统的串行化和状态缩减功能 - 旨在自动生成规格 -
  • DOI:
  • 发表时间:
    2010
  • 期刊:
  • 影响因子:
    0
  • 作者:
    檜山桂子;Arfin M;麓祥一;谷本圭司;檜山英三;西山正彦;M.Nakanishi;磯部祥尚
  • 通讯作者:
    磯部祥尚
プロセス代数に基づく並行システムの動作解析のための逐次化ツール
基于过程代数的并发系统行为分析的序列化工具
  • DOI:
  • 发表时间:
    2010
  • 期刊:
  • 影响因子:
    0
  • 作者:
    吉田浩之;高藤大介;田岡智志;渡邉敏正;D.Yokomine;磯部祥尚
  • 通讯作者:
    磯部祥尚
{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

ISOBE Yoshinao其他文献

ISOBE Yoshinao的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

相似海外基金

プロセス代数の応用に関する研究
过程代数应用研究
  • 批准号:
    05750326
  • 财政年份:
    1993
  • 资助金额:
    $ 2.25万
  • 项目类别:
    Grant-in-Aid for Encouragement of Young Scientists (A)
プロセス代数によるソフトウェア設計過程の形式化の研究
基于过程代数的软件设计过程形式化研究
  • 批准号:
    02650260
  • 财政年份:
    1990
  • 资助金额:
    $ 2.25万
  • 项目类别:
    Grant-in-Aid for General Scientific Research (C)
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了