位置：成果数据库 > 期刊 > 期刊详情页
Formal verification with projection temporal logic
  • ISSN号：1000-9825
  • 期刊名称：《软件学报》
  • 时间：0
  • 分类：TP311.11[自动化与计算机技术—计算机软件与理论;自动化与计算机技术—计算机科学与技术] TP393.08[自动化与计算机技术—计算机应用技术;自动化与计算机技术—计算机科学与技术]
  • 作者机构：[1]ICTT and ISN Laboratory, Xidian University, Xi'an 710071 , China
  • 相关基金：Acknowledgements This work was supported by the National Natural Science Foundation of China （Grant Nos. 61133001, 61272117, 61202038, 61322202, 61420106004 and 91418201）.
作者： TIAN Cong DUAN ZhenHua[1]
关键词： 区间时序逻辑, 形式化验证, 投影, PTL, 时间间隔, 可判定性, 验证方法, 复杂性, Projection temporal logic, Modeling, Verification, Semantics, Model checking
中文摘要：

Projectiontemporallogic (PTL ) isanextensionofintervaltemporallogic (ITL ) withanew projectionoperatorprjandinfiniteintervalswhichhasbeenwellinvestigatedinthepasttenyears.Inthis 纸， wereviewtheworkonPTLinfouraspects :(1 ) decidability， complexityandexpressivenessof propositionalPTL (PPTL ) ；(2 ) 建模， simulationandverificationlanguage (MSVL ) ；(3 ) formalverificationapproacheswithMSVLandPPTL；并且(4 ) supportingtoolkitMSV。

英文摘要：

Projection temporal logic （PTL） is an extension of interval temporal logic （ITL） with a new projection operator prj and infinite intervals which has been well investigated in the past ten years. In this paper, we review the work on PTL in four aspects： （1） decidability, complexity and expressiveness of propositional PTL （PPTL） ; （2） modeling, simulation and verification language （MSVL） ; （3） formal verification approaches with MSVL and PPTL, and （4） supporting toolkit MSV.

同期刊论文项目
基于定理证明的多核并行程序验证
期刊论文 17 会议论文 10 获奖 1
C/Verilog程序的MSVL验证理论与方法
期刊论文 3
开放软件系统的基础理论与关键技术
期刊论文 20
基于共享变量的多核并发程序模型检测
期刊论文 9
基于语义的恶意程序主动防御与检测机理研究
期刊论文 7
形式化验证
期刊论文 10
同项目期刊论文
分布式软件系统交互行为建模、验证与测试
绳牵引摄像机器人的力位混合稳定性评价方法
性能非对称多核处理器上的自适应调度
真并发等价性下的流程模型转换方法
基于事件确定有限自动机的UML2．0序列图描述与验证
BPEL流程建模中的交叠模式分析与转换
PN2MSVL：工作流网到MSVL的转换
自由选择工作流网的可靠完备化简规则集
一个命题投影时序逻辑符号模型检测器
MSVL程序的自动定理证明方法
利用区间与概率的星载可展天线齿轮防卡分析
一种布尔子句的两阶段聚类方法
NuTL2PFG：νTL公式的可满足性检查
基于聚类和划分的SAT分治判定
二维逻辑PPTL^SL的可满足性检查
面向Agent程序设计的研究
一种基于多Agent系统的云服务自组织管理方法
WISHBONE片上总线符号模型检测
分布式软件系统交互行为建模、验证与测试
利用区间与概率的星载可展天线齿轮防卡分析
一种布尔子句的两阶段聚类方法
NuTL2PFG：νTL公式的可满足性检查
基于聚类和划分的SAT分治判定
二维逻辑PPTL^SL的可满足性检查
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程序的自动定理证明方法
WISHBONE片上总线符号模型检测
NuTL2PFG：νTL公式的可满足性检查
二维逻辑PPTL^SL的可满足性检查
分布式软件系统交互行为建模、验证与测试
绳牵引摄像机器人的力位混合稳定性评价方法
性能非对称多核处理器上的自适应调度
PN2MSVL：工作流网到MSVL的转换
自由选择工作流网的可靠完备化简规则集
一个命题投影时序逻辑符号模型检测器
MSVL程序的自动定理证明方法
WISHBONE片上总线符号模型检测
分布式软件系统交互行为建模、验证与测试
PN2MSVL：工作流网到MSVL的转换
一个命题投影时序逻辑符号模型检测器
利用区间与概率的星载可展天线齿轮防卡分析
一种布尔子句的两阶段聚类方法
NuTL2PFG：νTL公式的可满足性检查
基于聚类和划分的SAT分治判定
二维逻辑PPTL^SL的可满足性检查
WISHBONE片上总线符号模型检测
期刊信息
  • 《软件学报》
  • 北大核心期刊（2011版）
  • 主管单位:中国科学院
  • 主办单位:中国科学院软件研究所 中国计算机学会
  • 主编：赵琛
  • 地址：北京8718信箱中国科学院软件研究所
  • 邮编：100190
  • 邮箱：jos@iscas.ac.cn
  • 电话：010-62562563
  • 国际标准刊号：ISSN：1000-9825
  • 国内统一刊号：ISSN：11-2560/TP
  • 邮发代号:82-367
  • 获奖情况:
  • 2001年入选中国期刊方阵“双百期刊”,2000年荣获中国科学院优秀科技期刊一等奖
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,美国数学评论（网络版）,波兰哥白尼索引,德国数学文摘,荷兰文摘与引文数据库,美国工程索引,美国剑桥科学文摘,英国科学文摘数据库,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊（2004版）,中国北大核心期刊（2008版）,中国北大核心期刊（2011版）,中国北大核心期刊（2014版）,中国北大核心期刊（2000版）
  • 被引量:54609