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

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

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

这项研究旨在通过结合程序验证，类型系统和模型检查技术的典型方法来建立新的程序验证方法。今年的研究结果如下： - 改进典型的平行程序分析设备，该设备以前一直在研究，并且已经通过典型的并行程序改进了结合类型系统和模型检查技术的并行程序，以提高验证僵局的存在或不存在。这允许使用递归在过程中自动验证僵局的自由，这以前没有成功。 - 改进计算资源使用验证，我们开发了一种研究方法，用于分析使用类型系统的计算资源（例如文件，内存和网络）的使用。未解决的类型尚未解决。设计了一种算法来确定推论资源的访问顺序是否符合程序员声明的资源使用情况，并证明了其健全性和完整性。这使得能够完全自动验证计算资源的使用情况。基于此结果，实施了计算资源使用验证程序的原型，以证明验证方法的有效性。・一种新的方法，用于验证使用类型和模型检查的组合进行信息流分析的研究程序，并未泄漏敏感信息，首先，首先，一种方法用于使用类型进行分析，然后对分析进行分析，然后使用分析模型进行分析，然后进行分析信息，然后进行分析。与单独使用模型检查相比，这允许更快，并且可以生成一个具体的信息泄漏示例，这与单独使用类型的方法不同。

项目成果

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;四熊 尚方;湯瀬 芳洋;岩間 太
• 通讯作者: 岩間 太

Resource usage analysis

• DOI: 10.1145/1057387.1057390
• 发表时间: 2002-01
• 期刊: ACM Trans. Program. Lang. Syst.
• 作者: Atsushi Igarashi;N. Kobayashi