课题基金 / 基金详情

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

型システムとモデル検査の融合によるソフトウェア検証
类型系统和模型检查相结合的软件验证
批准号：
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を改良し,デッドロックの有無を検証する能力を向上させた.これにより,従来うまく扱えなかった再帰を用いたプロセスのデッドロックフリーダムを自動で検証できるようになった.・計算資源使用法検証の改良従来から研究をすすめてきたファイルやメモリ,ネットワークなどの計算資源の使用法を型システムを用いて解析する手法の研究を発展させた.未解決のままとなっていた,型を用いて推論された資源のアクセス順序が,プログラマの宣言した資源の使用法に適合しているかどうかを判定するためのアルゴリズムを考案し,その健全性および完全性を証明した.これにより,計算資源の使用法の検証が全自動で行えるようになった.また,この成果に基づいて,計算資源使用法検証器のプロトタイプを実装し,検証手法の有効性を実証した.・型とモデル検査の組み合わせによる情報流解析の手法の研究プログラムが機密情報を漏洩していないことを検証するための新しい手法として,まず型を用いてプログラムを粗く高速に解析し,その解析情報を利用してモデル検査を効率的に行う手法を考案した.これにより,モデル検査のみを使うよりも高速で,型のみによる手法と異なり,情報が漏れる場合の具体例を生成することができる.
期刊论文(18)
专著(0)
科研奖励(0)
会议论文
Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes
用于验证 Pi 微积分过程空间性质的偏序约简
DOI： --
发表时间： 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
结合基于类型的分析和模型检查寻找抗干扰反例
DOI： --
发表时间： 2006
期刊： Proceedings of ACM SIGPLAN Workshop on Programming Languages and Analysis for Security(PLAS'06)
影响因子： --
作者： [Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa]
通讯作者： Akinori Yonezawa
計算資源使用法検証における計算資源の仕様と実際の使用法の間の適合性検証アルゴリズム
计算资源使用验证中计算资源规格与实际使用情况的兼容性验证算法
DOI： --
发表时间： 2007
期刊： 情報処理学会論文誌:プログラミング 48(SIG4(PRO32))
影响因子： --
作者： [岩間太, 五十嵐淳, 小林直樹]
通讯作者： 小林直樹
例外機構を備えた言語のための資源使用法解析
具有异常机制的语言的资源使用分析
DOI： --
发表时间： 2005
期刊： PPL2005予稿集
影响因子： --
作者： [Futoshi Iwama, 四熊 尚方, 湯瀬 芳洋, 岩間 太]
通讯作者： 岩間 太
共 8 条
    無住道暁と南宋代成立典籍に関する総合的研究
    • 批准号：
      23K00298
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $1.41万
    • 财政年份：
      2023
    • 负责人：
      小林 直樹
    • 依托单位：
      Osaka Metropolitan University
    潜在的カビ毒産生菌種を利用したカビ毒生合成抑制メカニズムの解明
    • 批准号：
      23K05081
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $2.91万
    • 财政年份：
      2023
    • 负责人：
      小林 直樹
    • 依托单位：
      Azabu University
    偏光分光型マルチスペクトルカメラを用いた目視診断用画像システムの研究開発
    • 批准号：
      23K11878
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $3.08万
    • 财政年份：
      2023
    • 负责人：
      小林 直樹
    • 依托单位：
      Saitama Medical University
    Program Verification Based on Higher-Order Fixpoint Logic
    • 批准号：
      20H00577
    • 项目类别：
      Grant-in-Aid for Scientific Research (A)
    • 资助金额：
      $28.45万
    • 财政年份：
      2020
    • 负责人：
      小林 直樹
    • 依托单位：
      The University of Tokyo
    海外基金