项目名称: Java构件的组合模型检验技术研究

项目编号: No.60803042

项目类型: 青年科学基金项目

立项/批准年度: 2009

项目学科: 金属学与金属工艺

项目作者: 文艳军

作者单位: 中国人民解放军国防科学技术大学

项目金额: 20万元

中文摘要: 软件模型检验的可扩展性是一个技术难点,它严重制约了模型检验技术在软件方面的广泛应用。针对此问题,本课题研究以组合的方式对软件系统进行形式验证,以扩大验证规模、提高验证能力。课题针对Java 构件的关键性质在设计层和实现层进行验证,可有效提高软件设计与实现阶段的质量保障能力。本课题研究工作主要包括在构件设计层的基于Fractal构件模型的构件建模和分析、基于cCSP的构件语义模型研究、构件实现层的数据竞争和原子性问题的模型检验、Java构件运行时验证几个方面。本课题的研究能显著提高面向对象软件关键性质的保障能力,能丰富和发展形式验证理论,因而具有广泛的应用价值和重要的科学意义。

中文关键词: 组合模型检验;面向对象程序;形式验证;Fractal构件模型

英文摘要: How to improve the scalability of software model checking is a technical difficulty, which restrains the abroad application of model checking technology on softwares. As to this problem, the project focuses on the formal verification of software systems in a compositional manner, which can improve the scalability of formal verification. The verification problem of Java components at both design and implementation phases will be researched, which can effectively improve the quality assurance ability to software designs and implementations. The main research content includes: component modeling and analysis based on the Fractal component model, component semantics model based on cCSP, model checking of data-race and atomicity problem, runtime verification of Java components. The project can bring benefits to the quality assurance of objectoriented softwares on cricital properties, can enrich and develop the formal verification theories, and thus has abroad application value and important scientific meaning.

英文关键词: compositional model checking; object oriented programs; formal verification; Fractal component model

成为VIP会员查看完整内容
0

相关内容

专知会员服务
33+阅读 · 2021年10月17日
专知会员服务
52+阅读 · 2021年9月18日
专知会员服务
34+阅读 · 2021年8月1日
专知会员服务
92+阅读 · 2021年6月23日
专知会员服务
55+阅读 · 2021年6月1日
专知会员服务
29+阅读 · 2021年5月8日
专知会员服务
21+阅读 · 2021年4月20日
【ACL2020-Google】逆向工程配置的神经文本生成模型
专知会员服务
16+阅读 · 2020年4月20日
肖新光建议:加速推进软件安全工程相关工作
CCF计算机安全专委会
0+阅读 · 2022年3月7日
2021年的Java热门趋势
AI前线
0+阅读 · 2022年2月7日
基于规则的建模方法的可解释性及其发展
专知
4+阅读 · 2021年6月23日
智能合约的形式化验证方法研究综述
专知
13+阅读 · 2021年5月8日
事实抽取与验证研究综述
专知
0+阅读 · 2021年4月20日
已删除
将门创投
18+阅读 · 2019年2月18日
国家自然科学基金
4+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
16+阅读 · 2020年5月20日
小贴士
相关VIP内容
专知会员服务
33+阅读 · 2021年10月17日
专知会员服务
52+阅读 · 2021年9月18日
专知会员服务
34+阅读 · 2021年8月1日
专知会员服务
92+阅读 · 2021年6月23日
专知会员服务
55+阅读 · 2021年6月1日
专知会员服务
29+阅读 · 2021年5月8日
专知会员服务
21+阅读 · 2021年4月20日
【ACL2020-Google】逆向工程配置的神经文本生成模型
专知会员服务
16+阅读 · 2020年4月20日
相关资讯
肖新光建议:加速推进软件安全工程相关工作
CCF计算机安全专委会
0+阅读 · 2022年3月7日
2021年的Java热门趋势
AI前线
0+阅读 · 2022年2月7日
基于规则的建模方法的可解释性及其发展
专知
4+阅读 · 2021年6月23日
智能合约的形式化验证方法研究综述
专知
13+阅读 · 2021年5月8日
事实抽取与验证研究综述
专知
0+阅读 · 2021年4月20日
已删除
将门创投
18+阅读 · 2019年2月18日
相关基金
国家自然科学基金
4+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
微信扫码咨询专知VIP会员