型システムとモデル検査の融合によるソフトウェア検証

类型系统和模型检查相结合的软件验证

• 批准号: 16650004
• 负责人: 小林 直樹
• 金额: $ 2.24万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Exploratory Research
• 财政年份: 2004
• 资助国家: 日本
• 起止时间: 2004 至 2006
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-16650004/
• 关键词: 型システム; プログラム解析; ソフトウェア検証; モデル検査; 並行プログラム; 資源使用法解析; 情報流解析; プログラム検証

本研究では,プログラム検証のための代表的な手法である型システム,モデル検査の技術を融合して新しいプログラム検証手法を確立することを目指している.本年度の研究成果は以下のとおり.・並行プログラムの解析器TyPiCalの改良従来から研究をすすめてきた,型システムとモデル検査技術を組み合わせた並行プログラムのための検証器TyPiCalを改良し,デッドロックの有無を検証する能力を向上させた.これにより,従来うまく扱えなかった再帰を用いたプロセスのデッドロックフリーダムを自動で検証できるようになった.・計算資源使用法検証の改良従来から研究をすすめてきたファイルやメモリ,ネットワークなどの計算資源の使用法を型システムを用いて解析する手法の研究を発展させた.未解決のままとなっていた,型を用いて推論された資源のアクセス順序が,プログラマの宣言した資源の使用法に適合しているかどうかを判定するためのアルゴリズムを考案し,その健全性および完全性を証明した.これにより,計算資源の使用法の検証が全自動で行えるようになった.また,この成果に基づいて,計算資源使用法検証器のプロトタイプを実装し,検証手法の有効性を実証した.・型とモデル検査の組み合わせによる情報流解析の手法の研究プログラムが機密情報を漏洩していないことを検証するための新しい手法として,まず型を用いてプログラムを粗く高速に解析し,その解析情報を利用してモデル検査を効率的に行う手法を考案した.これにより,モデル検査のみを使うよりも高速で,型のみによる手法と異なり,情報が漏れる場合の具体例を生成することができる.

This study aims to establish a representative method for the identification of new types and methods of identification by integrating the techniques of identification. This year's research results are as follows: The improved TyPiCal parallel analyzer is designed to improve the ability to detect the presence or absence of a parallel analyzer. This is the first time I've ever seen someone who's been in the business since I was a kid. Research on Improved Methods of Computing Resource Usage Analysis Unsolved problems, type of use, inference of resource access sequence, declaration of resource use method, suitability determination, integrity verification. This is a fully automatic way to verify the usage of computing resources. In addition, the results are based on the implementation of computational resource utilization method, and the effectiveness of the verification method is demonstrated. A Study on the Method of Information Flow Analysis for Type and Type Detection and Combination of Information and Information. A Study on the Method of Information Flow Analysis for Type and Type Detection and Combination of Information and Information. For example, when information is leaked, a specific example is generated.

项目成果

Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes

用于验证 Pi 微积分过程空间性质的偏序约简

• 发表时间: 2004
• 期刊: Proceedings of 11^<th> International Workshop on Expressiveness in Concurrency (EXPRESS 2004)
• 作者: Reynald Affeldt;Naoki Kobayashi
• 通讯作者: Naoki Kobayashi

Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference

结合基于类型的分析和模型检查寻找抗干扰反例

• 发表时间: 2006
• 期刊: Proceedings of ACM SIGPLAN Workshop on Programming Languages and Analysis for Security(PLAS'06)
• 作者: Hiroshi Unno;Naoki Kobayashi;Akinori Yonezawa
• 通讯作者: Akinori Yonezawa

計算資源使用法検証における計算資源の仕様と実際の使用法の間の適合性検証アルゴリズム

计算资源使用验证中计算资源规格与实际使用情况的兼容性验证算法

• 发表时间: 2007
• 期刊: 情報処理学会論文誌:プログラミング 48(SIG4(PRO32))
• 作者: 岩間太;五十嵐淳;小林直樹
• 通讯作者: 小林直樹

例外機構を備えた言語のための資源使用法解析

具有异常机制的语言的资源使用分析

• 发表时间: 2005
• 期刊: PPL2005予稿集
• 作者: Futoshi Iwama;四熊 尚方;湯瀬 芳洋;岩間 太
• 通讯作者: 岩間 太

A New Type System for Deadlock-Free Processes

一种新型无死锁进程系统

• 发表时间: 2006
• 期刊: Proceedings of the 17th International Conference on Concurrency Theory(CONCUR'06) 4137
• 作者: Naoki Kobayashi;Kohei Suenaga;Lucian Wischik;小林直樹
• 通讯作者: 小林直樹