实时软件设计方法的发展趋势

介绍实时程序设计方法学的两个基本方面:实时程序设计语言和实时程序的规范说明及形式化验证,讨论实时程序设计的基本特点和与一般程序设计的不同之处,程序层次的实时性包括静态的时间限制表达和动态的时间限制维护,程序规范层次的实时性包括建立规范说明模型和形式化证明.     

可视程序设计语言形式化规范的研究

在计算机领域引入程序可视化技术，把图形技术融进程序设计中，其目的在于减少人与机器交流的故障。首先简述可视程序设计的基本概念，然后介绍可视程序设计语言的形式化描述，如图形系统的形式化规范，图标操作符，图标谗句的语法与语义分析描述。     

一个形式化的程序设计方法及其实验系统

本文提出了一个形式化的程序设计方法,即以循环不变式为指导,运用程序变换规则从程序说明逐步地形式化地推争程序。生成的程序对于输入说明和输出说明是正确的。我们使用正则自动机作为程序的算法模型。这种算法模型具有通用性,它表示的程序可以等价地变换为某种程序设计语言的程序文本,如FORTRAN或PASCAL程序。 文中提出了“程序语句生成器”的概念及有关的程序变换规则,论述了利用循环不变式自动构造循环程序的原则和方法。文章还扼要介绍了应用这个方法的一个小型自动程序设计实验系统APES-82。     

基于面向对象结构的AI基础语言

本文分析了面向对象的程序设计方法,由此规范了面向对象的AI 程序设计的思想。根据这一思想,文章论述了基本面向对象结构的AI 基础语言的基本结构,并通过一例说明这一设计的特点。     

面向对象程序设计方法学与Ada

本文从现行功能性程序设计方法学的局限性论及面向对象程序设计方法学的实质,以及用该方法学进行程序设计的步骤,并有用Ada语言按此规范作设计的实例。面向对象程序设计方法学是现行功能性程序设计方法学的延伸和发展。用这这种规范开发的软件不仅适应并发、实时应用的要求,而且易于满足软件工程的规范。 Ada虽不是面向对象程序设计语言,但它的数据抽象和封装机制很适合于这种规范。从而,将面向对象程序设计方法学用于Ada程序设计,可以形成良好的程序设计风格。实际上,已经形成了Ada程序设计方法学。     

一类数组算法的演绎综合

1.引言演绎综合是一种形式化开发算法程序的方法,它从给定问题的一个易于理解、简洁明确的规范说明出发(规范说明表达了所要设计程序的目的),通过定理证明,程序变换,演绎推理等手段,形式化地推导出解决问题的正确算法或程序。算法程序演绎综合的基础     

程序设计方法学

本文目的旨在阐明程序设计的一些基本原理和方法。全文共分十二部分:第一至四部分的主要内容是程序结构分析,并由此熟悉本教程使用的面向教学的程序设计语言T的概貌。第五至九部分是本教程的重点,内容包括结构程序设计方法、过程和模块的设计方法、递归程序的设计方法等。第十至十二部分使用了比较形式化的方法进行讨论。内容有形式语义,程序的功能描述,程序推导和程序变换。最后还论述了研制程序设计工具和环境的意义。     

基于Petri网的嵌入式软件组件的实时性研究

根据嵌入式系统软件的特点和发展需求,设计了一种新的嵌入式软件组件模型SECOM,给出了模型的基本组成元素。同时,利用时间Petri网TPN建立一个TPN计时器timer,对该组件模型SECOM非功能性约束中的实时性进行建模与分析,形式化地验证了该组件的实时性。     

PASCAL过程蓝图

提出一种面向标准PASCAL语言的程序处理逻辑图形化表示法－PASCAL过程蓝图,这种工程化表示法支持逻辑和实现两个层次的程序抽象表示,是一种简单实用、容易理解、结构良好的程序设计工具。文中给出PASCAL过程蓝图的形式化模型、抽象逻辑结构图的图形表示方法,以及程序设计的基本过程。     

一种面向嵌入式实时软件的需求建模语言

针对嵌入式实时系统复杂动态交互行为和严格实时的领域特征，提出了一种软件需求规约语言RTRSM。该语言以扩充的层次并发有穷状态机HCA为核心，以支持合成的模板为基本组成单元．利用转换有效期和事件预定机制来描述时间限制，既具有较强的时间限制描述能力，又能自然而直接地支持交互行为的建模，可执行且具有良好的形式语义。给出了该语言的形式化语法，举例说明了其时间描述机制，并通过执行步算法和基于HCA项的结构化操作规则定义了该语言的形式化操作语义。     

基于对象的分布式实时系统调度模型研究

为了解决分布式实时系统有关分配和调度等问题，给出并用形式化方法描述了一种基于对象分布式实时系统调度的通用模型。该模型包括表示时限的绝对时间约束，表示周期属性的周期约束，表示各种前趋关系和同步要求的相对时间约束以及保证资源使用一致性的一致性约束，此外该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述系统实时的约束的不足，允许从方法和活动上描述所需的约束，降低了单一约束描述的繁杂程度，为了能够使用现有调度算法进行任务调度，讨论了约束转换的问题，给出了高层约束到底层约束的转换规则和相应的转换算法。     

基于对象分布式实时系统约束的一致性研究

在分布式实时系统中,时间约束规格的一致性是解决任务分配和调度等关键问题的必要前提。该文给出了一种基于对象分布式实时系统调度的通用模型,并对该模型进行了形式化描述。该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述系统实时约束的不足,允许从方法和活动上描述所需的约束,降低了单一约束描述的繁杂程度。为了解决使用该模型进行约束规格的一致性问题,该文给出了绝对时间约束、相对时间约束、一致性约束以及相对时间约束和一致性约束之间的一致性判定的必要条件。     

An Approach to Platform Independent Real-Time Programming: (2) Practical Application

In a previously published companion paper a method for extending programming languages with timing constructs was proposed. It was shown that the extension enables the construction of real-time programs that can be proven correct independently of the properties of the machine that is used for their execution. It also yields a strict division of system construction into two phases: (1) a platform-independent programming phase that includes the expression of timing requirements, and (2) an implementation phase where all platform dependencies are addressed. In this second paper the approach is illustrated using an example problem often quoted in the literature: the mine-pump system. The two mentioned phases are described in detail for this example. First, a program is obtained in a systematic way. Then, realizations of the program under various schemes for distribution and scheduling are considered and analyzed. A comparison with other approaches to real-time programming is given.     

An Approach to Platform Independent Real-Time Programming: (1) Formal Description

A method for extending programming languages with timing constructs is proposed. It enables the specification of timing constraints in programs. The approach is not language specific and the extension can be included in many existing programming languages. With the extension it is possible to write real-time program components that can be proven correct independently of the properties of the machine that is used for their execution. It therefore provides a similar abstraction from the execution platform as is normal in non-real-time programming. The presented approach distinguishes two phases in system construction: (1) a platform-independent programming phase that includes the expression of timing requirements, and (2) an implementation phase where all platform dependencies are addressed. The latter only differs from a normal compilation in the sense that a feasible schedule must be found to execute the program.     

基于构件的嵌入式实时软件建模与分析

嵌入式实时软件具有严格的时间要求,任何时间错误都可能造成重大的经济损失甚至导致灾难性的后果。因此,在软件开发早期,对其时间需求进行形式化的分析和验证是非常重要的。本文提出一种基于构件的嵌入式实时软件建模与分析方法,该方法不仅可以检测出需求模型中的时间冲突,有助于保证嵌入式实时软件时间约束的正确性,而且也也使得分析结果具有可复用、可扩展的优点。     

基于实时交通信息的车辆路径问题研究

石油化工企业的物流配送越来越成为降低成本、提高效率的1个重要环节,而车辆路径问题是其中的基础性问题。面对各种不确定性,动态随机车辆路径问题越来越成为有价值的研究方向,其关键在于实时交通信息的利用。本文研究了基于实时交通信息的单配送中心、有时间窗口约束的车辆路径问题,建立了混合整数规划模型,提出了利用实时速度估计信息的动态调度策略,并设计了带插入规则的节约算法。通过对标准benchmark问题进行仿真,验证了策略和算法的有效性。     

Expressing and Enforcing Timing Constraints in a Dynamic Real-Time CORBA System

Distributed real-time applications have presented the need to extend the Object Management Group's Common Object Request Broker Architecture (CORBA) standard to support real-time. This paper describes a Dynamic Real-Time CORBA system, which supports the expression and enforcement of end-to-end timing constraints as an extension to a commercial CORBA system. The paper also describes performance tests that demonstrate the system's ability to enforce expressed timing constraints.     

A sequential real-time refinement calculus

We present a comprehensive refinement calculus for the development of sequential, real-time programs from real-time specifications. A specification may include not only execution time limits, but also requirements on the behaviour of outputs over the duration of the execution of the program. The approach allows refinement steps that separate timing constraints and functional requirements. New rules are provided for handling timing constraints, but the refinement of components implementing functional requirements is essentially the same as in the standard refinement calculus. The product of the refinement process is a program in the target programming language extended with timing deadline directives. The extended language is a machine-independent, real-time programming language. To provide valid machine code for a particular model of machine, the machine code produced by a compiler must be analysed to guarantee that it meets the specified timing deadlines. Received: 27 September 1997 / 13 June 2000     

The Spring kernel: a new paradigm for real-time systems

A real-time operating system kernel, called the Spring kernel, that provides some of the basic support required for large, complex, next-generation real-time systems, especially in meeting timing constraints, is presented. The approach meets the need to build predictable yet flexible real-time systems. Most current real-time operating systems contain the same basic paradigms found in time-sharing operating systems and often use a basic priority-scheduling mechanism that provides no direct support for meeting timing constraints. Spring uses two criteria to classify tasks' interaction with and effects on the environment: importance and timing requirements. Implementation experience with Spring is described