首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到15条相似文献,搜索用时 78 毫秒
1.
基于XYZ/E的混成系统   总被引:3,自引:0,他引:3  
混成系统是由计算机和物理设备组成的嵌入式实时计算系统.它允许在交互式实时系统中引入连续变化的单元.XYZ/E 是基于Manna-Pnueli的线性时序逻辑的程序设计语言.它将程序的动态语义与静态语义统一在同一框架中,支持从抽象的程序规范到可执行代码的逐步求精的全过程.该文使用XYZ/E语言描述和验证混成系统.首先介绍了计算模型,然后介绍了XYZ语言对混成系统的形式化描述,最后介绍了混成系统的验证.与同类工作相比,XYZ/E支持状态转换,从而可以方便地描述复杂的控制算法.  相似文献   

2.
基于时序逻辑的软件体系结构描述语言XYZ/ADL   总被引:26,自引:1,他引:26       下载免费PDF全文
朱雪阳  唐稚松 《软件学报》2003,14(4):713-720
  相似文献   

3.
李广元  唐稚松 《软件学报》2000,11(3):285-292
指针是一种重要的数据类型,使用指针能使程序更加有效和优美.可是指针却以不易驾御而闻名,至今在时序逻辑语言中未见到对它的形式化工作.XYZ/E既是一个时序逻辑系统也是一个程序设计语言,它能表示普通高级语言中几乎所有的重要机制.本文主要讨论在时序逻辑语言XYZ/E中指针的形式化表示问题以及在结构化XYZ/SE程序中指针的验证问题.  相似文献   

4.
可视化体系结构描述语言XYZ/ADL   总被引:31,自引:3,他引:28  
骆华俊  唐稚松  郑建丹 《软件学报》2000,11(8):1024-1029
  相似文献   

5.
闫安  唐稚松 《软件学报》2000,11(6):711-719
XYZ/E是一个时序逻辑系统,同时也是一种时序逻辑程序设计语言。XYZ/E能够在统一的框架下表示高层和低层的描述,所以便于软件系统的描述与实现。该文对基于XYZ/E的蒸气锅炉问题进行了描述与实现,并介绍了为该问题实现的图形用户界面.  相似文献   

6.
UML2.0通信图可以表示对象之间的交互,很适合用于对系统的交互行为建模,但由于UML缺乏精确语义,使得难以对其所表示的系统行为进行分析和验证.XYZ/E是可执行线性时序逻辑语言,既可描述系统的静态语义和动态语义.在定K.UML2.0通信图的形式化语法的基础上,给出了通信图的XYZ/E时序逻辑语义,为进一步的系统分析和验证提供了形式化基础.  相似文献   

7.
针对软件形式化描述和正确性验证研究中存在的问题,提出了基于XYZ/SE的统一框架研究该问题。在该框架下,基于逐步求精思路对软件进行抽象;对软件整体进行形式化描述和部分正确性验证;对抽象得到的软件各部分进行形式化描述和部分正确性验证;进行调整和验证,即:如果推导结果与预期不一致,则需要重写相关程序或者回溯检查推导过程是否存在错误,直至程序部分正确性得到验证为止。以国库信息处理系统为对象,分析了基于XYZ/SE的统一框架性能。分析表明,基于该框架能够对软件的不同抽象层次进行规范描述,实现从抽象(静态语义)到具体(动态语义)的平滑过渡。同时,基于XYZ/SE的统一框架也可以表示Hoare逻辑推演规则。  相似文献   

8.
赵琛  唐稚松  马华东 《软件学报》2000,11(8):996-1002
XYZ系统是一个以增强软件可靠性和提高软件生产率为目的的程序开发支撑系统.它由时序逻 辑语言(temporal logic language,简称TLL)XYZ/E和以该语言为基础的一组软件工程工具组 成.为了研究XYZ系统在多媒体领域中的应用问题,介绍了一种依据多媒体对象时序描述 自动生成用XYZ/RE表示的播放同步器的方法,XYZ/RE是时序逻辑语言族XYZ/E中表示实时系统 的子语言.与相关工作比较,该方法不仅可以处理简单的时序关系,而且可以处理嵌套的时序 关系,所产生的同步器可以复用于不同的节目.  相似文献   

9.
时序逻辑语言XYZ/E在统一的逻辑框架下既能表示静态语义又能表示动态语义,支持软件体系结构从高层到低层的逐步过渡。该文建立了CA认证系统组件模型,采用基于组件的逐步求精方法,用XYZ/E描述了CA认证系统的体系结构。  相似文献   

10.
龚洁 《软件学报》1996,7(Z1):170-177
本文介绍交互式图形工具XYZ/BESE,它能将任意时序逻辑语言XYZ/E的子语言XYZ/BE表示的程序转换成结构化程序.如以XYZ/BE作为中间语言,并将这工具与XYZ与系统中源语言转换系统XYZ/CCSS结合起来,即可将任意其它源语盲的程序转换成为结构化程序.本系统是用XYZ/E的交互式图形设计工具XYZ/CFC实现的。结构化转换过程用图形表示,可增加其直观性,使这变换易于理解.  相似文献   

11.
XYZ系统是一个CASE工具系统.它的核心是一个时序逻辑语言XYZ/E.XYZ/E有一基本的表示状态转换的低级形式XYZ/BE(或用于表示并发的XYZ/CE)及一个结构化的高级形式XYZ/SE.它们均有其相应的图形表示.XYZ/CFC与XYZ/PAD是分别以XYZ/BE(或XYZ/CE)及XYZ/SE用逐步求精方法进行程序设计的交互式的图形环境.每步均可由图形程序自动生成时序逻辑形式的程序.  相似文献   

12.
用XYZ/E语言描述和验证硬件的行为   总被引:6,自引:1,他引:5  
本文考虑用时态逻辑语言XYZ/E描述硬件行为的可行性.作为实例,用XYZ/E语言描述了一个基于微处理器的容错计算机系统,这种描述可以在XYZ系统上执行,从而可对系统进行模拟.特别有意义的是利用XYZ/VERI验证子系统对所期望的性质进行了形式化证明.本文还将XYZ/E描述与相应的VHDL(VHSIChardwaredescriptionlanguage)描述进行了比较.从中可以看出时态逻辑语言的描述具有其独特的优点.  相似文献   

13.
XYZ系统在动画设计中的应用   总被引:5,自引:0,他引:5  
XYZ系统是一套以线形时序逻辑为基础的CASE环境系统,其核心是时序逻辑语言XYZ/E.XYZ/ADL(animationdescriptionlanguage)是XYZ系统在动画领域的应用.马华东博士采用基于时序逻辑的动画描述模型TLAD(temporal-logic-basedanimationdescriptionmodel),提出了动画剧本描述语言(SDL/A).本文介绍的XYZ/ADL语言是以XYZ/E的框架为基础扩充SDL/A而成.它使用XYZ/E中面向对象程序设计的基本结构——代理机构(Agent)作为基本描述单元.代理机构由通讯进程和相应的包块构成,包块处理对象封装,进程处理通讯.从而能更方便地刻画动画过程中的复杂、多层次的角色(包括父子角色)的运动特征及多角色之间的同步协调关系,并且在统一的逻辑框架下实现了计算机动画中运动对象的行为抽象和运动的抽象描述,更具一般性.  相似文献   

14.
张文辉 《软件学报》1995,6(12):719-727
XYZ/E的好处之一在于高级和低级的说明能够在同一框架下表示,因而使得软件的说明和实现变得容易一些.在这同时,开发验证工具以验证不同层次的说明是否满足所期望的关系是很重要的.谢洪亮等同志曾研究过XYZ/SE程序的验证规则.本篇文章增加了有关使用数组、过程说明和过程调用的规则.同时着重说明XYZ/SE程序验证的自动化方面的问题,且实现了一些化简验证条件的规则.  相似文献   

15.
A Structured Temporal Logic Language:XYZ/SE   总被引:2,自引:0,他引:2       下载免费PDF全文
In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is the basis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a general conpositional verification method in the XYZ system concerning the sequential case.  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号