Realizability Decision and Program Synthesis for Reactive System Specification described by Temporal Logic

时态逻辑描述的反应式系统规范的可实现性决策和程序综合

• 批准号: 25330008
• 负责人: YOSHIURA Noriaki
• 金额: $ 3.08万
• 依托单位: Saitama University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2013
• 资助国家: 日本
• 起止时间: 2013-04-01 至 2017-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25330008/
• 关键词: 時間論理; モデルチェッキング; 実現可能性; リアクティブシステム; 適切さの論理; 仕様記述; プログラム化可能性; 仕様検証

项目成果

Extracting Environmental Constraints in Reactive System Specifications

提取反应式系统规范中的环境约束

• 发表时间: 2015
• 作者: Harumichi Nishimura;Yuichi Fukaya and Noriaki Yoshiura
• 通讯作者: Yuichi Fukaya and Noriaki Yoshiura

分解証明法を利用したリアクティブシステム仕様の強充足可能性判定器の提案

使用分解证明方法提出反应式系统规范的强可满足性确定器

• 发表时间: 2015
• 作者: Nakajima T;Fujita H;Aratani S;Yagishita N;中村 風太，吉浦 紀晃
• 通讯作者: 中村 風太，吉浦 紀晃

Verification of System Requirements

系统要求验证

• 发表时间: 2014
• 作者: Kunihiko Hiraishi;Koichi Kobayashi;Sunseong Choe;Naoshi Uchihira;Noriaki Yoshiura
• 通讯作者: Noriaki Yoshiura

Construction and Verificationof Mobile Ad Hoc Network Protocols, In Proceedings of 5th International Symposium on Cyberspace Safety and Security, Lecture Notes in Computer Science,

移动自组织网络协议的构建和验证，第五届网络空间安全国际研讨会论文集，计算机科学讲义，

• 发表时间: 2013
• 作者: Kunihiko Hiraishi;Koichi Kobayashi;Sunseong Choe;Naoshi Uchihira;Noriaki Yoshiura;Tetsuo Ida and Fadoua Ghourabi;Harumichi Nishimura;Natsuki Kimura and Noriaki Yoshiura
• 通讯作者: Natsuki Kimura and Noriaki Yoshiura

Computational Verification of Network Programs for Several OpenFlow Switches in Coq

Coq 中几种 OpenFlow 交换机的网络程序的计算验证

• 发表时间: 2016
• 期刊: Lecture Notes in Computer Science
• 作者: Hiroaki Date;Noriaki Yoshiura
• 通讯作者: Noriaki Yoshiura