Abstract We describe a toolset, consisting of a graphical editor, a simulator, and an assertion checker, for prototyping real‐time systems that are specified as Communicating Real‐Time State machines (CRSMs). CRSMs are timed state machines that communicate synchronously over unidirectional channels. The system behavior of CRSMs is characterized by a time‐stamped trace of communication events. Safety and timing assertions on the trace of communication events are expressed in a notation based on Real‐Time Logic. We illustrate the simulator and assertion checker by specifying a traffic‐light controller and other real‐time systems. There are two main contributions in this work: first, the prototyping environment serves as a validation of the model, the execution algorithm and paper design of example CRSMs, demonstrating that the ideas are realizable and potentially useful. Secondly, the paper presents a novel and useful method of specifying safety and timing properties, and checking them during simulation.

Communicating real-time state machines (CRSMs), a complete and executable notation for specifying concurrent real-time systems including the monitored and controlled physical environment, are introduced. They are essentially state machines that communicate synchronously in a manner much like the input-output in Hoare's CSP. In addition, CRSMs have a novel and small set of facilities for describing timing properties and accessing real time. The author defines the CRSM language, gives many examples of its use in requirements specification, outlines an algorithm for executing or simulating CRSMs, introduces some techniques for reasoning about the specifications, and discusses some open problems and issues.>

Abstract A model based on simple, unadorned processes and abstract data types has been proposed for the design and implementation of real‐time systems. We describe our generally successful experiences in using this model for the construction of a real‐time operating system kernel containing services for process control, synchronization, time and input‐output. Our work and results focus on the usefulness of the scheme for designing modules at hardware/software interfaces, for predicting deterministic timing behaviour, and for software development.

A timing tool has been implemented for a subset of C as an initial experiment in validating a methodology for predicting the deterministic execution times of programs. The tool is based on formal timing schema that are defined for each source level construct (procedures, statements, expressions). The tool accepts a program and bounds for each loop, and produces predictions for best and worst case execution times. Two versions of the tool were written, using two extremes of granularity for the atomic elements of the timing schema. Within the constraints of the target architecture and compiler, measured execution times for a variety of simple constructs and programs agree with times predicted by the tool. The implementation decomposes naturally into a system-independent part, which is believed to be determined by the 'timing semantics' of the language, and a lower-level system-dependent portion. The experiments validate the general timing schema approach but also point out a number of problems and possible refinements.>

A methodology for specifying and providing assertions about time in higher-level-language programs is described. The approach develops three ideas: the distinction between, and treatment of, both real-time and computer times; the use of upper and lower bounds on the execution times of program elements; and a simple extension of Hoare logic to include the effects of the passage of real-time. Schemas and examples of timing bounds and assertions are presented for a variety of statement types and programs, such as conventional sequential programs including loops, time-related statements such as delay, concurrent programs with synchronization, and software in the presence of interrupts. Examples of assertions that are proved include deadlines, timing invariants for periodic processes, and the specification of time-based events such as those needed for the recognition of single and double clicks from a mouse button.>

Periodic processes are major parts of many real-time embedded computer applications. The programming language Ada permits programming of simple periodic processes, but it has some serious limitations: producing Ada programs with real-time performance comparable to that of programs produced to date using traditional cyclic executives requires techniques that are specific to one machine or compiler. The authors present and evaluate the cyclic executive model for controlling periodic processes. The features and limitations of Ada for programming cyclic executive software are discussed and demonstrated, and some practical techniques for circumventing Ada problems are described.>

Flow expressions describe sequential and concurrent flows of entities, such as control, messages, commands, jobs, and resources, through system software components, such as programs, procedures, modules, and processes. They consist of regular expressions extended with cyclic and interleaving operators and a synchronization facility. The language of flow expressions is defined and some of its formal properties are presented. Applications are exhibited in the modeling of concurrent programs, the description of operating system architectures, the specification and solution of synchronization problems, the flow and description of command languages, and in systems analysis and verification.

Abstract This paper describes a nucleus for controlling process interaction in multiprogramming systems. The nucleus has three components: a set of primitive operations and data structures for the management of processes and resources, a library of service routines for implementing a variety of resource management strategies and facilities for cleanly handling all input‐output and interrupts. The process management component is straightforward, but the resource facilities are novel in permitting the dynamic definition and control of classes of real or virtual resources. Resources are considered to be anything on which a process can be blocked and consequently encompass consumable (message‐like) as well as conventional, re‐usable objects. Applications of the nucleus as well as some implementation details are also presented.

A syntax-directed picture analysis system based on a formal picture description scheme is described. The system accepts a description of a set of pictures in terms of a grammar generating strings in a picture description language; the grammar is explicitly used to direct the analysis or parse, and to control the calls on pattern classification routines for primitive picture components. Pictures are represented by directed graphs with labeled edges, where the edges denote elementary picture components and the graph connectivity mirrors the picture component connectivity; blank and don't care “patterns” allow the description of simple relations between visible patterns. The bulk of the paper is concerned with the picture parsing algorithm which is an n -dimensional analog of a classical top-down string parser, and an application of an implemented system to the analysis of spark chamber film. The potential benefits of this approach, as demonstrated by the application, include ease of implementation and modification of picture processing systems, and simplification of the pattern recognition problem by automatically taking advantage of contextual information.