Search

This paper defines an algorithm for predicting worst-case and best-case execution times, and determining execution-time constraints of control-flow paths through real-time programs using their partial correctness semantics. The algorithm produces a linear approximation of path traversal conditions, worst-case and best-case execution times and strongest postconditions for timed paths in abstract real-time programs. Also shown are techniques for determining the set of control-flow paths with decidable worst-case and best-case execution times. The approach is based on a weakest liberal precondition semantics and relies on supremum and infimum calculations similar to standard computations from linear programming and Presburger arithmetic. The methodology is applicable to any executable language with a predicate transformer semantics and hence provides a verification basis for both high-level language and assembly code execution-time analysis.

We present an abstract model of the leader election protocol used in the IEEE 1394 High Performance Serial Bus standard. The model is expressed in the probabilistic Guarded Command Language . By formal reasoning based on this description, we establish the probability of the root contention part of the protocol successfully terminating in terms of the number of attempts to do so. Some simple calculations then allow us to establish an upper bound on the time taken for those attempts.

The refinement calculus is a well-established theory for translating specifications to program code. Recent research has extended the calculus to handle real-time requirements and we have developed an interactive support tool based on these extensions. Via a case study, this paper shows how the tool helps the programmer by supporting the many forms of variables used in the theory. These include simple state variables as in the untimed calculus, timed-trace variables that model the evolution of properties over time, and auxiliary variables that exist to support formal reasoning only.

The management of risks in business processes has been a subject of active research in the past few years. Many benefits can potentially be obtained by integrating the two traditionally-separated fields of risk management and business process management, including the ability to minimize risks in business processes (by design) and to mitigate risks at run time. In the past few years, an increasing amount of research aimed at delivering such an integrated system has been proposed. However, these research efforts vary in terms of their scope, goals, and functionality. Through systematic collection and evaluation of relevant literature, this paper compares and classifies current approaches in the area of risk-aware business process management in order to identify and explain relevant research gaps. The process through which relevant literature is collected, filtered, and evaluated is also detailed.

When developing multitasking real-time systems, schedulability tests are used to formally prove that a given task set will meet its deadlines. A wide range of such tests have appeared in the literature. This tutorial acts as a guide to the major tests available for preemptive multitasking applications.

Developing concurrent real-time programs is one of computer science's greatest challenges. Not only is such software expensive to manufacture, but its role in safety-critical systems demands that it be correct. Formal methods of program specification and refinement could strengthen the mathematical precision used to develop such software. Nevertheless, formalisms that embrace both real-time and concurrency requirements are only just emerging. The Quartz method treats time and functional behavior with equal importance in the development process. The authors argue that by modeling program development in a unified framework, we can increase our confidence in the correctness of real-time concurrent code.

A novel m-ary tree-based approach is presented to solve asset management decisions which are combinatorial in nature. The approach introduces a new dynamic constraint-based control mechanism which is capable of excluding infeasible solutions from the solution space. The approach also provides a solution to the challenges with ordering of assets decisions.

Linear assets are engineering infrastructure, such as pipelines, railway lines, and electricity cables, which span long distances and can be divided into different segments. Optimal management of such assets is critical for asset owners as they normally involve significant capital investment. Currently, Time Based Preventive Maintenance (TBPM) strategies are commonly used in industry to improve the reliability of such assets, as they are easy to implement compared with reliability or risk-based preventive maintenance strategies. Linear assets are normally of large scale and thus their preventive maintenance is costly. Their owners and maintainers are always seeking to optimize their TBPM outcomes in terms of minimizing total expected costs over a long term involving multiple maintenance cycles. These costs include repair costs, preventive maintenance costs, and production losses. A TBPM strategy defines when Preventive Maintenance (PM) starts, how frequently the PM is conducted and which segments of a linear asset are operated on in each PM action. A number of factors such as required minimal mission time, customer satisfaction, human resources, and acceptable risk levels need to be considered when planning such a strategy. However, in current practice, TBPM decisions are often made based on decision makers’ expertise or industrial historical practice, and lack a systematic analysis of the effects of these factors. To address this issue, here we investigate the characteristics of TBPM of linear assets, and develop an effective multiple criteria decision making approach for determining an optimal TBPM strategy. We develop a recursive optimization equation which makes it possible to evaluate the effect of different maintenance options for linear assets, such as the best partitioning of the asset into segments and the maintenance cost per segment.

Electronic Health Record systems are being introduced to overcome the limitations associated with paper-based and isolated Electronic Medical Record systems. This is accomplished by aggregating medical data and consolidating them in one digital repository. Though an EHR system provides obvious functional benefits, there is a growing concern about reliability trust (trustworthiness) of Electronic Health Records. Security requirements such as confidentiality, integrity, and availability can be satisfied by traditional data security mechanisms. However, measuring data trustworthiness is an issue that cannot be solved with traditional mechanisms, especially since degrees of trust change over time. In this chapter, a Medical Data Trustworthiness Assessment model to assist an EHR system to validate the trustworthiness of received/stored medical data based on who entered the data and when is presented. The MDTA model uses a statistical approach that depends on the observed experiences available to the EHR system. In order to provide an accurate trustworthiness estimate for historical medical data, a time scope around the time when the data was entered was used. This scope enables the model to capture the dynamic behavior of the data entry agent’s trustworthiness. To conduct this assessment medical metadata is used to extract information about the medical data sources (e.g. timestamps, and the identities of healthcare agents and medical practitioners) and, thereafter, this information is used in a statistical process to derive a trustworthiness value for the medical data. The result can then be expressed in the displayed health record by manipulating the EHR’s metadata to alert the medical practitioner to possible trustworthiness problems.

Linear (or continuous) assets are engineering infrastructure that usually spans long distances and can be divided into different segments, all of which perform the same function but may be subject to different loads and environmental conditions. Typical linear assets include railway lines, roads, pipelines and cables. How and when to renew such assets are critical decisions for asset owners as they normally involves significant capital investment. Through investigating the characteristics of linear asset renewal decisions and identifying the critical requirements that are associated with renewal decisions, we present a multi-criteria decision support method to help optimise renewal decisions. A case study that concerns renewal of an economiser’s tubing system in a coal-fired power station is adopted to demonstrate the application of the method. Although the paper concerns a particular linear asset decision type, the approach has broad applicability for linear asset management generally.

Optimal Asset Maintenance (AM) decisions are imperative for efficient asset management. Decision Support Systems (DSSs) are often used to help asset managers make maintenance decisions, but high quality decision support must be based on sound decision-making principles. For long-lived assets, a successful AM decision-making process must effectively handle multiple time scales. For example, high-level strategic plans are normally made for periods of years, while daily operational decisions may need to be made within a space of mere minutes. When making strategic decisions, one usually has the luxury of time to explore alternatives, whereas routine operational decisions must often be made with no time for contemplation. In this paper, we present an innovative, flexible decision-making process model which distinguishes meta-level decision making, i.e. deciding how to make decisions, from the information gathering and analysis steps required to make the decisions themselves. The new model can accommodate various decision types. Three industrial cases are given to demonstrate its applicability.

Real-time networked control systems (NCSs) over data networks are being increasingly implemented on a massive scale in industrial applications. Along with this trend, wireless network technologies have been promoted for modern wireless NCSs (WNCSs). However, popular wireless network standards such as IEEE 802.11/15/16 are not designed for real-time communications. Key issues in real-time applications include limited transmission reliability and poor transmission delay performance. Considering the unique features of real-time control systems, this paper develops a conditional retransmission enabled transport protocol (CRETP) to improve the delay performance of the transmission control protocol (TCP) and also the reliability performance of the user datagram protocol (UDP) and its variants. Key features of the CRETP include a connectionless mechanism with acknowledgment (ACK), conditional retransmission and detection of ineffective data packets on the receiver side.

Linear (or continuous) assets such as railway lines, roads, pipelines and cables are essential in modern society. They play an important socioeconomic role and thus need to be maintained in a way that guarantees their reliability. Linear assets usually span long distances and can be divided into different segments, all of which perform the same function but may be subject to different loads and environmental conditions. Linear assets are usually well-engineered, long-lived assets. As a result, when conducting a reliability analysis, we often only have sparse right-censored failure records, as the majority of segments have not yet failed. Furthermore, many existing linear assets were built decades ago, and their failure and maintenance histories have not been recorded in detail until very recently, leading to a left-censored failure dataset. In addition to having incomplete failure data, linear assets, over their life spans, often present multiple failure characteristics and follow mixed failure distributions, typically a combination of exponential and Weibull distributions. A model that can effectively address these three issues has yet to be developed. In this paper, we present a hazard based predictive method to meet this need. Initially, a training hazard dataset is built up based on the available, incomplete historical failure data. This is then used to develop a parametric hybrid empirical hazard model which is finally used for reliability analysis and prediction.

In cloud computing, resource allocation and scheduling of multiple composite web services is an important and challenging problem. This is especially so in a hybrid cloud where there may be some low-cost resources available from private clouds and some high-cost resources from public clouds. Meeting this challenge involves two classical computational problems: one is assigning resources to each of the tasks in the composite web services; the other is scheduling the allocated resources when each resource may be used by multiple tasks at different points of time. In addition, Quality-of-Service (QoS) issues, such as execution time and running costs, must be considered in the resource allocation and scheduling problem. Here we present a Cooperative Coevolutionary Genetic Algorithm (CCGA) to solve the deadline-constrained resource allocation and scheduling problem for multiple composite web services. Experimental results show that our CCGA is both efficient and scalable.

When an organisation becomes aware that one of its products may pose a safety risk to customers, it must take appropriate action as soon as possible or it can be held liable. The ability to automatically trace potentially dangerous goods through the supply chain would thus help organisations fulfill their legal obligations in a timely and effective manner. Furthermore, product recall legislation requires manufacturers to separately notify various government agencies, the health department and the public about recall incidents. This duplication of effort and paperwork can introduce errors and data inconsistencies. In this paper, we examine traceability and notification requirements in the product recall domain from two perspectives: the activities carried out during the manufacturing and recall processes and the data collected during the enactment of these processes. We then propose a workflow-based coordination framework to support these data and process requirements.

Refactoring focuses on improving the reusability, maintainability and performance of programs. However, the impact of refactoring on the security of a given program has received little attention. In this work, we focus on the design of object-oriented applications and use metrics to assess the impact of a number of standard refactoring rules on their security by evaluating the metrics before and after refactoring. This assessment tells us which refactoring steps can increase the security level of a given program from the point of view of potential information flow, allowing application designers to improve their system's security at an early stage.

Wireless network technologies, such as IEEE 802.11 based wireless local area networks (WLANs), have been adopted in wireless networked control systems (WNCS) for real-time applications. Distributed real-time control requires satisfaction of (soft) real-time performance from the underlying networks for delivery of real-time traffic. However, IEEE 802.11 networks are not designed for WNCS applications. They neither inherently provide quality-of-service (QoS) support, nor explicitly consider the characteristics of the real-time traffic on networked control systems (NCS), i.e., periodic round-trip traffic. Therefore, the adoption of 802.11 networks in real-time WNCSs causes challenging problems for network design and performance analysis. Theoretical methodologies are yet to be developed for computing the best achievable WNCS network performance under the constraints of real-time control requirements. Focusing on IEEE 802.11 distributed coordination function (DCF) based WNCSs, this paper analyses several important NCS network performance indices, such as throughput capacity, round trip time and packet loss ratio under the periodic round trip traffic pattern, a unique feature of typical NCSs. Considering periodic round trip traffic, an analytical model based on Markov chain theory is developed for deriving these performance indices under a critical real-time traffic condition, at which the real-time performance constraints are marginally satisfied. Case studies are also carried out to validate the theoretical development.

Type unions, pointer variables and function pointers are a long standing source of subtle security bugs in C program code. Their use can lead to hard-to-diagnose crashes or exploitable vulnerabilities that allow an attacker to attain privileged access over classified data. This paper describes an automatable framework for detecting such weaknesses in C programs statically, where possible, and for generating assertions that will detect them dynamically, in other cases. Exclusively based on analysis of the source code, it identifies required assertions using a type inference system supported by a custom made symbol table. In our preliminary findings, our type system was able to infer the correct type of unions in different scopes, without manual code annotations or rewriting. Whenever an evaluation is not possible or is difficult to resolve, appropriate runtime assertions are formed and inserted into the source code. The approach is demonstrated via a prototype C analysis tool.

The economiser is a critical component for efficient operation of coal-fired power stations. It consists of a large system of water-filled tubes which extract heat from the exhaust gases. When it fails, usually due to erosion causing a leak, the entire generator unit must be shut down to effect repairs. Not only are such repairs highly expensive, but the overall repair costs are significantly affected by fluctuations in electricity market prices, due to revenue loss during the outage. As a result, decisions about when to repair an economiser can alter the repair costs by up to millions of dollars. Therefore, economiser repair decisions are critical and must be optimised. However, making optimal repair decisions is difficult because economiser leaks are a type of interactive failure. If left unfixed, a leak in a tube can cause additional leaks in adjacent tubes which will need more time to repair. In addition, when choosing repair times, one also needs to consider a number of other uncertain inputs such as future electricity market prices and demands. Although many different decision models and methodologies have been developed, an effective decision-making method specifically for economiser repairs has yet to be defined. In this paper, we describe a Decision Tree based method to meet this need. An industrial case study is presented to demonstrate the application of our method.

The Reliability Based Preventive Maintenance (RBPM) strategy is commonly used in industry to improve the reliability of engineering assets. In RBPM, a reliability threshold is predefined for a particular engineering asset. Whenever the reliability of the asset falls to this level, a preventive maintenance action is conducted to improve the asset’s reliability. As preventive maintenance is costly, finding optimal RBPM strategies for engineering assets, especially over a long term with multiple maintenance cycles, is of strategic importance to their owners, so as to increase their market competitiveness. Selecting an optimal RBPM strategy usually involves finding an optimal reliability threshold which enables the total expected cost, including repair cost, preventive maintenance cost and production loss, to be minimised. A number of factors such as required minimal mission time, customer satisfaction, human resources and acceptable risk levels can limit the ability of an organisation to achieve this objective. These factors are usually termed as constraints and have different influences on decision making. However, an effective tool which enables industries to make optimal RBPM decisions with consideration of the effects of these factors is still lacking. To address this issue, here we investigate these factors and identify critical constraints. Furthermore we develop an effective approach for determining the optimal RBPM strategy within the identified multiple constraints.

TARDIS is a generic framework that prescribes mechanisms needed during software development to cater for 'nonfunctional' system requirements. These requirements have been treated in an ad hoc manner in the past, but the increasing importance of safety-critical embedded systems demands more rigorous approaches. The TARDIS framework mandates the inclusion of nonfunctional goals during initial requirements specification and subsequent adherence to these requirements through all phases of software development. The role of TARDIS during specification and high-level design of a software system with stringent real-time goals is illustrated.

Electronic Health Record (EHR) systems are being introduced to overcome the limitations associated with paper-based and isolated Electronic Medical Record (EMR) systems. This is accomplished by aggregating medical data and consolidating them in one digital repository. Though an EHR system provides obvious functional benefits, there is a growing concern about the privacy and reliability (trustworthiness) of Electronic Health Records. Security requirements such as confidentiality, integrity, and availability can be satisfied by traditional hard security mechanisms. However, measuring data trustworthiness from the perspective of data entry is an issue that cannot be solved with traditional mechanisms, especially since degrees of trust change over time. In this paper, we introduce a Time-variant Medical Data Trustworthiness (TMDT) assessment model to evaluate the trustworthiness of medical data by evaluating the trustworthiness of its sources, namely the healthcare organisation where the data was created and the medical practitioner who diagnosed the patient and authorised entry of this data into the patient's medical record, with respect to a certain period of time. The result can then be used by the EHR system to manipulate health record metadata to alert medical practitioners relying on the information to possible reliability problems.

Discrete event-driven simulations of digital communication networks have been used widely. However, it is difficult to use a network simulator to simulate a hybrid system in which some objects are not discrete event-driven but are continuous time-driven. A networked control system (NCS) is such an application, in which physical process dynamics are continuous by nature. We have designed and implemented a hybrid simulation environment which effectively integrates models of continuous-time plant processes and discrete-event communication networks by extending the open source network simulator NS-2. To do this a synchronisation mechanism was developed to connect a continuous plant simulation with a discrete network simulation. Furthermore, for evaluating co-design approaches in an NCS environment, a piggybacking method was adopted to allow the control period to be adjusted during simulations. The effectiveness of the technique is demonstrated through case studies which simulate a networked control scenario in which the communication and control system properties are defined explicitly.

Simulation is widely used as a tool for analyzing business processes but is mostly focused on examining rather abstract steady-state situations. Such analyses are helpful for the initial design of a business process but are less suitable for operational decision making and continuous improvement. Here we describe a simulation system for operational decision support in the context of workflow management. To do this we exploit not only the workflow's design, but also logged data describing the system's observed historic behavior, and information extracted about the current state of the workflow. Making use of actual data capturing the current state and historic information allows our simulations to accurately predict potential near-future behaviors for different scenarios. The approach is supported by a practical toolset which combines and extends the workflow management system YAWL and the process mining framework ProM. This technical report contains a detailed description of how a simulation model including operational decision support can be generated by our software based on the running example.

Accurate and reliable information sharing is essential in the healthcare domain. Currently, however, information about individual patients is held in isolated medical records maintained by numerous separate healthcare providers. Accurately linking this information is necessary for planned nationwide Electronic Health Record systems, but this must be done in a way that not only satisfies traditional data confidentiality requirements, but also meets patientspsila personal privacy needs. Here we present an architecture for linking electronic medical records in a way that gives patients control over what information is revealed about them. This is done through the use of indirect pseudonym identifiers. We then explain how this architecture can be implemented using existing technologies. A case study is used to show how our architecture satisfies data accuracy needs and patientspsila privacy requirements.

The economizer is a critical component in coal fired power stations. An optimal renewal strategy is needed for minimizing the lifetime cost of this component. Here we present an effective optimization approach which considers economizer tubing failure probabilities, repair and renewal costs, potential production losses, and fluctuations in electricity market prices.

There is currently a strong focus worldwide on the potential of large-scale Electronic Health Record systems to cut costs and improve patient outcomes through increased efficiency. A number of countries are developing nationwide EHR systems to aggregate services currently provided by isolated Electronic Medical Record databases. However, such aggregation introduces new risks for patient privacy and data security, both by linking previously-separate pieces of information about an individual, and by creating single access points to a wide range of personal data. It is thus essential that new access control policies and mechanisms are devised for federated Electronic Health Record systems, to ensure not only that sensitive patient data is accessible by authorized personnel only, but also that it is available when needed in life-critical situations. Here we review the traditional security models for access control, Discretionary Access Control, Mandatory Access Control and Role-Based Access Control, and use a case study to demonstrate that no single one of them is sufficient in a federated healthcare environment. We then show how the required level of data security can be achieved through a judicious combination of all three mechanisms.

Networked control over data networks has received increasing attention in recent years. Among many problems in networked control systems (NCSs) is the need to reduce control latency and jitter and to deal with packet dropouts. This paper introduces our recent progress on a queuing communication architecture for real-time NCS applications, and simple strategies for dealing with packet dropouts. Case studies for a middle-scale process or multiple small-scale processes are presented for TCP/IP based real-time NCSs. Variations of network architecture design are modelled, simulated, and analysed for evaluation of control latency and jitter performance. It is shown that a simple bandwidth upgrade or adding hierarchy does not necessarily bring benefits for performance improvement of control latency and jitter. A co-design of network and control is necessary to maximise the real-time control performance of NCSs

We propose a queuing communication architecture for real-time applications of networked control systems (NCSs). Simple strategies are developed to deal with packet dropouts. Typical scenarios are modelled, simulated, and analysed to demonstrate how a TCP/IP based NCS is configured for real- time control of a middle-scale process or multiple small-scale processes.

Any program that measures quantities from its physical environment must compute using correct and consistent units of measurement. Such a program is described as well-measuring. In many systems, particularly embedded control software, paying inadequate attention to units of measurement can result in catastrophe. Unfortunately, current programming languages and tools provide little aid to the programmer attempting to establish or verify the well-measuring property. We present a program analysis technique for inferring and checking the units used within a program. The technique combines traditional Hindley-Milner-style type inference with the use of static single assignment (SSA) form to enable analysis of imperative programs.

The refinement calculus is extended for real-time system development. Heuristic rules for deriving high-level designs from Z specifications are also given. A detailed example of real-time refinement is presented.

Computer software now controls critical systems worldwide. International standards require such programs to be produced from mathematically-precise specifications, but the techniques and tools involved are highly complex and unfamiliar to most programmers. We present a formal basis for extending a tool already used by software developers, the program compiler, to undertake much of the task automatically. This is done by devising a code generation strategy, based on program refinement theory, capable of translating specification constructs embedded in programs into executable code, without the need for programmer intervention.

In component-based software engineering programs are constructed from pre-defined software library modules. However, if the library's subroutines do not exactly match the programmer's requirements, the subroutines' code must be adapted accordingly. For this process to be acceptable in safety or mission-critical applications, where all code must be proven correct, it must be possible to verify the correctness of the adaptations themselves. In this paper we show how refinement theory can be used to model typical adaptation steps and to define the conditions that must be proven to verify that a library subroutine has been adapted correctly.

Embedded control programs are hard to analyse because their behaviour depends on how they interact with hardware devices. In particular, embedded code typically uses interrupts to respond to external events in a timely manner. Such asynchronous control constructs make static analysis difficult due to the potentially large number of alternative control-flow paths they allow. We show how model checking can be used to effectively analyse the behaviour of interrupt-dependent programs. This is done by developing an abstraction of the code that captures its essential timing and functional properties, including those related to external interrupts. The model is made efficient by grouping program instructions into basic blocks whose behaviour is atomic with respect to interrupts.

The dynamic behaviour of multitasking systems is complex and hard to understand. We explain how a simple multitasking simulator was constructed by implementing scheduling theory's computational model in a commercial simulation toolkit. The resulting simulator displays multitasking behaviours graphically.

Refinement is the process of deriving verifiably-correct software from its specification. In practice, however refinement steps are complex and difficult to prove correct. We show how animation can be used to provide insights into the correctness, or otherwise, of refinement steps for the most general form of data refinement in which the whole system design can be changed in a single step.

Many automated programming environments construct software by integrating predefined components from a software library. A fundamental challenge in this process is to match the programmer's specified requirements against the stated capabilities of the components. We explain how the chances of successfully achieving a match can be increased by taking the program context surrounding each requirement into consideration. Formal rules, based on program refinement theory, are defined for context-based matching. The rules allow properties that can be proven to hold at a particular point in the program to justify matching with components that operate correctly only in such a context.

Security protocols preserve essential properties, such as confidentiality and authentication, of electronically transmitted data. However, such properties cannot be directly expressed or verified in contemporary formal methods. Via a detailed example, we describe the phases needed to formalise and verify the correctness of a security protocol in the state-oriented Z formalism.

We show how familiar mathematical concepts from differential and integral calculus can be represented in the Z specification language. Digital computer systems involve hardware devices and software variables that can adopt a limited range of values only, and may be temporarily inaccessible or ill-defined. Emphasis is therefore given to supporting discrete range types and partial functions.

Animation tools have proven to be effective as a means of visualising formal specifications. Specifications that might otherwise be impenetrable can be communicated to a wide range of people involved in the software development process. The authors argue that animation can also aid understanding of formal program development or refinement. We examine two case studies that demonstrate the effectiveness of visualisations generated from a specification animation tool for improving the understanding of refinements.

Timed-trace formalisms have emerged as a powerful method for specifying and reasoning about concurrent real-time systems. We present a simple variant which builds methodically on set theory, and is thus suitable for use by programmers with little formal methods experience.

A practical methodology for compilation of trustworthy real-time programs is introduced. It combines new program development and timing analysis techniques with traditional compilation and assembly technologies.

We show how real-time schedulability tests and program refinement rules can be integrated to create a formal development method of practical use to real-time programmers. A computational model for representing task scheduling is developed within a ⋆imed’ refinement calculus. Proven multi-tasking schedulability tests then become available as feasibility checks during system refinement.

The behaviour of a real-time system that interacts repeatedly with its environment is most succinctly specified by its possible traces, or histories. We present a way of using the refinement calculus for developing real-time programs from requirements expressed in this form. Our trace-based specification statements and target language constructs constrain the traces of system variables, rather than updating them destructively like the usual state-machine model. The only variable that is updated is a special current-time variable. The resulting calculus allows refinement from formal specificationswith hard real-time requirements, to high-level language programs annotatedwith precise timing constraints.

This paper describes the interactive verification of a simple interrupt-driven real-time scheduler written in the machine code language of the MIPS R3000 RISC processor. The formal verification was carried out using the interactive theorem prover Ergo.

Process algebraic specification languages, i.e., CSP, CCS, LOTOS, etc., are semantically founded in the notion of interleaved traces of events. Unfortunately such traces are inadequate when the dimension of “real” time is considered since a totally ordered trace cannot model two or more time-consuming events overlapping in time. As a first step towards solving this problem, it is explained how, through a simple notational device, conventional traces can be augmented to retain causal event relationships. As a concrete illustration, a constructive definition of Basic LOTOS is given in terms of partially ordered traces. The resultant properties are discussed and their applicability outlined. An implementation of these concepts, as a trace generator, is described.

Program compilation can be formally defined as a sequence of equivalence-preserving transformations, or refinements, from high-level language programs to assembler code. Recent models also incorporate timing properties, but the resulting formalisms are intimidatingly complex. Here we take advantage of a new, simple model of real-time refinement, based on predicate transformer semantics, to present a straightforward compilation formalism that incorporates real-time constraints.