位置：立项数据库 > 立项详情页
基于流分析的分布式Java程序模型检查技术研究
  • 项目名称：基于流分析的分布式Java程序模型检查技术研究
  • 项目类别：面上项目
  • 批准号：60673155
  • 申请代码：F0208
  • 项目来源：国家自然科学基金
  • 研究期限：2007-01-01-2009-12-31
  • 项目负责人：张大方
  • 负责人职称：教授
  • 依托单位：湖南大学
  • 批准年度：2006
中文摘要：

现有的软件测试方法一般以测试用例覆盖率理论为基础，很难发现分布式软件系统中一些关键而隐蔽的错误。本项目研究Java程序的模型检查技术，验证Java程序的时态逻辑性质，以弥补软件测试技术之不足。本项目从Java源程序中提取程序有限状态模型，采用流分析作为Java 程序模型检查的算法基础，开发Java程序模型检查工具，以实际软件系统、网络协议程序为重点开展程序模型检查实验，研究模型检查技术在实际系统中的应用方法和效果；研究新型的高效搜索技术，探索提高模型检查算法时间和空间效率的新途径。本项目开发了Java 源程序分析与模型检查系统（JAMCT），实现了自动从源代码中提取程序模型，自动验证软件的时态逻辑性质；在该系统中，实现了基于流分析的模型检查算法；进一步研究了并发系统的模型检查算法，针对Java内存模型提出更精确的并发模型及检查算法；在以上工作的基础上，开展了模型检查应用于实际系统的实验，对Linux内核，网络协议，安全协议等系统进行性质验证，发现或重现了一些漏洞和缺陷。

中文主题词： Java程序；模型检查；流分析；性质验证；程序模型检查工具
结论摘要：

英文主题词Java Program;model checking;flow analysis;property verify;program model checking tools

成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 56
  • 14
  • 6
  • 0
  • 0
期刊论文
基于计数布鲁姆过滤器的快速多维包分类算法
DHT-based Lightweight Broadcast Algorithms in Large-Scale Computing Infrastructures
基于Gilbert丢包机制的TCP吞吐量模型
Toward accurate and efficient available bandwidth measurement
包对探测统计模型与测量精度分析
一种基于 Linux 内核的高效包分类算法
基于模型检查的 TCP 连接管理协议分析与验证
路径容量测量中包对行为的特征分析
基于 Spin 的 UML 状态图模型检查的设计与实现 ,
IEEE802.11 中 WEP 认证协议的 SPIN 模型检测
面向流量识别系统的聚类算法的比较与分析 ,
带路径探索检测的 RCN 路由抖动抑制算法
Logical causality analysis method for alert correlation
Non-travelling wave solutions to a (3+1)-dimensional potential-YTSF equation and a simplified model
Reliable user-level rollback recovery implementation for multithreaded processes on windows
过程间并发程序分析不可判定的一个新证明方法
基于仿真分析的端到端最小包时延测量方法
程序模型检查的两阶段框架
基于有效载荷分析的 BT 流量识别技术
高速网络中 TCP 拥塞控制算法的研究和改进
端到端最小时延可测性的排队分析与仿真
On Evaluating the Differences of TCP and ICMP in Network Measurement
基于节点性能估算的应用层组播算法
可信高效的可用带宽测量方法研究
Optimizing the BitTorrent performance using an adaptive peer selection strategy
Linux 进程间通信的模型检测
Performance evaluation of end-to-end path capacity measurement tools in a controlled environment
基于 IXP2400 的流量控制实现
基于正方形网格剖分的无线传感器网络方向性路由算法的研究
基于导出策略的路由配置错误检测方法 ,
基于 SPIN 实现 UML Statechart 的模型检查
通信下推系统的一种有界可达算法
Improved sample filtering method for measuring end-to-end path capacity
基于布鲁姆过滤器距离的集合变动定量评估算法
路径容量测量中包对行为的特性分析
端到端最小包时延可测性的排队分析与仿真
基于梯度化邻居节点信息的传感器网络节点距离测量
BitTorrent中一种基于全局贡献的节点选择策略
基于路由更新的BGP路由稳定性监测工具设计
IEEE802.11中WEP认证协议的SPIN模型检测
Netfilter／Iptables框架下基于TCP滑动窗口的串行流量控制算法
WPathload：一种改进的可用带宽测量方法
基于预测的传感器网络副本自适应控制机制
基于无线传感器网络的数据交换算法的研究
基于人工鱼群的DNA编码序列组合优化算法研究
基于MP、RUP对软件过程的研究
会议论文
An Activeness-Based Seed Choking Algorithm for Enhancing BitTorrent's Robustness
A Token-based Broadcast Algorithm over DHT for Large-Scale Computing Infrastructures
A New Algorithm for the Longest Common Subsequence Problem
An Improve Algorithm for the Longest Common Subsequence Problem
Improving Rollback- Recovery Efficiency by Tuning Pessimism Grain
A Coarse-Grained Pessimistic Message Logging Scheme for Improving Roll-back Recovery Efficiency
A Regular Expression Matching Algorithm Using Transition Merging
An Adaptive Sampling Methodology for Internet Traffic Data Measurement
A Coarse-Grained Pessimistic Message Logging Scheme for Improving Roll-back Recovery Efficiency
A New Algorithm for the Longest Common Subsequence Problem
WPathload ：一种改进的可用带宽测量方法
基于 Java 内存模型的并发程序模型检测
A Byte-Filtered String Matching Algorithm for Fast Deep Packet Inspection.
A Partition-based Broadcast Algorithm over DHT for Large-Scale Computing Infrastructures
专利
一种网络路由拓扑对称性的定量评估方法
一种可扩展的布鲁姆过滤器查询方法及元素插入方法
一种基于通用PC的高精度网络时延测量方法
基于布鲁姆过滤器距离的集合变动定量评估方法
基于节点轨迹标签的无结构P2P副本一致性维护方法
一种基于Bloom Filter结构的查询方法
相关项目
无线传感器网络流测量与分析技术研究
期刊论文 2 会议论文 2 专利 1
基于Reo的协调理论及其在信息物理系统开发方法中的应用
期刊论文 3 会议论文 11
基于分离逻辑的程序验证方法研究
期刊论文 9 获奖 2
基于模型检查的软件错误定位技术研究
期刊论文 45 会议论文 9
针对多线程程序失效的用户级半自动诊断方法研究
期刊论文 15 会议论文 8
张大方的项目
软件容错测量理论与技术研究
期刊论文 69 会议论文 9
系统级故障诊断基础理论与算法研究
期刊论文 24 会议论文 13
第10届IEEE/IFIP环太平洋地区可信计算国际会议
基于端系统的网络在线测量理论与方法研究
期刊论文 39 会议论文 15
基于多核处理器的高性能深度数据包检测技术研究
期刊论文 59 会议论文 22
基于图形处理单元的高性能网络包处理技术研究
期刊论文 7
基于模型检查的软件错误定位技术研究
期刊论文 45 会议论文 9