时序Ada网的语言性质

在Ada网的基础上，利用时序Petri网为Ada任务程序建模，提出了时序Ada网的概念，利用时序Ada网，可以很好地反映Ada程序的公平性和原子性要求及描述程序的需求，规范，对时序Ada网的语言性质进行分析，结论表明时序Ada网所能接受的网语言能完整地刻画程序的动态行为和时序关系，有助于对程序性质的分析和验证。     

基于同步合成的结构复杂Petri网的行为描述

首先分析了一类结构简单的Petri网--S-网的语言性质,得到了它们的行为描述方法.拓展了Petri网同步合成的概念,证明了给定一个结构复杂的Petri网都可通过一组S-网的同步合成运算而得到,并给出了相应的求解算法.引入语言的同步交运算,分析了结构复杂的Petri网与其同步合成子网之间的行为关系,给出了结构复杂Petri网的行为描述算法,为利用网语言分析实际系统的行为特征提供了可靠的理论依据和方法.     

PN2MSVL:工作流网到MSVL的转换

现有的工作流网到程序设计语言的转换所生成的程序不仅可读性较差而且难以进行验证.针对这一情况,该文给出了一个工作流网到建模、仿真和验证语言(MSVL)的结构化转换工具PN2MSVL.该文首先定义了注释工作流网,然后以注释工作流网为中间模型,利用一组转换规则不断地压缩注释工作流网中的正规结构,最终得到MSVL程序.PN2MSVL生成的MSVL程序不仅具备更好的可读性,而且可以利用MSVL的支持工具MSV进行建模、仿真和验证.另外,该文通过一个应用实例详细地展示了PN2MSVL的执行过程,并通过大量的实验分析了PN2MSVL的可用性.     

基于Petri网语言的并发系统性质研究

给出Petri网弱活性（无死锁）与活性的两个语言刻画,讨论了同步合成Petri网的语言性质,基于Petri网语言,给出了判定Petri网活性的充分必要条件。同时研究了Petri网同步合成过程中活性保持问题,给出保持活性的充分必要条件。这些结果为讨论网的活性测试和控制提供了形式语言的方法。     

精炼工作流网的行为保持性质

本文定义了工作流网的精炼操作，研究了精炼工作流网的行为保持性质。结果表明精炼工作流网满足行为保持性质，即精炼工作流网的行为与原网和子网行为保持一致。在精炼工作流网行为保持性质的基础上，给出了基于原网语言和子网语言的精炼工作流网的语言刻画。本文结果有助于复杂工作流的设计、建模和验证。     

Ada中实时结构的Petri网建模与分析

本文从一般时间网出发，派生出一种简单时间网，并建模了延迟，分支选择，异步选择，优先权等Ada实时结构，特别是把优先权处理为一种时间特性，这样不仅扩充了Petri网在Ada中的建模能力，同时可以更加准确刻画Ada程序行为。     

随机Petri网的计算机仿真

本文研究了用计算机仿真技术作为随机Petri网的分析工具,并以通用仿真语言GPSS为例,讨论了随机Petri网与GPSS程序块之间的转换,并给出了应用实例。     

Ada编译中若干问题

Ada是由Jean D.Ichbiah等人代表美国国防部设计的一个新的系统程序设计语言,我们提出了Ada编译程序的一种结构,它分为(不依赖于机器的)前端部分与依赖于机器的后端部分。文章讨论了解决前端设计某些问题的若干方法。最后简要地介绍了中间语言DIANA,它是专门为表示Ada程序的中间形式而设计的。     

分布式Ada语言系统的实现

基于Ada 95参考手册附录E“分布式系统”中的思想,提出了实现分布式Ada语言系统的一些概念和设计思想,并给出了实现分区通信子系统的具体方案.在此基础上,通过一些前置处理,并利用已实现的分区通信子系统的接口,实现了分布式Ada语言系统.最后通过一个实例,具体介绍了分布式Ada语言系统的程序设计方法.     

基于Petri网的CSP并发系统验证技术研究

通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri 网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。     

Towards complexity metrics for Ada tasking

Using Ada as a representative distributed programming language, the author discusses some ideas on complexity metrics that focus on Ada tasking and rendezvous. Concurrently active rendezvous are claimed to be an important aspect of communication complexity. A Petri net graph model of Ada rendezvous is used to introduce a rendezvous graph, an abstraction that can be useful in viewing and computing effective communication complexity     

Adam: An Ada-based language for multiprocessing

Adam is a high-level language for parallel processing. It is intended for programming resource scheduling applications, in particular supervisory packages for run-time scheduling of multiprocessing systems. An important design goal was to provide support for implementation of Ada and its run-time environment. Adam has been used to implement Ada task supervision and also as a high-level target language for compilation of Ada tasking. Adam provides facilities corresponding to the Ada sequential constructs (including subprograms, packages, exceptions, generics). In addition, it provides specialized module constructs for implementation of packages that may be shared between parallel processes, and new predefined types for scheduling. The parallel processing constructs of Adam are more primitive than Ada tasking. Strong restrictions are enforced on the ways in which parallel processes can interact. A compiler for Adam has been implemented in MacLisp on DEC PDP-10 computers. Runtime support packages in Adam for scheduling (on a single CPU) and I/O are also provided. The compiler contains a library manipulation facility for separate compilation. The Adam compiler has been used to build an Ada compiler for most of the July 1980 Ada, including task types and rendezvous constructs. This was achieved by implementing the translation of Ada tasking into Adam parallel processing as a preprocessor to the Adam compiler. This present Ada compiler, which has been operational since December 1980, uses a procedure call implementation of tasking. It can be easily modified to other implementations. Compilation of Ada tasking into a high-level target language such as Adam facilitates studying questions of correctness and efficiency of various compilation algorithms, and code optimizations specific to tasking, e.g. elimination of unnecessary threads of control. This paper gives an overview of Adam and examples of its use. Emphasis is placed on the differences from Ada. Experience using Adam to build the experimental Ada system is evaluated. Design of a run-time supervisor in Adam is discussed in detail.     

Detection of Ada static deadlocks using Petri net invariants

A method is presented for detecting deadlocks in Ada tasking programs using structural; and dynamic analysis of Petri nets. Algorithmic translation of the Ada programs into Petri nets which preserve control-flow and message-flow properties is described. Properties of these Petri nets are discussed, and algorithms are given to analyze the nets to obtain information about static deadlocks that can occur in the original programs. Petri net invariants are used by the algorithms to reduce the time and space complexities associated with dynamic Petri net analysis (i.e. reachability graph generation)     

Verifying general safety properties of Ada tasking programs

The isolation approach to symbolic execution of Ada tasking programs provides a basis for automating partial correctness proofs. The strength of this approach lies in its isolation nature; tasks are symbolically executed and verified independently, and then checked for cooperation where interference can occur. This keeps the verification task computationally feasible and enhances its compositionality. Safety, however, is a more appropriate notion of correctness for concurrent programs than partial correctness. The author shows how the isolation approach to symbolic execution of Ada tasking program supports the verification of general safety properties. Specific safety properties that are considered include mutual exclusion, freedom from deadlock, and absence of communication failure. The techniques are illustrated using a solution to the readers and writers problem     

ARTK-M2: A kernel for Ada tasking requirements: An implementation and an automatic generator

A run-time kernel, ARTK-M2, supporting Ada tasking semantics is discussed; full support for task creation, synchronization, communication, scheduling, and termination is provided, together with all options of the Ada rendezvous. An implementation in Modula-2 is presented and a method for automatically translating Ada programs into semantically equivalent Modula-2 programs with corresponding kernel calls is introduced. A parser generator and an attribute grammar were used for the automatic translation. A subset of the Ada Compiler Validation Capability was processed to test the implementation and to illustrate the translation mechanism. The kernel is applicable to the study of real-time control systems; it can also serve as a baseline for studying implementation alternatives of Ada concepts, such as new scheduling algorithms, and for analysing new language constructs. Work is under way to implement some of the changes to the Ada tasking model being proposed as a result of the language revision (Ada9X). Finally, through proper extensions, ARTK-M2 can form an integral part of programming tools such as an Ada compilation system and a distributed kernel for multi-processing environments.     

Design and implementation of a Petri net based toolkit for Adatasking analysis

The use of Petri nets for defining a general static analysis framework for Ada tasking is advocated. The framework has evolved into a collection of tools that have proven to be a very valuable platform for experimental research. The design and implementation of tools that make up the tasking-oriented toolkit for the Ada language (TOTAL) are defined and discussed. Modeling and query/analysis methods and tools are discussed. Example Ada tasking programs are used to demonstrate the utility of each tool individually as well as the way the tools integrate. TOTAL is divided into two major subsystems, the front-end translator subsystem (FETS) and the back-end information display subsystem (BIDS). Three component tools that make up FETS are defined. Examples demonstrate the way these tools integrate in order to perform the translation of Ada source to Petri-net format. The BIDS subsystem and, in particular, the use of tools and techniques to support user-directed, but transparent, searches of Ada-net reachability graphs are discussed     

Monitoring for Deadlock and Blocking in Ada Tasking

We present a deadlock monitoring algodrithm for Ada tasking programs which is based on transforming the source program. The transformations introduce a new task called the monitor, which receives information from all other tasks about their tasking activities. The monitor detects deadlocks consisting of circular entry calls as well as some noncircular blocking situations. The correctness of the program transformations is formulated and proved using an operational state graph model of tasking. The main issue in the correctness proof is to show that the deadlock monitor algorithm works correctly without having simultaneous information about the state of the program. In the course of this work, we have developed some useful techniques for programming tasking applications, such as a method for uniformly introducing task identifiers. We argue that the ease of finding and justifying program transformations is a good test of the generality and uniformity of a programming language. The complexity of the full Ada language makes it difficult to safely apply transformational methods to arbitrary programs. We discuss several problems with the current semantics of Ada's tasks.     

Real-time interrupt handling in Ada

The Ada? programming language defines the semantics of interrupt handling as part of the tasking mechanism, making it possible to construct implementation-independent interrupt handlers. However, for the Ada mechanism to be effective, an implementation must provide support not specified by the Ada standard, such as for initializing hardware interrupting devices, handling unexpected interrupts and optimizing for real-time performance constraints. This paper analyses some of the constraints that efficient interrupt support places on an implementation. It develops a model for the interaction between interrupt hardware and Ada tasks and describes optimizations for Ada interrupt handlers. Implementation issues, including task priorities and task termination for interrupt handlers, are discussed in detail.     

Experience acquiring and retargeting a portable Ada compiler

A technique for implementing Ada with reasonable effort on a piece of non-standard hardware is described. The target machine is a single processing element in an experimental multiprocessor based on NS32000. A portable Ada front-end compiler was used for retargeting, and the process of acquiring and evaluating the front end is described. Based on this experience, comments on the validation, quality and efficiency of Ada compilers are given, along with a detailed overview of the resultant system. The Ada system was built from scratch on the bare hardware. It has three main components: a code generator, a run-time system and an Ada kernel. The code generator is table driven and generates symbolic NS32000 assembler. This code is then assembled and linked by commercially available components. The run-time system and the kernel are implemented in assembly language and Concurrent Euclid and handle tasking, exceptions and scheduling. The result is a complete Ada implementation.