基于XYZ／E的CA认证系统描述与求精

时序逻辑语言XYZ／E在统一的逻辑框架下既能表示静态语义又能表示动态语义，可以实现从抽象描述到可执行程序的平滑过渡。本文建立了CA认证系统组件求精模型，对CA和RA组件用XYZ／E进行了描述和求精。     

基于时序逻辑的UML2.0通信图语义研究

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

UML活动图的时序逻辑语义

UML活动图可以表示不同抽象级的控制流,很适合用于对系统的行为建模．但是缺乏精确的语义使得难以对它所表示的系统行为进行分析．XYZ／E是一可执行线性时序逻辑语言,既可描述系统的动态行为又可表示程序性质,用它对活动图形式化后,就可在统一的逻辑框架下分析活动图的性质．定义了一个有向图结构用以表示UML活动图,再给出其XYZ／E语义,并用一个例子说明活动图到XYZ／E的语义转换,为进一步的分析提供形式化基础．     

基于线性时序逻辑的实时系统建模与求精

线性时序逻辑语言XYZ／E在统一的语义框架下．能表示从高层需求规范到低层实现模型之间的不同抽象层次的系统描述，也适于描述实时系统的模型和逐步求精过程．本文提出了一种基于构件的实时系统求精方法，并给出一个具体实例一电梯控制系统，采用XYZ／E语言描述了该系统的模型及其求精过程．     

双重软件体系结构描述框架XYZ/ADL

体系结构设计在软件开发过程中扮演着重要角色.工程中常用图形语言为软件体系结构建模,它们有直观、半形式化的优点;但是语义不够精确,难以对它们表示的模型进行分析,在这方面,形式化方法可与之互补.但在工程使用中仅用形式化语言建模又不太现实,所以如何结合二者之长以提高软件的可靠性已成为工业界和学术界共同关心的问题.提出了双重软件体系结构描述框架XYZ/ADL:支持工程中软件体系结构的基本概念,前端用一般的体系结构框图作为结构描述,用UML活动图、状态图作为抽象行为表示;后端用既可表示系统动态语义又可表示系统静态语义的时序逻辑语言XYZ/E作为一致的语义基础.前端的图形语言便于软件工程师的交流和使用,后端的形式语言是进一步的形式化分析验证的基础.     

XYZ/E在CA认证系统的一个初步应用

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

UML Statecharts的模型检验方法

统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Büchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统.     

基于时序逻辑语言描述的监控系统的软件体系结构求精

该文提出了一种基于组件的软件体系结构求精方法,主要通过一个具体实例———移动通信监控系统,基于时序逻辑语言XYZ/E形式化描述其体系结构,对该求精方法及过程做进一步阐述。     

基于XYZ/RE的多媒体同步器自动构造方法

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