位置：立项数据库 > 立项详情页
基于定理证明的多核并行程序验证
  • 项目名称：基于定理证明的多核并行程序验证
  • 项目类别：青年科学基金项目
  • 批准号：61202038
  • 申请代码：F020106
  • 项目来源：国家自然科学基金
  • 研究期限：2013-01-01-2015-12-31
  • 项目负责人：张南
  • 依托单位：西安电子科技大学
  • 批准年度：2012
中文摘要：

扩展命题投影时序逻辑Propositional Projection Temporal Logic(PPTL)，提出适合描述多核并行程序的柱面计算模型Cylinder Computation Model(CCM)，建立扩展的命题投影时序逻辑CCM-PPTL系统。研究它的语法，语义和逻辑规则，研究它的范式，范式图及可判定性。定义CCM-PPTL的公理和推理规则，建立CCM-PPTL的公理系统；证明该公理系统的合理性和完备性。对PPTL定理证明器进行扩展，实现基于PVS的CCM-PPTL证明器原型。建立基于CCM-PPTL公理系统和证明器对多核并行程序进行验证的理论和方法。

中文主题词： 定理证明；时序逻辑；多核；并行程序；形式化验证
结论摘要：

英文主题词Theorem Proving；Temporal Logic；Multi-Core；Parallel Program；Formal Verification

成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 17
  • 10
  • 0
  • 1
  • 0
期刊论文
A formal proof of the deadline driven scheduler in PPTL axiomatic system
Verification of embedded real - time systems using symbolic model checking : a case study
Verifying safety critical task scheduling systems in PPTL axiom system
绳牵引摄像机器人的力位混合稳定性评价方法
Verification of distributed systems with the axiomatic system of MSVL
A complete axiom system for propositional projection temporal logic with cylinder computation model
An extended strange planet protocol
性能非对称多核处理器上的自适应调度
PN2MSVL：工作流网到MSVL的转换
一个命题投影时序逻辑符号模型检测器
MSVL程序的自动定理证明方法
Formal verification with projection temporal logic
WISHBONE片上总线符号模型检测
会议论文
Extending MSVL with Function Calls
An axiomatization for cylinder computation model
Detecting spurious counterexamples efficiently in abstract model checking
A transformation from p-π to MSVL
Simulation of CTCS-3 protocol with temporal logic programming
Extending MSVL with function calls
Translation from Workflow Nets to MSVL
Some fixed-point issues in PPTL
Normal form expressions of propositional projection temporal logic
An Extended Strange Planet Protocol
获奖
可信软件设计开发与验证的基础理论与关键技术
相关项目
符号轨迹计值的形式化语义及模型检测技术研究
期刊论文 1 会议论文 3
集成电路NoC低功耗通讯协议栈基础研究
期刊论文 13
物联网中可信设备协同的建模与验证方法研究
期刊论文 5 会议论文 9
针对安全关键系统的多语言编程形式化验证
期刊论文 3 会议论文 1
基于抽象的软件符号模型检测研究
期刊论文 20
基于加速效应的多核系统实时调度模型MAMORTS及其算法研究
期刊论文 1 会议论文 1
框架时序逻辑程序设计
期刊论文 54 会议论文 46 获奖 1 著作 3
基于约束凸多面体和抽象加细技术的混合系统的模型检测
期刊论文 22 会议论文 4 专利 1
多核处理器中非确定性错误的调试技术研究
期刊论文 11 会议论文 3 著作 1
张南的项目
基于动态符号执行的MSVL程序模型检测