基于XYZ/E的混成系统

混成系统是由计算机和物理设备组成的嵌入式实时计算系统.它允许在交互式实时系统中引入连续变化的单元.XYZ/E 是基于Manna-Pnueli的线性时序逻辑的程序设计语言.它将程序的动态语义与静态语义统一在同一框架中,支持从抽象的程序规范到可执行代码的逐步求精的全过程.该文使用XYZ/E语言描述和验证混成系统.首先介绍了计算模型,然后介绍了XYZ语言对混成系统的形式化描述,最后介绍了混成系统的验证.与同类工作相比,XYZ/E支持状态转换,从而可以方便地描述复杂的控制算法.     

抽象解释理论框架及其应用

在高度依赖计算机的现代社会,软件（特别是大型实时安全攸关软件）的可靠性成为计算机界和整个社会都非常关注的问题。现有的形式化软件验证工具都不得不通过近似来处理复杂问题中的计算,P.Cousot和R.Cousot提出的抽象解释作为一种在数学模型间进行可靠近似的理论,为各类自动验证工具中不同的近似方法建立起一个统一的形式化框架。抽象解释理论在程序分析和验证研究领域得到了广泛的关注与应用,其应用范围涵盖了程序静态分析、程序变换、程序调试、程序水印等方面。描述了基于程序不动点语义的抽象解释理论框架,并对其近年来的应用现状进行了较为全面的介绍,最后给出了抽象解释理论中尚存在的一些问题及可能的研究方向。     

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

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

UML活动图的时序逻辑语义

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

程序性质的描述与证明

XYZ/E是一种基于Manna-Pnueli线性时序逻辑的线性时序逻辑语青(LTLL),其主要特征为它在统一的时序逻辑框架下既能表示程序的静态规范(XYZ/AE)也能表示可执行代码(XYZ/EE),因此程序规范和程序可执行代码的语义一致性也就得以在时序逻辑框架下验证。对于顺序程序,XYZ系统提供了一套基于Hoare逻辑规则的验证工具XYZ/VERI。此工具通过读取程序及其前后断     

一个面向C和Fortran数值程序的静态分析工具

程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式。在此基础上,本文还对数组等复杂语法结构进行了建模和抽象。实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题。     

基于XYZ/ADL的网络中心化仿真运行支撑平台体系结构形式化描述

网络中心化仿真运行支撑平台体系结构是为了满足动态构建仿真任务共同体而提出的相应支撑环境。采用基于XYZ/ADL的双重软件体系结构描述框架,分别从图形语言和形式语言对仿真运行支撑平台体系结构进行了描述并对仿真任务共同体构建中仿真核心服务层实施了分解与逐步求精。该体系结构描述方法不但从可视化角度表示了仿真运行支撑平台体系结构框图及行为抽象,还从形式化角度验证了体系结构设计的正确性和完整性。该研究是形式化描述方法在军事领域的全新尝试,为仿真运行支撑平台服务的合成与重用机制提供了形式化的理论指导。     

基于CPA的抽象解释分析方法研究

安全关键领域中,如何保证软件安全性已经成为了一个广受关注的重要课题。确保程序中没有运行时错误,对于软件安全性的保证十分重要。基于抽象解释的静态分析方法对程序语义进行抽象,是验证运行时错误最合适的形式化方法之一。可配置程序分析（configurable program analysis,CPA）是一种适合多种静态分析方法的通用分析框架。本文使用CPA对抽象解释分析方法进行建模,给出了使用基于CPA的抽象解释方法验证程序中的运行时错误的验证流程,并用实例说明该验证方法的有效性。为程序中运行时错误的自动化分析和验证提供了一种可行方案。     

基于XYZ/ADL的电梯控制系统体系结构的描述与求精

研究软件体系结构的首要问题是如何描述体系结构模型;运用XYZ/ADL描述软件体系结构模型,可以在统一时序逻辑框架下描述系统静态语义到实现之间不同抽象层次的规范,便于体系结构的逐步求精及相关性质分析;以电梯控制系统为例,运用XYZ/ADL形式化地描述了系统体系结构的风格、静态模型和动态模型,并对体系结构模型的主要组件进行了逐步求精,使系统的体系结构从最初的总体功能规范平滑地过渡到了最终的可执行程序;研究表明:形式化描述语言XYZ/ADL在实时控制系统的开发中有着重要的实践意义。     

一种基于UPPAAL的Web服务组合模型检测方法

Web服务组合的正确性验证对提高软件开发效率、实现服务增值具有重要意义。为从高层抽象层次研究Web服务组合的正确性及其形式化验证方法,考虑到Web服务组合中的实时特征,在采用软件体系结构描述语言XYG/ADL对Web服务组合进行描述的基础上,将其实时描述部分XYZ/RE转换至时间自动机模型,组合后系统应满足的性质用分支时序逻辑CTL公式表示,最后应用模型检测工具UPPAAL实现了Web服务组合正确性的自动化验证。     

A Structured Temporal Logic Language:XYZ/SE

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.     

XYZ／SE程序的验证

ＸＹＺ／Ｅ的好处之一在于高级和低级的说明能够在同一框架下表示，因而使得软件的说明和实现变得容易一些．在这同时，开发验证工具以验证不同层次的说明是否满足所期望的关系是很重要的．谢洪亮等同志曾研究过ＸＹＺ／ＳＥ程序的验证规则．本篇文章增加了有关使用数组、过程说明和过程调用的规则．同时着重说明ＸＹＺ／ＳＥ程序验证的自动化方面的问题，且实现了一些化简验证条件的规则．     

An Introduction to IN CAPS System

INCAPS，a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System,The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program‘s correctness which are supported respectively by the mechanized logics-FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system:the rules,implementation,tactics,forward proof and backward proof.It also gives several typical examples for demonstration of INCAPS‘ working principle.The achievement to data in that we have now accomplished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.     

基于时态逻辑的软件体系结构描述语言及其可视化环境

在时态逻辑语言XYZ／E的基础上,建立了一种以可视化图形表示的软件体系结构描述语言XYZ／ADL．它可同时描述软件体系结构的静态与动态行为,能在统一的形式框架下完成不同抽象层次体系结构设计之间的逐步过渡,从而将模块化程序设计方法和基于规范的逐步求精方法有机地结合起来。     

基于形式化描述的电梯控制系统的建模与仿真

研究电梯控制系统中组件之间复杂的信号传输关系。针对传统的建模方法不能同时精确描述系统模型的静态与动态语义的问题,从系统体系结构的组件与连接件入手,探讨形式化描述语言XYZ/ADL描述系统模型的特性,运用XYZ/ADL形式化地描述电梯控制系统的总体功能规范、主要组件的结构模型、组件之间信号传输的动态模型和电梯运行模型,并基于所构建的形式化描述模型实现系统的仿真运行。结果表明,基于XYZ/ADL描述的形式化模型能准确分析电梯组件之间复杂的信号传输关系,精确模拟电梯运行的各种状态。