Summary form only given. From the earliest days, designers of real-time systems have had to decide how to manage the hardware-level mechanisms (such as interrupts and multi-level priorities) that have been provided to share the computing resources between competing demands. One approach is to ignore these mechanisms and use software techniques to schedule program segments; another is to align the software architecture with the hardware features, e.g. by dividing a program into tasks or processes that are scheduled dynamically according to hardware priorities. These are two of many possible engineering solutions to the problem of meeting the timing constraints of real-time programs. Looked at more formally, the problem is to prove that the implementation of the program, by whatever method is chosen, can be shown to satisfy its timing specifications. This is altogether harder to accomplish. Proofs at the program level require guarantees of timing properties at lower levels.

Meta-model based development offers a promising way of managing the complexity of industrial scale software development by describing a system in terms of different 'views'. These views can then be described as instances of a single meta-model. Such views are usually not disjoint and it is essential that they are shown to be consistent. A weakness of meta-modelling tools is the lack of support for describing the behaviour of models, and this is central to demonstrating the consistency of views. We address this problem by combining meta-modelling with formal techniques for stating and verifying behavioural properties. In this paper, we describe a formalization of models and meta-models and show how this leads to automated procedures for consistency checking between views in an industrial software development framework.

Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs. This article shows how fault-tolerance, timing, and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be usedto combine these properties. It also permits results from scheduling theory to be interpreted and used within a formal proof framework. The notation and model are illustrated using a simple example.

Abstract Assume that a real-time program P T consisting of a number of parallel processes is executed on a system having a set Pr of processors which are shared between the processes by a real-time scheduler S T . Assume that P T must meet some timing deadlines. We show that such an implementation of P T can be represented as a transformationL( P T ) and that the deadlines of P T will be met if they are satisfied by the timing properties of the transformed program. The condition for feasibility of a real-time program executed under a scheduler is formalized and rules are provided for verification. The scheduler S T can be specified generically and applied to different programs, making it unnecessary to introduce low-level operations such as scheduling primitives into the programming language. Thus real-time program specification and Schedulability can be considered in the same framework and the timing properties of a program can be determined at the specification level. By separating the specification of the scheduler from that of the program, the feasibility of an implementation can be proved by considering a scheduling policy rather than its implementation details.

Abstract In this paper we describe how a program constructed for afault-freesystem can be transformed into afault-tolerantprogram for execution on a system which is susceptible to failures. A program is described by a set of atomic actions which perform transformations from states to states. We assume that a fault environment is represented by a programF. Interference by the fault environmentFon the execution of a programPcan then be described as afault-transformationℱ which transformsPinto a program ℱ(P). This is proved to be equivalent to the programP□PF, wherePFis derived fromPandF, and □ defines the union of the sets of actions ofPandFP. A recovery transformation ℛ transformsPinto a program ℛ(P) =P□Rby adding a set ofrecovery actions R, called arecovery program. If the system isfailstopand faults do not affect recovery actions, we have ℱ(ℛ(P))=ℱ(P)□R=P□PF□RWe illustrate this approach to fault-tolerant programming by considering the problem of designing a protocol that guarantees reliable communication from a sender to a receiver in spite of faults in the communication channel between them.

A real-time system is a concurrent computing system whose computations and actions must satisfy time constraints. Guaranteeing that such a system will meet its constraints can be viewed either in terms of an extended model of program correctness or as a problem of scheduling, e.g. establishing a feasible schedule. However, a crucial distinction between real-time and other concurrent programs is not merely that of time, but that the former must often execute on systems with limited resources. The authors give a short account of a limited resource semantics of program execution. The model can serve both as the basis for a formal specification system for real-time programs and to characterize real-time scheduling problems.>

There are two major performance issues in a real-time system where a processor has a set of devices connected to it at different priority levels. The first is to prove whether, for a given assignment of devices to priority levels, the system can handle its peak processing load without losing any inputs from the devices. The second is to determine the response time for each device. There may be several ways of assigning the devices to priority levels so that the peak processing load is met, but only some (or perhaps none) of these ways will also meet the response-time requirements for the devices. In this paper, we define a condition that must be met to handle the peak processing load and describe how exact worst-case response times can then be found. When the condition cannot be met, we show how the addition of buffers for inputs can be useful. Finally, we discuss the use of multiple processors in systems for real-time applications.

Recursive procedures have been extensively used for a long time, yet it was only in 1977 that Sokolowski gave a proof rule for the total correctness of recursive procedure calls. Unfortunately, even for simple programs his rule requires the use of complex predicates that encode information about the depth of recursion. Thus the rule can be very difficult to use for practical programs. In this paper we propose a new rule for this purpose. This rule makes use of the structure of the recursion which is discovered by carrying out an interval analysis of the procedure call graph in the proof. Proofs using this rule are simpler to carry out, and it is shown that Sokolowski's rule is in fact a special case of the new rule.

Abstract CCNPASCAL is a language derived from Pascal and Concurrent Pascal which has been used in the development of an operating system for a multiprocessor. This paper introduces some of the important features of the language and illustrates them with examples. The language provides mechanisms for interfacing separately compiled modules, for building abstractions of collections of resources and for efficient asynchronous communication.