论文部分内容阅读
MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言．为了证明区间时序逻辑程序的正确性，提出了MSVL语言的一个公理系统：包括正则形转换的状态公理和状态推演规则，以及将程序从一个状态转换到另一个状态的区间公理和区间推演规则．最后给出验证实例说明基于该公理系统的程序验证方法．
MSVL语言的公理系统的程序验证
【摘 要】
：
MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言．为了证明区间时序逻辑程序的正确性，提出了MSVL语言的一个公理系统：包括正则形转换的状态公理和状态推演规
【机 构】
：
西安电子科技大学计算理论与技术研究所
【出 处】
：
西安电子科技大学学报
【发表日期】
：
2010年1期
【基金项目】
：
国家自然科学基金资助项目（60873018）,国家自然科学基金重点资助项目（60433010）
其他文献
针对杂波干扰环境下的被动多目标跟踪问题,将多站集中式融合方法与概率假设密度粒子滤波递归过程相结合,实现被动多目标跟踪.进一步,将概率假设密度粒子滤波递归过程并行化处