In this paper a novel approach to high-level (i.e. architecture independent) worst case execution time (WCET) analysis is presented that automatically computes exact bounds for all inputs. To this end, we make use of the distinction between micro and macro steps as usually done by synchronous languages. As macro steps must not contain loops, a later low-level WCET analysis (architecture dependent) is simplified to a large extent. Checking exact execution times for all inputs is a complex task that can nevertheless be efficiently done when implicit state space representations are used. With our tools, it is not only possible to compute path information by exploring all computations, but also to verify given path information.

Synchronous programming languages are well-suited for the implementation and verification of real-time systems. The main benefit for the estimation of real-time constraints is thereby that the macro steps provided by synchronous programs can be directly used for runtime analysis. If synchronous circuits are generated from these descriptions, the macro steps are implemented by combinatorial circuits, and if software is generated, they correspond to basic building blocks that do not contain loops. In this paper, we describe methods to generate timed transitions systems from a synchronous program by taking the final architecture into account. For software synthesis, this requires considering different microprocessors and compilers, and for hardware synthesis, this requires considering a hierarchy of clocks to optimize the clock speed.

We present an extension of synchronous programming languages that can be used to declare program locations irrelevant for verification. An efficient algorithm is proposed to generate from the output of the usual compilation an abstract real-time model by ignoring the irrelevant states, while retaining the quantitative information. Our technique directly generates a single real-time transition system, thus overcoming the known problem of composing several real-time models. A major application of this approach is the verification of real-time properties by symbolic model checking.

We present a new temporal logic for the specification and verification of real-time systems. This logic is defined on discrete time transition systems which are interpreted in an abstract manner instead of the usual stuttering interpretation. Our approach directly allows the abstraction of real-time systems by ignoring irrelevant qualitative properties, but without loosing any quantitative information.

We present a new real-time temporal logic for the specification and verification of discrete quantitative temporal properties. This logic is an extension of the well-known logic CTL. Its semantics is defined on discrete time transition systems which are in turn interpreted in an abstract manner instead of the usual stuttering interpretation. Hence, our approach directly supports abstractions of real-time systems by ignoring irrelevant qualitative properties, but without loosing any quantitative information. We analyse the complexity of the presented model checking algorithm and furthermore present a fragment of the logic that can be efficiently checked.

We present abstraction techniques for systems containing counters, which allow us to significantly reduce their state spaces for their efficient verification. In contrast to previous approaches, our abstraction technique lifts the entire verification problem, i.e., also the specification, to the abstract level. As an application, we consider the reduction of real-time systems by replacing discrete clocks of timed automata with abstract counters. The presented method allows the reduction of such systems to very small state spaces. As benchmark examples, we consider the generalized railroad crossing and Fischer's mutual exclusion protocol.

If real number calculations are implemented as circuits, only a limited preciseness can be obtained. Hence, formal verification cannot be used to prove the equivalence between the mathematical specification based on real numbers and the corresponding hardware realization. Instead, the number representation has to be taken into account in that certain error bounds have to be verified. For this reason, we propose formal methods to guide the complete design flow of these circuits from the highest abstraction level down to the register-transfer level with formal verification techniques that are appropriate for the corresponding level. Hence, our method is hybrid in the sense that it combines different state-of-the-art verification techniques. Using our method, we establish a more detailed notion of correctness that considers beneath the control and data flow also the preciseness of the numeric calculations. We illustrate the method with the discrete cosine transform as a real-world example.

Abstract We present a very simple scheme for compiling boolean expressions in the short‐circuit manner in one pass. The generated code is of very high quality and avoids most inefficiencies commonly associated with one‐pass code generation. In particular, redundant conditional and unconditional branches are kept to a minimum. The scheme is general enough to compile the boolean expressions of a typical high‐level language such as Pascal. It is presented in a format suited for syntax‐directed translation and can be used with both top‐down and bottom‐up parsing.