ISCAS OpenIR  > 基础软件与系统重点实验室
axiomatic temporal logic programs verification
Yang Xiaoxiao; Duan Zhenhua
2010
会议名称2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010
会议录名称Proceedings - 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010
页码87-94
会议日期August 25,
会议地点Taipei, Taiwan
收录类别EI
出版地United States
ISBN9780770000000
部门归属(1) Institute of Computing Theory and Technology, ISN Laboratory, Xidian University, Xi'an,710071, China; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Science, China
摘要In this paper, we investigate the axiomatic system of Modeling Simulation and Verification Language (MSVL). To this end, a set of state axioms and state inference rules is given. They are useful to deduce a program into its normal form. Further, a propositional projection temporal logic is used as assertion language to describe the required property of a program. Moreover, to deduce a program over an interval, a set of rules in terms of triple like Hoare logic is formalized. These rules enable us to deduce a program in its normal form at the current state to the next one and to verify safety, liveness properties over an interval. © 2010 IEEE.
关键词Computer Simulation Languages Logic Programming Safety Engineering Software Engineering
主办者National Taiwan University; Res. Cent. Inf. Technol. Innov., Acad. Sin.; National Science Council; Ministry of Education; IEEE Computer Society
内容类型会议论文
URI标识http://ir.iscas.ac.cn/handle/311060/8682
专题基础软件与系统重点实验室
推荐引用方式
GB/T 7714
Yang Xiaoxiao,Duan Zhenhua. axiomatic temporal logic programs verification[C]. United States,2010:87-94.
条目包含的文件
文件名称/大小 文献类型 版本类型 开放类型 使用许可
05587722.pdf(373KB) 开放获取--请求全文
个性服务
推荐该条目
保存到收藏夹
查看访问统计
导出为Endnote文件
谷歌学术
谷歌学术中相似的文章
[Yang Xiaoxiao]的文章
[Duan Zhenhua]的文章
百度学术
百度学术中相似的文章
[Yang Xiaoxiao]的文章
[Duan Zhenhua]的文章
必应学术
必应学术中相似的文章
[Yang Xiaoxiao]的文章
[Duan Zhenhua]的文章
相关权益政策
暂无数据
收藏/分享
所有评论 (0)
暂无评论
 

除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。