基于实时语言和面向方面的形式化开发方法

面向方面方法和实时语言特性应用于实时软件开发工程，将降低实时软件开发的复杂性，而形式化方法将提升系统的可信度。该文提出的一种面向方面的实时软件开发方法AOSDBRTL，它基于经面向方面扩展的形式化方法AO RT Z，在编码阶段应用实时语言PEARL，实现了软件开发各个阶段对面向方面的无缝支持。     

面向方面的实时系统形式化开发方法

实时系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要如面向方面和基于组件的软件工程方法的支持,同时实时系统的可信性要求采用形式化方法来开发实时系统。本文试图建立一种面向方面的实时系统形式化开发方法,这种方法对RT—Z进行了面向方面和面向部件的扩展,并通过实时组件模型在需求和设计阶段提供了对基于部件的系统开发方法(CBSD)和面向方面的系统开发方法(AOSD)的支持。本文给出了面向方面的实时Z(AO—RT—Z)的组件模型的框架结构、语法要求、方面的联结和功能接口和非功能接口的定义,重点讨论并证明了面向方面的实时Z(AO—RT—Z)作为规格描述语言的健全性。     

异构的动态分布式实时系统的面向方面的形式化方法

形式化方法是在严格的数学基础上建立的．具有精确数学含义的科学研究和验证方法。异构的动态分布式系统的开发过程是非常复杂的．不能用一种开发方法进行分析、设计和实现。由于形式化方法具有严谨、可数学分析和证明等特性,可以根据系统开发的不同方面采用不同的形式化语言进行实现．然后再把这些方面编织到系统中去。     

面向方面分布式系统形式化规格说明语言

分布式系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要面向方面软件工程方法的支持,而形式化方法能保证分布式系统的正确性。本文对分布式规格说明语言Ocsid进行了面向方面的扩展,讨论了面向方面的Ocsid的框架结构、语法要求、方面的联结和功能接口。定义了面向方面的Ocsid规格说明语言中叠加和组合的形式化描述,该形式化描述覆盖了各个精化阶段,使精化体系的各个独立视点被协调地组合,并能形式化地验证规格说明的时态属性和系统行为。本文的工作针对的是分布式系统的形式化规格说明,提出了面向方面Ocsid的形式基础和方面扩展,其基本思想同样适用于更一般的情况。     

实时系统的方面开发方法和应用模型

结合领域工程的方法,在某个领域内建立面向方面的软件开发AOSD框架是值得探讨的简单可行的方法,探讨了在实时系统开发过程中支持面向方面方法的几个关键问题及解决方案,提出了一种实时领域面向方面开发框架,降低了实时软件开发的复杂性,提升了系统的可信度,同时实现了实时软件开发各个阶段的无缝连接。     

Z实时扩展及基于多视点的应用模式

RT—Z是由Z和经实时扩展的通信顺序进程timed CSP集成的用以描述实时系统的规格说明语言,它将Z对状态描述的优点和timed CsP对时序关系和并发描述的优点相结合,具有强大的描述能力;而基于时序转化系统的Z扩展适合描述系统状态的转化。给出了Z实时扩展的分类原则并从讨论了其应用特点,最后在分析RT—Z的语义集成的基础上提出了Z实时扩展的多视点应用模式。     

一种基于CSP的面向方面状态图形式化描述方法

面向方面通过分离关注点解决软件系统中的横切问题,通过扩展UML可实现对面向方面的建模。本文利用UML的扩展机制将方面加入状态图中,描述了状态图中的方面与核心组件以及方面之间的编织,然后利用进程代数的形式化语义描述了扩展后的UML状态图,克服了扩展UML描述状态图的缺乏形式化动态语义,不利于对模型进行形式化验证和证明的缺
点。最后,以ATM自动取款机为例验证了基于CSP的面向方面状态图形式化描述的有效性。     

形式化语言B的面向方面编程扩充

借助传统编程语言的面向方面编程扩充——AspectJ/AspectC＋＋的技术经验,提出形式化语言B的AOP扩充机制AspectB。分析了B语言针对AOP扩充在连接点范围及正确性验证方面的制约,提出连接点的范围必须限制在IMPLEMENTATION组件中,方面代码的正确性验证必须考虑连接点上下文所涉及的不变性条件。以一个简单图形编辑器为例,在B语言环境中描述面向方面编程的核心概念——连接点、连接点集合、建议代码、方面。     

面向方面软件重构等价性形式化证明方法

软件重构在不改变程序行为的情况下通过对代码进行小的改进以提升设计,使之更容易理解和维护,面向方面的程序设计是软件开发的新技术,为了有效实施面向方面的软件重构,需要开发者识别面向方面程序的转化规则。然而,由于使用的AOP语言没有形式化的语义定义,难以确认转化和重构的程序运行行为。本文对MCI操作语义的面向方面的扩展使之支持程序的方面特征的描述,定义了两个程序的观测等价,讨论了AspectJ的形式语义模型的建立,在MCI的语义下形式化地精确证明了Add Before-executing编程规则的观测等价性,其基本原理和方法可以适用于其他规则的证明,通过上述工作提出了面向方面重构的程序和它的面向对象程序原型等价性的证明方法。     

面向方面在实时系统中间件中的应用

实时系统中间件存在着分布性、实时性、容错性、安全控制、性能分析、日志记录等非功能的横切关注点,基于面向方面的中间件构件技术就是要把这些非功能的要求从中问件的核心功能中分离出,形成非功能方面,运用面向方面的编程技术可实现中间件核心功能关注点和非功能的横切关注点的并行设计与开发,这增加了中间件设计的模块性、可扩展性和可维护性.文中提出了采用面向方面的编程思想,重构基于Java的RMI(Renote Method Invocation)分布式框架,实现实时系统中间件的分布性.     

The formal definition of a real-time language

Summary This paper presents the formal definition of TOMAL (Task-Oriented Microprocessor Applications Language), a programming language intended for real-time systems running on small processors. The formal definition addresses all aspects of the language. Because some modes of semantic definition seem particularly well-suited to certain aspects of a language, and not as suitable for others, the formal definition employs several complementary modes of definition.The primary definition is axiomatic and is employed to define most statements of the language. Simple, denotational (but not lattice-theoretic) semantics complement the axiomatic semantics to define type-related features, such as binding of names to types, data type coercions, and evaluation of expressions. Together, the axiomatic and denotational semantics define all features of the sequential language. An operational definition is used to define real-time execution, and to extend the axiomatic definition to account for all aspects of concurrent execution. Semantic constraints, sufficient to guarantee conformity of a program with the axiomatic definition, can be checked by analysis of a TOMAL program at compilation.     

Object modelling and formal specification during real-time system development

Object oriented techniques promote understanding of requirements leading to flexible and extendible designs. The use of formal specification techniques ensures a complete understanding of system requirements and provides sound foundations for subsequent testing and verification. This paper describes the use of the Z and Timed CSP formal specification techniques to support object modelling during real-time system development. Relationships between class attributes are specified within the corresponding Z schemas and inheritance relationships between classes are formally specified using the schema extension mechanism of Z. Z is used to specify the domain types of the attributes of classes identified during object oriented analysis and design. Z is also used to produce model based specifications of the methods within classes that are specified informally during functional analysis. Dynamic analysis identifies events, states and temporal relationships between events. Timed CSP is used to formally specify this information as well as timing information that is necessary during real-time system development.     

AOSD方法及其在分布式系统开发中的应用

在包含诸多横切关注点的复杂软件系统开发中,面向对象软件开发方法（OOSD）存在无法克服的缺陷。在分析面向对象软件开发方法对横切关注点处理的缺陷的基础上,讨论了面向方面软件开发（aspect-oriented software development,AOSD）方法及其在复杂系统开发中的优越性,提出了一种面向方面软件开发方法的过程模型,介绍了面向方面软件开发方法在分布式系统开发中的应用。     

Integrating structured OO approaches with formal techniques for the development of real-time systems

The use of formal methods in the development of time-critical applications is essential if we want to achieve a high level of assurance in them. However, these methods have not yet been widely accepted in industry as compared to the more established structured and informal techniques. A reliable linkage between these two techniques will provide the developer with a powerful tool for developing a provably correct system. In this article, we explore the issue of integrating a real-time formal technique, TAM (Temporal Agent Model), with an industry-strength structured methodology known as HRT-HOOD. TAM is a systematic formal approach for the development of real-time systems based on the refinement calculus. Within TAM, a formal specification can be written (in a logic-based formalism), analysed and then refined to concrete representation through successive applications of sound refinement laws. Both abstract specification and concrete implementation are allowed to freely intermix. HRT-HOOD is an extension to the Hierarchical Object-Oriented Design (HOOD) technique for the development of Hard Real-Time systems. It is a two-phase design technique dealing with the logical and physical architecture designs of the system which can handle both functional and non-functional requirement, respectively. The integrated technique is illustrated on a version of the mine control system.     

Object-oriented specification and formal verification of real-time systems

An object-oriented approach for specification and verification of real-time systems is described in this paper. It is motivated by taking advantage of object-oriented techniques to produce real-time software that is easy to understand, maintain, and reuse. The approach specifies the structural, behavioral, and control aspects of objects in one model with a textual representation as well as a graphical representation. For ease to comprehend and use, the model encapsulates object states and allows an analyst to focus on specifying object operations one at a time. System behavior from individual objects can be deduced and analyzed. For safety considerations, the approach supports specification of failures to object behavior and their resultant faults. The approach also supports modeling of timed temporal constraints for specifying and verifying desirable real-time properties. An object timed temporal logic OTTL is defined for expressing the syntax and semantics of these constraints. Decision procedures for their verification are also presented.     

An action-based formal model for concurrent real-time systems

Action systems are a formalism for representing concurrent behaviours, based on interleaved atomic actions. We show how this model can be used to represent time-consuming, pre-emptible actions with real-time constraints. A development procedure is described which captures the steps programmers typically undertake in the design of real-time multi-tasking systems.