Research on the verification of highly parallel and concurrent embedded software

高度并行并发嵌入式软件验证研究

• 批准号: 20680001
• 负责人: AOKI Toshiaki
• 金额: $ 15.81万
• 依托单位: Japan Advanced Institute of Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (A)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20680001/
• 关键词: 形式手法; 形式検証; モデル検査; ソフトウェア工学; ソフトウェア開発効率化・安定化; ディペンダブル・コンピューティング

We focus on parallel/concurrent software which is controlled by real-time operating system(RTOS) and RTOS itself. We have proposed an algorithm and tool to verify the behavior of parallel/concurrent software which contains scheduling by RTOS and real-time for the former. For the latter, we have proposed a method and tools to verify the design and implementation of RTOS. In addition, we have applied those method and tools to RTOS products. We succeeded in proposing verification methods based on model checking in practical settings and conducted that they are applicable to practical software products.

我们专注于由实时操作系统（RTOS）和RTOS本身控制的并行/并发软件。我们提出了一种算法和工具来验证并行/并发软件的行为，其中包括 RTOS 调度和前者的实时调度。对于后者，我们提出了一种方法和工具来验证RTOS的设计和实现。此外，我们还将这些方法和工具应用到了RTOS产品中。我们成功地提出了基于实际环境中的模型检查的验证方法，并证明它们适用于实际的软件产品。

项目成果

An Improvement of Minimized Assumption Generation Method for Component-Based Software Verification

基于组件的软件验证最小化假设生成方法的改进

• 发表时间: 2012
• 作者: Pham Ngoc Hung;Viet Ha Nguyen;Toshiaki Aoki;Takuya Katayama
• 通讯作者: Takuya Katayama

RTOS設計検証の経験から

来自 RTOS 设计验证的经验

• 发表时间: 2010
• 作者: 森信介;笹田鉄郎;Neubig Graham;高岡晃教,佐藤昇志,宮崎忠昭,南山堂;K. Tanaka;青木利晃
• 通讯作者: 青木利晃

モデル検査によるリアルタイムオペレーティングシステムの設計検証

通过模型检查进行实时操作系统设计验证

• 发表时间: 2008
• 作者: Kanamori;T.;Hido;S.;Sugiyama;M.;渡辺正夫;青木利晃,山崎真吾
• 通讯作者: 青木利晃,山崎真吾

環境モデリングによるモデル検査スクリプトの自動生成

通过环境建模自动生成模型检查脚本

• 发表时间: 2009
• 作者: 関谷毅;染谷隆夫;矢竹健朗,西端浩和,青木利晃
• 通讯作者: 矢竹健朗,西端浩和,青木利晃

Detecting and Analyzing State Inconsistencies in Multi-task Software

检测和分析多任务软件中的状态不一致

• 发表时间: 2009
• 作者: Toshiaki Aoki;Tadashi Sekiguchi;Masayuki Hirayama;and Tomoji Kishi
• 通讯作者: and Tomoji Kishi