Automatic verification method for large scale embedded object-oriented design based on predicate abstraction

基于谓词抽象的大规模嵌入式面向对象设计自动验证方法

• 批准号: 19500025
• 负责人: YAMANE Satoshi
• 金额: $ 1.91万
• 依托单位: Kanazawa University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2007
• 资助国家: 日本
• 起止时间: 2007 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19500025/
• 关键词: 組込みシステム; 述語抽象化検証; オブジェクト指向; リアルタイムオブジェクト指向; 抽象化精錬検証; 構造とリアルタイム性の抽象化; 動的リアルタイムCEGAR; モデル検査; オブジェクトの生成消滅; 動的再構成組込みシステム; ハイブリッドオートマトン; 仕様記述言語; 検証; 述語抽象化洗練

リアルタイムオブジェクト指向言語を開発して、オブジェクトが生成消滅するシステムに対して、構造と時間の抽象化精錬で直接に検証できる、動的リアルタイムCEGARの開発と実装に取り組んだ。その結果、動的リアルタイムCEGARの実現により、オブジェクトの生成消滅といった構造の変化及びリアルタイム性を同時に抽象化精錬して、リアルタイムオブジェクト指向システムの効率的なモデル検査が実現できることを明らかにした。

The development of CEGAR is based on the abstract refinement of structure and time, and the direct detection of speech and speech. As a result, the realization of CEGAR, the generation and elimination of CEGAR, the transformation of CEGAR structure and the transformation of CEGAR structure are abstracted and refined simultaneously.

项目成果

並列動作する確率時間システムに対する拡張CEGAR

用于并行运行的随机时间系统的扩展 CEGAR

• 发表时间: 2008
• 作者: 安井雅俊;山崎真一;山根智
• 通讯作者: 山根智

動的再構成可能組込みシステムのモデル化と仕様記述

动态可重构嵌入式系统的建模和规范

• 发表时间: 2012
• 期刊: 第10回 ディペンダブルシステムワークショップ (DSW 2012)
• 作者: 柳瀬 龍;酒井 辰典;酒井 誠;山根 智
• 通讯作者: 山根 智

"階層構造の抽象化精錬によるステートチャートの自動検証", コンピュータソフトウェア

“通过层次结构的抽象细化自动验证状态图”，计算机软件

• 发表时间: 2009
• 期刊: 日本ソフトウェア科学会 Vol.26,No.3
• 作者: 山崎真一;山根智
• 通讯作者: 山根智

階層構造の抽象化精錬によるステートチャートの自動検証

通过层次结构的抽象细化自动验证状态图

• 发表时间: 2009
• 期刊: コンピュータソフトウェア 26(3)
• 作者: 山根智;山崎真一
• 通讯作者: 山崎真一

UMLと時間オートマトンを用いたソフトリアルタイムシステムの設計解析手法

使用UML和时间自动机的软实时系统设计分析方法

• 发表时间: 2007
• 期刊: 情報処理学会論文 Vol.48,No9
• 作者: 坂倉賢昭;山根智
• 通讯作者: 山根智