首页> 中文期刊> 《西安电子科技大学学报》 >MSVL语言的公理系统的程序验证

MSVL语言的公理系统的程序验证

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言.为了证明区间时序逻辑程序的正确性,提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则,以及将程序从一个状态转换到另一个状态的区间公理和区间推演规则.最后给出验证实例说明基于该公理系统的程序验证方法.

著录项

来源
《西安电子科技大学学报》 |2010年第1期|96-101|共6页
作者
杨潇潇; 段振华;
展开▼
作者单位

西安电子科技大学计算理论与技术研究所;

展开▼
原文格式 PDF
正文语种 chi
中图分类理论、方法;
关键词
形式验证; 时序逻辑; 正则形; 安全性; 公理系统;

相似文献

中文文献
外文文献
专利

1. PN2MSVL:工作流网到MSVL的转换 [J] . 师亚 ,段振华 ,田聪 . 计算机学报 . 2014,第012期
2. 框架时序逻辑语言MSVL中面向对象机制的实现 [J] . 王小兵 ,段振华 . 西安电子科技大学学报（自然科学版） . 2010,第003期
3. 用于C语言程序验证的性质描述语言C-PDL [J] . 左春华 ,张广泉 ,郭亮 . 苏州大学学报（自然科学版） . 2007,第003期
4. 柯尔莫哥洛夫公理系统的外部矛盾性及合理的概率论公理系统 [J] . 王鸣鹤 . 上海工业大学学报 . 1994,第002期
5. 一个小型公理系统的例子及中学几何公理系统的水平 [J] . 徐亨锡 . 苏州教育学院学报 . 1994,第001期
6. 模态逻辑GL的基于广义谢弗竖的分析性模态公理系统 [C] . Fangfang Tang ,唐芳芳 . 2017年全国现代逻辑学术研讨会 . 2017
7. 基于MSVL的动静结合程序验证和自动规划 [A] . 杨凯 . 2019

获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

客服微信
服务号