Formal Verification System by using Hardware Compiler Fusioning of Theorem Prover and Model Checker on the Grid Environment
Formal Verification System by using Hardware Compiler Fusioning of Theorem Prover and Model Checker on the Grid Environment
批准号:
23500174
负责人:
WASAKI Katsumi
金额:
$3.33万
依托单位:
依托单位国家:
日本
项目类别:
Grant-in-Aid for Scientific Research (C)
财政年份:
2011
资助国家:
日本
项目状态:
已结题
起止时间:
2011 至 2013
中文摘要
一个对网格计算环境实现的定理证明器,融合了输出硬件编译器目标实现的各种代码。建立一个与上游下游功能高度一致的形式化验证系统,从而大大提高异步并联电路系统的验证能力。在功能语言系统上描述了目标电路的配置信息。作为语言系统的编译输出,我们可以得到目标实现代码和对证明检查器的证明类型。基于异步逻辑门元件的4值逻辑双线模型,用消息传递并行计算机对目标电路进行了建模。最后,校验器利用电路连接校验其正确性。
英文摘要
A theorem prover that implements to the grid computing environment fuses the output hardware compiler target implementation various code. To build a formal verification system which is consistent high to function downstream from the upstream, thereby dramatically improving the ability for verification of asynchronous parallel circuit system. The configuration informations of the target circuit has been described on the functional language system. As compiler output of the language system, we can get the target implementation code and the type of proof to proof checker. The target circuit has been modeled by message passing parallel computer based on the 4-valued logic two-wire model of asynchronous logic gate element. Finally, proof checker can verify its correctness proof by using of the circuit connection.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
自由選択ネットの活性・安全性判定解析アルゴリズム改善と援用ツールへの実装
改进用于确定自由选择网的活性和安全性的分析算法以及在支持工具中的实现
DOI:
--
发表时间:
2012
期刊:
影响因子:
--
作者:
[井出和人, 和崎克己]
通讯作者:
和崎克己
Content Development for Distance Education in Advanced University Mathematics Using Mizar
使用 Mizar 进行高等大学数学远程教育内容开发
DOI:
--
发表时间:
2013
期刊:
Proceedings of the 2013 International Conference on e-Learning, e-Business, Enterprise Information Systems, and e-Government (EEE'13)
影响因子:
--
作者:
[Takaya IDO, Hiroyuki OKAZAKI, Hiroshi YAMAZAKI, Pauline Naomi KAWAMOTO, Katsumi WASAKI, Yasunari SHIDAMA]
通讯作者:
Yasunari SHIDAMA
Morphology for Image Processing. Part I
图像处理的形态学。
DOI:
10.2478/v10037-012-0008-y
发表时间:
2012
期刊:
Formalized Mathematics
影响因子:
0.3
作者:
[Hiroshi Yamazaki, Czeslaw Bylinski, Katsumi Wasaki]
通讯作者:
Katsumi Wasaki
UML シーケンス図の構造記述から線形時相論理式への自動変換手法
UML序列图结构描述到线性时序逻辑公式的自动转换方法
DOI:
--
发表时间:
2011
期刊:
影响因子:
--
作者:
[宮本直樹, 和崎克己]
通讯作者:
和崎克己
Automatic Generation of SPIN Model Checking Code from UML Activity Diagram and Its Application to Web Application Design
UML活动图自动生成SPIN模型检查代码及其在Web应用设计中的应用
DOI:
--
发表时间:
2011
期刊:
Proceedings of the 7th International Conference on Digital Content, Multimedia Technology and its Applications (IDCTA2011)
影响因子:
--
作者:
[Yutaka YAMADA, Katsumi WASAKI]
通讯作者:
Katsumi WASAKI
共 36 条
Design verification method of massively parallel arithmetic unit combined using a functional language and the Grid computing system
-
批准号:20500130
-
项目类别:Grant-in-Aid for Scientific Research (C)
-
资助金额:$2.91万
-
财政年份:2008
-
负责人:WASAKI Katsumi
-
依托单位:
海外基金