Linux环境下基于MSVL的仿真与验证

发布时间：2018-01-07 13:45

  本文关键词：Linux环境下基于MSVL的仿真与验证　出处：《西安电子科技大学》2013年硕士论文　论文类型：学位论文

  更多相关文章： 时序逻辑 MSVL 形式化方法 仿真验证 CTCS-3系统

【摘要】：随着计算机和互联网技术的快速发展，各种软、硬件系统已经广泛渗透到人类生产和生活中，如何保证计算机系统严格按照人类设计的方式进行工作已经成为当前计算机相关研究课题之一。采用形式化方法来描述软硬件系统，能够有效地减少系统设计中的错误，提高设计的可靠性。时序逻辑作为一种形式化方法已被广泛的应用于系统的仿真和验证中。 建模仿真和验证语言(Modeling, Simulation and Verification Language，MSVL)是一种基于投影时序逻辑(Projection Temporal Logic，PTL)的时序逻辑程序设计语言，它可以用于对计算机软硬件系统进行建模、仿真和验证。本文主要讨论Linux环境下基于MSVL的仿真和验证。文中首先介绍了PTL和MSVL的语法和语义，，并讨论了MSVL解释器的实现原理和功能，接着介绍了MSVL对系统进行仿真和验证的原理，然后基于系统层次化设计理论详细介绍了MSVL对系统的形式化描述方法，最后给出了一个用MSVL对CTCS-3列控系统进行形式化描述的实例，借助解释器MSV实现了对CTCS-3系统的仿真和验证，并给出了仿真和验证的结果。实例结果表明，此方法可以有效地检测系统设计上的缺陷。
[Abstract]:With the rapid development of computer and Internet technology , various software and hardware systems have been widely used in human production and life . How to ensure the computer system to work in strict accordance with human design has become one of the current computer - related research topics . The formal method is used to describe the software and hardware system , which can effectively reduce the errors in the system design and improve the reliability of the design . The time sequence logic has been widely used in the simulation and verification of the system as a formal method . Modeling , Simulation and Verification Language ( MSVL ) is a kind of sequential logic programming language based on Projection Logic Logic , which can be used to model , simulate and validate the hardware and software system of computer .

【学位授予单位】：西安电子科技大学
【学位级别】：硕士
【学位授予年份】：2013
【分类号】：TP302

【参考文献】

相关期刊论文 前2条

1 林惠民,张文辉;模型检测:理论、方法与应用[J];电子学报;2002年S1期

2 王淑礼,袁俊红,江祥奎;描述与求解哲学家就餐问题的Petri网模型研究[J];信阳师范学院学报(自然科学版);2004年04期

相关博士学位论文 前1条

1 王小兵;面向对象MSVL语言及其在组合Web服务验证中的应用[D];西安电子科技大学;2009年

相关硕士学位论文 前1条

1 马永涛;框架时序逻辑程序设计解释器及模型检测工具[D];西安电子科技大学;2008年

本文编号：1392826