基于进程代数规约生成软件体系结构模型的方法

需求规约到软件体系结构(SA)模型的转换是软件工程领域的一个研究热点,UML-RT广泛用于实时系统软件体系结构建模,然而基于自然语言规约建立的UML-RT模型往往是不精确的,存在二义性,为了解决这一问题,需要赋予UML-RT模型形式化语义.进程代数是一种用来解决并发系统通信问题的形式化方法,具有精确的语法和语义,并且便于机器自动检验与验证.TCSP是进程代数CSP的实时扩展,适合于规约实时系统带有时间约束的行为.提出一种基于进程代数规约生成SA模型的方法.首先建立了自然语言规约到SA模型的转换框架;然后使用时间通信顺序进程(TCSP)描述实时系统需求规约,通过建立TCSP到UML-RT的转换机制,从而实现进程代数规约到SA模型的转换;最后通过一个实例来验证该方法在实时软件建模过程中的有效性.实验分析表明通过该方法建立的UML-RT模型能够从整体上提高实时系统SA设计的可信性.     

一种自动的软件体系结构规约重写方法

在软件较高的抽象层次如软件体系结构,实施重构更有助于提高软件的易维护性,从而降低软件的维护成本。大量复杂的重构操作需要(半)自动化的支持。该文提出一种体系结构规约重写方法,将体系结构重构转换为接口重构和实现体重构2方面的规约重写,并给出规约重写基本操作规则。分析了实现体规约的重构操作,提出子构件提升操作、同级构件合并操作、跨级构件合并和构件分离合并操作4种基本操作。     

Agent系统软件体系结构形式化建模方法

基于Agent技术为复杂分布式问题提供了求解方法。软件体系结构是控制软件复杂性、提高软件系统质量、支持软件开发和复用的重要手段之一。软件体系结构设计可用于描述Agent与Agent之间的交互和组织结构的规划,因此Agent系统能从良好的体系结构设计中受益。该文整合了图表句法理论和层次谓词变迁网理论,提出一种形式化建模方法,从抽象层(架构)和实现层(动态行为)两方面来构建Agent系统的软件体系结构。模型具有可验证和追踪性,为Agent系统软件体系结构分析与评估提供了良好的基础。     

软件体系结构模型的形式化研究

用软件体系结构描述语言WRIGHT对三层C/S模型进行形式化描述,指出这种描述的优点以及软件体系结构模型形式化研究的重要性。     

形式化构件规约自动生成中的演化转换

基于软件体系结构的开发将是未来大型、复杂软件开发的主要技术,而构件是该方法的基础。形式化构件规约对构件的功能描述、分类和检索有重要意义。文中给出了一种用于形式化构件规约自动生成的转换方法即演化转换,对该方法的转换过程、转换规则提取、表示及主要转换算法进行了详细说明,并对规约的完整性和转换的正确性进行了探讨。最后,还对该方法的实现系统及其特点进行了简要介绍。演化转换能较好地控制转换粒度和跨度,对转换正确性和规约完整性也有一定的保证,在转换过程中实现了规约的垂直重用,使构造的模型和规约对需求变化有一定的适应性。     

面向对象软件体系结构的形式化模型

软件体系结构设计中的形式化方法，一直是软件工程领域中的研究热点。而在面向对象环境中如何对体系结构进行形式化，以精确描述其静态结构与动态交互行为，则一直未有好的解决办法。本文使用符号逻辑方法描述面向对象系统中的基本组成单元，并使用有限自动机建立面向对象体系结构的形式化模型。     

基于软件体系结构的Agent规约和演化

借助软件体系结构描述语言C2的表达能力,基于组件,连接体和体系结构配置3要素,研究适合于Agent规约和构造的组合方法,以软件体系结构的类型化理论为基础,探讨了基于子类型关系的Agent演化,用扩充关系表达有相互关联的不同类型的Agent之间的关系,通过为遗留代码定做包装器,领域翻译器以及相应的界面和约束,将非Agent实体迁移为Agent,相关案例说明结合组合,基于子类型关系的演化,扩充,迁移等方法,可以满足多Agent系统构造过程中Agent类型的多样性。     

软件体系结构模型的形式化研究

本文用软件体系结构描述语言WRIGHT对三层C／S模型进行形式化描述，指出这种描述的优点以及软件体系结构模型形式化研究的重要性。     

TFSP：一种分布式实时系统的形式化描述工具

Distributed Real Time Systems (DRTS) have very broad applications in space navigation, nuclear reaction,military affairs and industry department where the security and reliability requirement of the DRTS is very high.Thus, how to develop correct DRTS application systems is of vital importance. In this paper, first a formalized nota-tion system -Timed Finite State Processes (TFSP) is proposed to describe the complex dynamic behaviors of DRTS,then we describe a distributed real-time medirAl treatment system by Darwin Architecture language and TFSP.     

A Real-Time Discrete Event System Specification Formalism for Seamless Real-Time Software Development

We present a time domain extension of the hierarchical and modular discrete event specification (DEVS) formalism. This extension is important for establishing a seamless real-time software development framework. Formalisms help describe a system unambiguously. If formal models are implemented without any consistent frameworks, however, it is hard to guarantee that there is no semantic gap between models and codes. Real-Time DEVS, named RTDEVS, is an extension of DEVS that can be characterized in three perspectives: the real time execution of models, the addition of time interval functions, and the activity specification for each state. After analyzing a system, the framework based on RTDEVS helps to expand each model of the system for executing in a real-time environment. In order to support the RTDEVS formalism, we propose abstract executive concepts based on the abstract simulator concepts of the DEVS formalism. Also, we implement an RTDEVS execution engine, named DEVS Executive, which runs on real-time Mach.     

协议形式化开发环境的规范语言

LOTOS（languageoftemporalorderingspecification）是一种基于进程代数CCS的协议规范语言,面向协议验证,但它不能描述协议的某些性质．本文提出了一种LOTOS的扩充语言ELOTOS（extendedLOTOS）,它在LOTOS的基础上引入了异步通讯机制、时间描述、事件发生的随机性描述．     

网络协议设计中形式结构模型的创建方法研究

形式描述技术在协议设计中的应用是至关重要的和必不可少的,为形式规范确定一个合适的结构又是应用此技术的关键步骤,基于此文中重点研究了基于LOTOS技术的形式结构模型的创建方法。简要介绍了开发网络协议的形式描述技术、网络协议的结构概念、等级抽象和LOTOS描述规范风格。基于LOTOS技术,提出了网络协议开发过程中形式结构模型的创建原则和方法,此方法结合LOTOS语言特征,应用其描述规范风格,融协议结构、逐步改进和等级抽象为一体,简化了所开发协议的验证、测试和实现的复杂性。     

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

Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首先用时钟变量扩充线性时态逻辑,接着提出了一个方法——用带时钟变量的时态逻辑(LTLC)来扩充Object-Z。用LTLC扩充的Object-Z是一个模块化规格说明语言,是Object-Z语法和语义的最小扩充,其最大优点在于它能方便地描述和验证复杂的实时软件规格说明。     

Formal Specifications of User Requirements

There is a wide gap between informal requirements and a formal object-oriented specification. To help bridge this gap, we propose that a formal and executable user-centred model should be constructed initially. The user-centred model, which specifies the behaviour that the environment expects from the system, is expressed in terms of agent views and gives very early feedback to the requirements' capture process. Once the user-centred model has been validated with respect to the environment, it can be used as a step in the construction and validation of the formal object-oriented specification.     

A Contract-based Approach to Specifying and Verifying Safety Critical Systems

Light-weight formal method has been regarded as an important approach to development of component-based safety critical systems. The paper proposes an approach which can formally specify and verify the contract of static structure, dynamic behavior and refinement of component systems based on UML 2.0 superstructure. As results, the correctness of static contract can be obtained via type checking of interfaces and connectors. Dynamic contract can be verified through determining the cooperativeness of integrated components, whose contracts are depicted with interface protocol state machines and their semantics models, namely contract automata. The refinement relation between high level component and its implementation will be guaranteed through defining the alternating simulation between contract automata of components at different levels.     

分布实现完全LOTOS规范的转换方法

基于LOTOS规范语言,文章从系统功能规范出发,结合实际系统的分布特性,推导出符合实际系统结构的模块化规范的转换方法.用标注的完全LOTOS语言规范表达复杂的系统分布特性,研究了使用广播通信方式进行协同的、直接处理多模块划分的规范分解算法.     

Patterns for Timed Property Specifications

Patterns for property specification enable non-experts to write formal specifications that can be used for automatic model checking. The existing patterns identified in [Dwyer, M.B., G.S. Avrunin and J.C. Corbett, Property specification patterns for finite-state verification, in: FMSP '98: Proceedings of the second workshop on Formal methods in software practice (1998), pp. 7–15] allow to reason about occurrence and order of events, but not about their timing. We extend this pattern system by patterns related to time. This allows the specification of real-time requirements.     

一种嵌入式实时系统软件的形式化开发方法

领域特征突出的嵌入式实时系统软件开发,既需要严格地保证可靠性又要充分反映实时和交互行为特征,针对这种需要,该文提出了一种从需求分析到体系结构建模直至使用组件技术实现软件的形式化开发方法。文章在介绍了目前的各软件工程领域以及各软件开发阶段中的形式化模型和工具的现状和特点后,引入需求分析的模型和体系结构建模的描述语言,分析其长处和不足,最后对该方法与移动组件结合的前景进行了展望。