互联网 qkzz.net
全刊杂志网:首页 > 女性 > 文章正文
刊社推荐

用带时钟变量的线性时态逻辑扩充Object-Z


□ 文志诚 李长云 满君丰

   (湖南工业大学 计算机与通信学院 湖南 株洲 412008)
  
  摘 要:ObjectZ是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首先用时钟变量扩充线性时态逻辑,接着提出了一个方法——用带时钟变量的时态逻辑(LTLC)来扩充ObjectZ。用LTLC扩充的ObjectZ是一个模块化规格说明语言,是ObjectZ语法和语义的最小扩充,其最大优点在于它能方便地描述和验证复杂的实时软件规格说明。
  关键词:ObjectZ; 用带时钟变量的时态逻辑; 实时系统; 形式规格说明; 形式验证
  中图分类号:TP311文献标志码:A
  文章编号:1001-3695(2009)05-1764-06
  
  Adding linear temporal logic with clocks to ObjectZ
  WEN Zhicheng LI Changyun MAN Junfeng
  (School of Computer & Communication Hunan University of Technology Zhuzhou Hunan 412008 China )
  Abstract:ObjectZ an extension to formal specification language Z is good for describing large scale objectoriented software specification. While ObjectZ has found application in a number of areas its utility is limited by its inability to specify continuous variables and realtime constraints. Linear temporal logic can describe realtime system but it can not deal with time variables well and also can not describe formal specification modularly. This paper extended linear temporal logic with clocks(LTLC) and presented an approach to adding linear temporal logic with clocks to ObjectZ. Extended ObjectZ with LTLC a modular formal specification language is a minimum extension of the syntax and semantics of ObjectZ. The main advantage of this extension lies in that it is convenient to describe and verify the complex realtime software specification. ......
很抱歉,暂无全文,若需要阅读全文或喜欢本刊物请联系《计算机应用研究》杂志社购买。
欢迎作者提供全文,请点击编辑
分享:
 

了解更多资讯,请关注“木兰百花园”
分享:
 
精彩图文


关键字
支持中国杂志产业发展,请购买、订阅纸质杂志,欢迎杂志社提供过刊、样刊及电子版。
关于我们 | 网站声明 | 刊社管理 | 网站地图 | 联系方式 | 中图分类法 | RSS 2.0订阅 | IP查询
全刊杂志赏析网 2017