Extracting information for correction of flaws from embedded system specification of practical scale by formal method

采用形式化方法从实用规模的嵌入式系统规范中提取缺陷修正信息

• 批准号: 24500032
• 负责人: HAGIHARA Shigeki
• 金额: $ 3万
• 依托单位: Tokyo Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2012
• 资助国家: 日本
• 起止时间: 2012-04-01 至 2015-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24500032/
• 关键词: 形式手法; 組み込みシステム仕様; 修正情報抽出; 時間論理; オートマトン; 極小充足不能集合; 組込みシステム仕様

项目成果

Complexity of Strong Satisfiability Problems for Reactive System Specifications

• DOI: 10.1587/transinf.e96.d.2187
• 发表时间: 2013-10
• 期刊: IEICE Trans. Inf. Syst.
• 作者: Masaya Shimakawa;Shigeki Hagihara;N. Yonezaki

Developing Embedded Systems from Formal Specifications Written in Temporal Logic

根据时态逻辑编写的形式规范开发嵌入式系统

• DOI: 10.1007/978-1-4614-3363-7_13
• 发表时间: 2013
• 期刊: Proceedings of the Third International Conference on Trends in Information, Telecommunication and Computing, Lecture Notes in Electrical Engineering
• 作者: Shigeki Hagihara;Takahiro Arai;Masaya Shimakawa;Naoki Yonezaki
• 通讯作者: Naoki Yonezaki

Minimal strongly unsatisfiable subsets of reactive system specifications

反应式系统规范的最小强烈不可满足子集

• 发表时间: 2014
• 作者: Shigeki Hagihara;Naoki Egawa;Masaya Shimakawa;Naoki Yonezaki
• 通讯作者: Naoki Yonezaki

SAT-Based Bounded Strong Satisfiability Checking of Reactive System Specifications

基于 SAT 的反应式系统规范有界强可满足性检查

• DOI: 10.1007/978-3-642-36818-9_7
• 发表时间: 2013
• 期刊: Information and Communicatiaon Technology, Lecture Notes in Computer Science
• 作者: Masaya Shimakawa;Shigeki Hagihara;Naoki Yonezaki
• 通讯作者: Naoki Yonezaki

An Efficient Implementation of Satisfiability Checking for LTL with Mean-Payoff Constraints

具有平均收益约束的零担可满足性检查的有效实现

• 发表时间: 2014
• 作者: Takashi Tomita;Takahito Kimura;Shigeki Hagihara and Naoki Yonezaki
• 通讯作者: Shigeki Hagihara and Naoki Yonezaki