The reviewer explained to the author that in his deep insight into the nature of things and his long-term experience with textbooks there were books that improve the world and there were books that are being read.The author asked for confirmation whether the reviewer felt that the coming book would belong to those books that improve the world.Let me skip how I got myself out of this difficult situation.When asked whether a book will be read, the question is by whom.Citing the author, this book is intended for readers interested in the theory of abstract interpretation, the understanding of formal methods, and the design of verifiers and static analyzers.And my answer is, it is a must read for these groups of

No abstract available.

Worst-Case Execution-Time (WCET) Analysis is the first phase of Timing Analysis, which attempts to verify that a set of real-time tasks can be executed on an execution platform such that all tasks respect their deadlines. WCET analysis determines upper bounds on execution times, which are then passed on to a Schedulability Analysis, the second phase of Timing Analysis. This clean separation into the two phases holds for single-core execution platforms. Multi-core platforms require a more complex interaction between WCET analysis and schedulability analysis. We have solved the WCET-analysis problem for single-core platforms. Key to our success was the use of Abstract Interpretation for the static analysis of the behavior of architectural components such as caches, pipelines, buses, and peripheries. The Program-Analyzer Generator (PAG), which is based on Abstract Interpretation, allowed us to quickly develop and experiment with abstract domains, to arrive at sound, precise, and scalable solutions.

Multi-core processors are increasingly considered as execution platforms for embedded systems because of their good performance/energy ratio. Many applications implemented on multi-core platforms are safety- and some also time-critical. A critical issue for these applications is the reduced predictability of such systems resulting from the interference of different applications on shared resources. These interferences can be at least of two kinds: Several applications may request a resource at the same time, but the resource can only admit one access at a time. As a consequence, an arbitration mechanism may delay the request of all but one application, thus slowing down the other applications. This is the case of resources like buses, typically called bandwidth resources. On the other hand, one application may also change the state of a shared resource such that another application using that resource will suffer from a slowdown. This is the case with shared memories, such as shared caches and shared dynamic random-access memories, which fall into the class of storage resources. Interference on shared resources makes worst-case execution time (WCET) analysis of applications more difficult since a task or a thread can no longer be analyzed for its timing behavior in isolation. All potential interferences slowing down (or speeding up) the task under analysis have to be considered. This leads to a combinatorial explosion of the analysis complexity, as all possible interleavings of different threads have to be analyzed. The survey [1] considers several aspects of the execution of sets of tasks on multi-core platforms that have to do with the interference of the tasks on shared resources. One question is how the actual performance of tasks is slowed down by other co-running tasks. Another is how to compute bounds on the slow-down in order to derive sound guarantees for the timing behavior. A major problem is the increased complexity of this task compared to the single-task single-core case. This has led to the situation that industry is developing embedded systems for multi-core platforms while there exist no timing-analysis methods and tools that are both sound and precise.

A large class of embedded systems is distinguished from general-purpose computing systems by the need to satisfy strict requirements on timing, often under constraints on available resources. Predictable system design is concerned with the challenge of building systems for which timing requirements can be guaranteed a priori . Perhaps paradoxically, this problem has become more difficult by the introduction of performance-enhancing architectural elements, such as caches, pipelines, and multithreading, which introduce a large degree of uncertainty and make guarantees harder to provide. The intention of this article is to summarize the current state of the art in research concerning how to build predictable yet performant systems. We suggest precise definitions for the concept of “predictability”, and present predictability concerns at different abstraction levels in embedded system design. First, we consider timing predictability of processor instruction sets. Thereafter, we consider how programming languages can be equipped with predictable timing semantics, covering both a language-based approach using the synchronous programming paradigm, as well as an environment that provides timing semantics for a mainstream programming language (in this case C). We present techniques for achieving timing predictability on multicores. Finally, we discuss how to handle predictability at the level of networked embedded systems where randomly occurring errors must be considered.

No abstract available.

For non-embedded software, binary translation has shown to be a successful method for retargeting legacy software onto new platforms. To apply binary translation to embedded software, two issues must be considered. First of all, embedded software often involves real-time constraints that must still be met after translation. Secondly, embedded software contains a significant amount of code dedicated to peripheral device communication which necessitates device emulation. This paper focuses on the last aspect.

Embedded hard real-time systems need reliable guarantees for the satisfaction of their timing constraints. The precision of the results and the efficiency of timing-analysis methods are highly dependent on the predictability of the execution platform.

Embedded hard real-time systems need reliable guarantees for the satisfaction of their timing constraints. Experience with the use of static timing-analysis methods and the tools based on them in the automotive and the aeronautics industries is positive. However, both the precision of the results and the efficiency of the analysis methods are highly dependent on the predictability of the execution platform. In fact, the architecture determines whether a static timing analysis is practically feasible at all and whether the most precise obtainable results are precise enough. Results contained in this paper also show that measurement-based methods still used in industry are not useful for quite commonly used complex processors. This dependence on the architectural development is of growing concern to the developers of timing-analysis tools and their customers, the developers in industry. The problem reaches a new level of severity with the advent of multicore architectures in the embedded domain. This paper describes the architectural influence on static timing analysis and gives recommendations as to profitable and unacceptable architectural features.

Automotive systems are increasingly distributed and complex. Reduced time-to-market, cost and safety concerns require advance validation of the integrated systems and its components, from the functional, timing, and reliability standpoints. In particular, function correctness and performance may depend on communication and computation delays imposed by the selected architecture platform. Hence, the need for methods and tools capable of predicting the system-level timing behaviour (latencies and jitter), resulting from the HW platform selection, the synchronization between tasks and messages, and also from the synchronization and queuing policies of the middleware and RTOS levels. In this paper, we review methods and tools for the evaluation of the function performance and its timing correctness by simulation or by worst case static analysis.

Hard real-time systems have stringent timing constraints expressed in units of time. To ensure that a task finishes within its time-frame, the designer of sucha system must be able to derive upper bounds on the task's worst-case execution time (WCET). To compute such upper bounds, timing analyses are used. These analyses require that information such as bounds on the maximum numbers of loop iterations are known statically, i.e. during design time. Parametric timing analysis softens these requirements: it yields symbolic formulas instead of single numeric values representing the upper bound on the task's execution time. In this paper, we present a new parametric timing analysis that is able to derive safe and precise results. Our method determines what the parameters ofthe program are, constructs parametric loop bounds, takes processor behavior into account and attains a formula automatically. In the end, we present tests to show that the precision and runtime of our analysis are very close to those of numeric timing analysis.

The determination of upper bounds on execution times, commonly called worst-case execution times (WCETs), is a necessary step in the development and validation process for hard real-time systems. This problem is hard if the underlying processor architecture has components, such as caches, pipelines, branch prediction, and other speculative components. This article describes different approaches to this problem and surveys several commercially available tools 1 and research prototypes.

This is an introduction to the EMSOFT 2007 Panel on Grand Challenges in Embedded Software.

Shape analysis concerns the problem of determining “shape invariants” for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed using an abstract interpretation based on three-valued first-order logic. In that work, concrete stores are finite two-valued logical structures, and the sets of stores that can possibly arise during execution are represented (conservatively) using a certain family of finite three-valued logical structures. In this article, we show how three-valued structures that arise in shape analysis can be characterized using formulas in first-order logic with transitive closure. We also define a nonstandard (“supervaluational”) semantics for three-valued first-order logic that is more precise than a conventional three-valued semantics, and demonstrate that the supervaluational semantics can be implemented using existing theorem provers.

We consider the problem of scheduling a number of periodic tasks T on a real-time architecture composed of a set of identical processors P connected by a common bus. Each processor p \in P has a certain amount of memory \mu (p). In our setting, a task \tau \in¸ T is specified by the period t(\tau), the memory requirement \mu (\tau), the execution time c(\tau), and the deadline d(\tau). We always assume d (\tau) \leqslant t(\tau). Tasks may communicate with each other by sending messages. We denote the set of messages by M, and for each m \in M, src(m) is the source task of m, dst(m) is the target task of m, l(m) is the length of m, and d(m) is the deadline for m. The problem is to find a mapping \prod\limits_{}{} : T \in P representing an assignment of the tasks to the processors that satisfies timing and resource requirements for both tasks and messages. The problem is known to be NP-hard even if tasks do not communicate with each other [9].

The goal of this work is to develop compile-time algorithms for automatically verifying properties of imperative programs that manipulate dynamically allocated storage. The paper presents an analysis method that uses a characterization of a procedure's behavior in which parts of the heap not relevant to the procedure are ignored. The paper has two main parts: The first part introduces a non-standard concrete semantics, LSL, in which called procedures are only passed parts of the heap. In this semantics, objects are treated specially when they separate the "local heap" that can be mutated by a procedure from the rest of the heap, which---from the viewpoint of that procedure---is non-accessible and immutable. The second part concerns abstract interpretation of LSL and develops a new static-analysis algorithm using canonical abstraction.

The design of embedded real-time systems requires skills from multiple specific disciplines, including, but not limited to, control, computer science, and electronics. This often involves experts from differing backgrounds, who do not recognize that they address similar, if not identical, issues from complementary angles. Design methodologies are lacking in rigor and discipline so that demonstrating correctness of an embedded design, if at all possible, is a very expensive proposition that may delay significantly the introduction of a critical product. While the economic importance of embedded systems is widely acknowledged, academia has not paid enough attention to the education of a community of high-quality embedded system designers, an obvious difficulty being the need of interdisciplinarity in a period where specialization has been the target of most education systems. This paper presents the reflections that took place in the European Network of Excellence Artist leading us to propose principles and structured contents for building curricula on embedded software and systems.

Hard real-time avionics systems like flight control software are expected to always react in time. Consequently, it is essential for the timing validation of the software that the worst-case execution time (WCET) of all tasks on a given hardware configuration be known. Modern processor components like caches, pipelines, and branch prediction complicate the determination of the WCET considerably since the execution time of a single instruction may depend on the execution history. The safe, yet overly pessimistic assumption of no cache hits, no overlapping executions in the processor pipeline, and constantly mispredicted branches results in a serious overestimation of the WCET. Our approach to WCET prediction was implemented for the Motorola ColdFire 5307. It includes a static prediction of ∗ This work was partly supported by the RTD project IST-1999-20527 “DAEDALUS” of the European FP5 program. cache and pipeline behavior, producing much tighter upper bounds for the execution times. The WCET analysis tool works on real applications. It is safe in the sense that the computed WCET is always an upper bound of the real WCET. It requires much less effort, while producing more precise results than conventional measurement-based methods.

The architecture of tools for the determination of worst case execution times (WCETs) as well as the precision of the results of WCET analyses strongly depend on the architecture of the employed processor. The cache replacement strategy influences the results of cache behavior prediction; out-of-order execution and control speculation introduce interferences between processor components, e.g., caches, pipelines, and branch prediction units. These interferences forbid modular designs of WCET tools, which would execute the subtasks of WCET analysis consecutively. Instead, complex integrated designs are needed, resulting in high demand for memory space and analysis time. We have implemented WCET tools for a series of increasingly complex processors: SuperSPARC, Motorola ColdFire 5307, and Motorola PowerPC 755. In this paper, we describe the designs of these tools, report our results and the lessons learned, and give some advice as to the predictability of processor architectures.

Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision. A key innovation of the work is that the stores that can possibly arise during execution are represented (conservatively) using 3-valued logical structures. The framework is instantiated in different ways by varying the predicates used in the 3-valued logic. The class of programs to which a given instantiation of the framework can be applied is not limited a priori (i.e., as in some work on shape analysis, to programs that manipulate only lists, trees, DAGS, etc.); each instantiation of the framework can be applied to any program, but may produce imprecise results (albeit conservative ones) due to the set of predicates employed.

A method for finding bugs in code is presented. For given small numbers j and k, the code of a procedure is translated into a rela-tional formula whose models represent all execution traces that involve at most j heap cells and k loop iterations. This formula is conjoined with the negation of the procedure's specification. The models of the resulting formula, obtained using a constraint solver, are counterexamples: executions of the code that violate the specification.

Algorithm animation attempts to explain an algorithm by visualizing interesting events of the execution of the implemented algorithm on some sample input. Algorithm explanation describes the algorithm on some adequate level of abstraction, states invariants, explains how important steps of the algorithm preserve the invariants, and abstracts from the input data up to the relevant properties. It uses a small focus onto the execution state. This paper is concerned with the explanation of algorithms on linked data structures. The thesis of the paper is that shape analysis of such algorithms produces abstract representations of such data structures, which focus on the "active" parts, i.e., the parts of the data structures, which the algorithm can access during it's next steps. The paper presents a concept of visually executing an algorithm on these abstract representations of data.

We present a family of abstract-interpretation algorithms that are capable of determining "shape invariants" of programs that perform destructive updating on dynamically allocated storage. The main idea is to represent the stores that can possibly arise during execution using three-valued logical structures.

This article concerns the static analysis of programs that perform destructive updating on heap-allocated storage. We give an algorithm that uses finite shape graphs to approximate conservatively the possible “shapes” that heap-allocated structures in a program can take on. For certain programs, our technique is able to determine such properties as (1) when the input to the program is a list, the output is also a list and (2) when the input to the program is a tree, the output is also a tree. For example, the method can determine that “listness” is preserved by (1) a program that performs list reversal via destructive updating of the input list and (2) a program that searches a list and splices a new element into the list. None of the previously known methods that use graphs to model the program's store are capable of determining that “listness” is preserved on these examples (or examples of similar complexity). In contrast with most previous work, our shape analysis algorithm is even accurate for certain programs that update cyclic data structures; that is, it is sometimes able to show that when the input to the program is a circular list, the output is also a circular list. For example, the shape-analysis algorithm can determine that an insertion into a circular list preserves “circular listness.”

While the quality of the results of T E X's mathematical formula layout algorithm is convincing, its original description is hard to understand since it is presented as an imperative program with complex control flow and destructive manipulations of the data structures representing formulae. In this paper, we present a re-implementation of T E X's formula layout algorithm in the functional language SML, thereby providing a more readable description of the algorithm, extracted from the monolithical T E X system.

This paper concerns the static analysis of programs that perform destructive updating on heap-allocated storage. We give an algorithm that conservatively solves this problem by using a finite shape-graph to approximate the possible "shapes" that heap-allocated structures in a program can take on. In contrast with previous work, our method is even accurate for certain programs that update cyclic data structures. For example, our method can determine that when the input to a program that searches a list and splices in a new element is a possibly circular list, the output is a possibly circular list.

The compression of bottom-up tree automata and their representation as implemented in the OPTRAN tree transformation system are described here as a four-step process.First, the vertically working tree automata traversing one generation in one step are replaced by horizontally working automata, splitting this step into rank (operator) steps, This replaces each matrix of dimension rank (operator) by a tree of depth rank (operator), A second step replaces this tree by a shortened directed acyclic graph (DAG), that is, a DAG where equivalent states of the tree are identified and paths in the tree with no gain in information are condensed, The acceptance property of the automaton is not changed.This and the following size reduction steps critically depend on the "no-error" assumption, that is, the assumption that input trees are correctly built and that no error detection is required of the tree automata.The third step embeds the DAG, which is naturally represented by two-dimensional tables, into a linear array using row displacement and row column schemes.In addition, this step compresses strings of consecl~.,veidentical entries, which occur often in this type of automaton.The last step exploits the memory structure and addressability of the target machine.Using information on automata and table sizes, the most efilcient storage representation is selected.The data structures and access functions are generated as C objects and functions, respectively.Results showing the effectiveness of the different steps are given.

Call-by-need is widely regarded as an optimal (to within a constant factor) parameter passing mechanism for functional programming languages. Except for certain special cases involving higher order functions, call-by-need is optimal with respect to time. However, call-by-need is far from optimal with respect to space. We examine some of the space problems which can arise with call-by-need and other parameter passing mechanisms. A simple optimizing technique, based on work by Mycroft [1], is proposed. If it can be determined both that an expression must be evaluated eventually and that the evaluation of the expression is likely to reduce the space required by the program, then the evaluation is performed as soon as possible. This optimization does not result in optimal space performance in all cases. However, in most of the common cases where call-by-need causes a problem the proposed optimization avoids the problem. Since our technique is not always optimal, it is likely to be of greatest advantage in situations where efficiency is important but not critical. For example, functional languages with call-by-name semantics are increasingly being used as specification languages. Since such a specification is runnable, it may be used as a prototype. This makes it possible to experiment with a program and refine the specification before the implementation in the target language is started.

Inverse currying transformation of an attribute grammar moves a context condition to places in the grammar where the violation of the condition can be detected as soon as the semantic information used in the condition is computed. It thereby takes into account the evaluation order chosen for the attribute grammar. Inverse currying transformations can be used to enhance context sensitive parsing using predicates on attributes, to eliminate sources of backtrack when parsing according to ambiguous grammars, and to facilitate semantics-supported error correction.