Modern cyber-physical systems (CPS) consist of multiple components including sensors, controllers, machine learning (ML) components, real-time schedulers, among others. Each component is usually designed separately with the aim of working perfectly. For example, task schedulers aim to ensure that all deadlines are met and ML components aim to always make perfect inferences. The correctness or "perfection" of the overall CPS is inferred from the correctness of its components. However, none of the CPS components are perfect in reality. Schedulers or tasks sometimes miss deadlines, ML components sometimes make inaccurate inferences, and sensors are occasionally noisy. These imperfections are assumed to be small enough to be ignored. In particular, it is assumed – without guarantees – that these imperfections do not compromise system safety or the correctness of the CPS.We propose to reverse this approach and argue that there is usually sufficient tolerance at the system level. This tolerance should be explicitly modeled, and its impact on the correctness or perfection of system components should be determined. This enables the design of more cost-effective, robust systems. Furthermore, appropriately designing the other components to compensate for the imperfection of individual components ensures that system-level safety remains within the specified margins.

System security requires a solid foundation in both development and operation. During development, performance trade-offs result in security infrastructures that are more or less effective, but usually imperfect. Hence, during operation, runtime monitoring and anomaly detection continuously check for security issues.In this paper, we show how development and operation can be linked. We demonstrate how information and data from development and operation can be aggregated in a digital twin and/or digital thread which is used as the basis for runtime monitoring and anomaly detection. In particular, we address the trade-off between system security and performance in a concrete smart grid system.

In exposed data path architectures, registers are replaced by an on-chip network that connects their processing units (PUs) directly. This allows the compiler to determine PU allocation, instruction scheduling, and data transport between the PUs. To prevent unnecessary synchronization of the PUs, their network ports are typically buffered. Although many performance models are available for traditional RISC architectures, there are no specific performance models for buffered exposed datapath (BED) architectures.In this paper, we investigate the impact of the relevant design parameters of BED architectures, consider their dependencies, and determine reasonable parameter values for designing cost-effective efficient BED processors. In particular, we examine the number of PUs, the instruction issue width (superscalarity), the size of network buffers, and the latency of instructions, and relate these parameters with the processor performance. We develop a performance model to estimate the runtime in terms of the mentioned parameters and validate our performance model with experimental results.

In traditional von Neumann processors, the central register file is an inherent limiting factor in exploiting the instruction-level parallelism (ILP) of programs. To alleviate this problem, many processors follow a hybrid von Neumann/dataflow computing model in which specific instruction sequences are executed in dataflow order by communicating intermediate values directly from producer processing units (PUs) to consumer PUs without using a central register file. However, the intermediate values often reside in local registers of the PUs, which requires a synchronization of the data transports that still limits the exploitation of the ILP.To avoid the use of a central register file and the need for any synchronization between PUs, some newer architectures suggest first-in-first-out (FIFO) buffers instead of local registers at the input and output ports of the PUs. Since values are produced and consumed, and are thus never overwritten (as in registers), the compiler must determine the required number of copies of each value. Furthermore, it is necessary to control the number of copies of values to develop buffer size aware compilation methods. However, the number of variable uses in a sequential program may depend on the future execution. This paper presents transformations for ‘balancing’ a given program, i.e., transforming the program so that for all points in the program, the number of future uses of all variables can be accurately determined in order to allocate the required buffer sizes in the later compilation phases. The classical space-time trade-off is demonstrated by the experimental results which show an improvement of the processor performance with increasing buffer sizes and vice versa. More importantly, the experimental results demonstrate the potential of buffered hybrid dataflow architectures for a scalable use of ILP.

Graphical dataflow models are widely used for industrial control system implementation and are accepted by users with different backgrounds due to their intuitive visualization of the dataflow. As real-world applications have evolved, the complexity of these diagrams has increased, posing a challenge in the verification and maintenance of software models. In this paper, we argue that the perceived complexity of real-world applications can be simplified and transformed into formal models for reuse in software engineering or formal verification. To overcome the limitations of previous research on optimizing graphical dataflow models in an industrial context, we identify potentially optimizable submodels and optimize them, leaving the non-modifiable components unchanged. The optimized software model is then reconstructed and optionally translated into formal models for reuse or verification purposes. The paper describes the identification of submodels in real-world applications and demonstrates the need for configurability of the optimization. We present an open-source-based implementation using graphical dataflow models of programmable logic controllers and demonstrate the impact of our optimization approach using real-world applications from the literature and vendor-provided examples. The results help to reduce the complexity of existing dataflow models and to reuse existing real-world applications as formal software models.

Dataflow process networks (DPNs) provide a convenient model of computation that is often used to model system behavior in model-based designs. With fixed sets of nodes, they are also used as dataflow graphs as an intermediate program representation by compilers to uncover instruction-level parallelism of sequential programs. Many recent processor architectures, which are still von Neumann architectures, also use dataflow computing to increase their exploitation of instruction-level parallelism by exposing their datapaths so that the compiler can take care of the allocation of processing units (PUs), the execution schedules of instructions on the PUs, and the communication of intermediate values between PUs. If the communication paths are buffered, these architectures can be abstracted into a DPN architecture whose PUs and interconnection network are DPN nodes. In this article, we introduce a DPN abstraction of hybrid dataflow/von Neumann architectures and consider the mapping of the nodes of a given dataflow graph to the PUs of such a DPN architecture such that there are no conflicts due to the mapping of different nodes to the same PU. We express the allocation and scheduling constraints in terms of propositional logic for the original dataflow graph and for a modified version of the dataflow graph that simplifies the constraints by introducing levels using copy nodes, such that all nodes receive inputs only from nodes of the previous level. We also formulate equisatisfiable SMT constraints using integer variables to reason directly about the parallel runtime. On this basis, we further present alternative SAT constraints that explicitly encode concurrency, and discuss variants of the constraints for a better understanding of the same.

Function Block Diagrams (FBDs) are widely used for implementing the software of IEC 61131-3 based systems. In general, there is a risk that FBDs used in industry will become more and more complex during their life cycle, while at the same time strict specifications have to be met. On the other hand, a trend towards model-based design with standardized modeling tools can be observed in software engineering. While previous research focuses on translating existing FBDs to formal models for verification purposes, this paper presents two translations from existing FBDs to sequentially constructive statecharts, thus enabling an intuitive functional reuse for a model-based design. Besides a basic translation in the first approach, it is shown in the second approach that it is possible to improve the readability through code refactoring within the synchronous paradigm.

Many novel processor architectures expose their processing units (PUs) and internal datapaths to the compiler. To avoid an unnecessary synchronization of PUs, the datapaths are often buffered which results in buffered exposed datapath (BED) architectures. This paper suggests a code generation technique for BED architectures from dataflow graphs that are used as intermediate program representations. Inspired by results on queue layouts in graph drawing, we determine in this paper constraints for the node and edge orderings of the dataflow graphs to ensure the first-in-first-out behavior of the buffers. Formalizing these constraints in propositional logic enables SAT solvers to compute optimal PU allocations. Moreover, future code generation techniques may develop heuristics based on the code generation criteria of this paper.

The synthesis of distributed embedded systems by desynchronization starts from a synchronous model and keeps its functional behavior while generating a corresponding dataflow process network (DPN). This method supports the modeling of dynamic behaviors while avoiding the problems like deadlocks and buffer overflows in DPNs. However, a DPN can be heterogeneous in the sense that different nodes may exhibit either static or dynamic behaviors. An efficient synthesis method should automatically generate implementations by exploiting this heterogeneity.In this paper we improve the desynchronization process by exploiting synchronous components with various input/output behaviors which can then be desynchronized to a heterogeneous DPN where each node can be scheduled and executed accordingly. Moreover, a synthesis tool chain is developed to automatically synthesize the heterogeneous DPN to the open computing language (OpenCL) based implementation that can be deployed on various commercial off-the-shelf (COTS) target platforms.

The synthesis of distributed embedded systems from dataflow models like Kahn Process Networks (KPN) has to deal with particular problems like absence of deadlocks and buffer overflows. However, the verification of the absence of these problems for a KPN model is in general not decidable. Starting with synchronous models, desynchronization avoids such design difficulties by generating sound dataflow networks by correctness of construction. In this paper, we present a design flow following such an approach. Our design flow differs from previous work in the following aspects: The synchronous models are specified by an imperative synchronous language and are therefore better suited for control-intensive applications. Verification of desynchro-nization criteria is carried out efficiently with the help of model checking and SAT-solving, ensuring the compliance of the functional behavior. Qualified code is translated automatically into the KPN model. Finally, the KPN model is automatically synthesized to the open computing language (OpenCL) based implementation which is platform independent and can be executed on various commercial off-the-shelf target platforms.

The synthesis of distributed embedded systems based on desynchronization is attractive since it preserves the functional behavior of the synchronous model while avoiding the verification of the absence of problems like deadlocks and buffer overflows. In this paper, we improve the desynchronization process by introducing synchronous components with various input/output (IO) patterns which can then be desynchronized to a heterogeneous dataflow process network (DPN) where each node can be scheduled and executed accordingly. We further designed a synthesis tool chain that automatically synthesizes the heterogeneous DPN to the open computing language (OpenCL) based implementation which is platform-independent and can be deployed on various commercial off-the-shelf (COTS) target platforms.

In this paper, a translation from structured sequential programs to equivalent dataflow process networks (DPNs) is presented that is based on a carefully chosen set of nodes including load/store operations to access a shared global memory. For every data structure stored in the main memory, we use corresponding tokens to enforce the sequential ordering of load/store operations accessing that data structure as far as needed. Except for the load/store nodes, all nodes obey the Kahn principle so that they are deterministic in the sense that the same inputs are always mapped to the same outputs regardless of the execution schedule of the nodes. Due to the sequential ordering of load/store nodes, determinacy is also maintained by them. Moreover, the generated DPNs are quasi-static, i.e., they have schedules that are bounded in a very strict sense: For every statement of the sequential program, the corresponding DPN behaves like a homogeneous synchronous actor, i.e., it consumes one value of each input port and will finally provide one value on each output port. Hence, no more than one value needs to be stored in each buffer.

Programmable logic controllers operating in a sequential execution scheme are widely used for various applications in industrial environments with real-time requirements. The graphical programming languages described in the third part of IEC 61131 are often intended to perform open and closed loop control tasks. Continuous Function Charts (CFCs) represent an additional language accepted in practice which can be interpreted as an extension of IEC 61131-3 Function Block Diagrams. Those charts allow more flexible positioning and interconnection of function blocks, but can quickly become difficult to manage. Furthermore, the sequential execution order forces a sequential processing of possible independent and thus possibly parallel program paths. The question arises whether a translation of existing CFCs to synchronous programs considering independent actions can lead to a more manageable software model. While current formalization approaches for CFCs primarily focus on verification, the focus of this approach is on restructuring and possible reuse in engineering. This paper introduces a possible automated translation of CFCs to imperative synchronous Quartz programs and outlines the potential for reducing the states of equivalent extended finite state machines through restructuring.

A dataflow process network (DPN) is a system of concurrent processes which communicate with each other through statically determined and buffered point-to-point connections. While the general model of computation (MoC) does not impose further restrictions, many different subclasses of DPNs have been considered over time like Kahn process networks, cyclo-static networks and synchronous dataflow networks. These classes differ in the kinds of behaviors of the processes that are precisely described based on how each process is triggered for an execution, and based on how each execution of a process consumes/produces data. A heterogeneous combination of particular kinds of processes can be effectively used to model different components of a system with different kinds of MoCs. Such a composition of dataflow processes within a network is termed as heterogeneous DPN. There are design tools for modeling like Ptolemy and FERAL that support different MoCs including particular classes of DPNs by the use of so-called directors. However, design tools for synthesis are usually restricted to the weakest classes of DPNs, i.e., cyclo-static and synchronous DPNs. In this paper, we present an extendable model-based design framework called SHeD for automatic -software synthesis of heterogeneous -DPNs. SHeD supports different kinds of DPN processes and therefore also different kinds of MoCs. To this end, SHeD proposes a general DPN model that is used with specific definitions and constraints to formulate the precise classes of DPNs. Also, it provides a tool chain, including different specialized code generators for specific MoCs, and a runtime system that finally maps models using a combination of different MoCs on the target hardware. We demonstrate the effective use of SHeD by a case study of a distributed automotive research platform.

Conventional processor architectures are limited in exploiting instruction level parallelism (ILP). One of the reasons for this limitation is their relatively low number of registers. Thus, recent processor architectures expose their datapaths so that the compiler can take care of directly transporting results from processing units to other processing units. Among these architectures, the Synchronous Control Asynchronous Dataflow (SCAD) architecture is a recently proposed exposed datapath architecture whose goal is to completely bypass the use of registers.

The RVC-CAL language is used for implementing dataflow process networks (DPNs), i.e., distributed systems of actors. The behavior of an actor is defined by a set of actions which can consume input tokens and produce output tokens. RVC-CAL DPNs can offer parallelism both at the level of actors and at the level of actions. To efficiently execute these models on a target hardware, it is important to generate parallel code based on the entire parallelism provided by these two levels. In this paper, we discuss criteria for the generation of parallel software from RVC-CAL models based on the potential parallelism of modeled behaviors. The approach considers both the coarse-grained (task-parallel) execution of actors using multithreading and the fine-grained (data-parallel) execution of their actions using the open computing language (OpenCL) or even a higher-level layer of OpenCL, namely SYCL. The methodology is validated by benchmarks on OpenCL abstracted hardware platforms. Based on the experimental results, the methodology is evaluated for efficiency (performance) in comparison with a pure multithreaded C++ approach and a well-known reference framework.

In general, model-based design flows start from hardware-agnostic models and finally generate code based on the used model of computation (MoC). The generated code is then manually mapped with an additional non-trivial deployment step onto the chosen target architecture. This additional manual step can break all correctness-by-construction guarantees of the used model-based design, in particular, if the chosen architecture employs a different MoC than the one used in the model. To automatically bridge this gap, we envisage a holistic model-based design framework for heterogeneous synthesis that allows the modeling of a system using a combination of different MoCs. Second, it integrates the standard hardware abstractions using the Open Computing Language (OpenCL) to promote the use of vendor-neutral heterogeneous architectures. Altogether, we envision an automatic synthesis that maps models using a combination of different MoCs on heterogeneous hardware architectures. This paper evaluates the feasibility of incorporating OpenCL as a standard hardware abstraction for such a framework. The evaluation is presented as a case study to map a synchronous application on different target architectures using the OpenCL specification.

No abstract available.

Radix-based interconnection networks recursively partition the messages according to the most significant bits of their target addresses. The required split modules are usually implemented by binary sorting networks or by permutation networks. While sorting networks are self-routing, it can be proven that permutation networks cannot be self-routing so that they require additional configuration logic which is not required for sorting networks. In this paper, we point out that sorting networks are however not the best self-routing split modules. In particular, we first use our previous work to construct better self-routing split modules from sorting networks. Second, we show that even if the best sorting networks are used for the latter construction, we can still find better self-routing split modules. To determine optimal self-routing split modules, we reduce the problem to an equivalent model-checking problem. Using this, we derive provably optimal-depth and optimal-size self-routing split modules for small numbers of inputs.

Abstract Conventional processor architectures are restricted in exploiting instruction level parallelism (ILP) due to the relatively low number of programmer-visible registers. Therefore, more recent processor architectures expose their datapaths so that the compiler (1) can schedule parallel instructions to different processing units and (2) can make effective use of local storage of the processing units. Among these architectures, the Synchronous Control Asynchronous Dataflow (SCAD) architecture is a new exposed datapath architecture whose processing units are equipped with first-in first-out (FIFO) buffers at their input and output ports. In contrast to register-based machines, the optimal code generation for SCAD is still a matter of research. In particular, SAT and SMT solvers were used to generate optimal resource constrained and optimal time constrained schedules for SCAD, respectively. As Answer Set Programming (ASP) offers better flexibility in handling such scheduling problems, we focus in this paper on using an answer set solver for both resource and time constrained optimal SCAD code generation. As a major benefit of using ASP, we are able to generatealloptimal schedules for a given program which allows one to study their properties. Furthermore, the experimental results of this paper demonstrate that the answer set solver can compete with SAT solvers and outperforms SMT solvers.This paper is under consideration for acceptance in TPLP.

Conventional processor architectures are restricted in exploiting instruction level parallelism (ILP) due to the limited number of available registers in their instruction sets. Therefore, recent processor architectures expose their datapaths so that the compiler not only schedules instructions to functional units, but also takes care of directly moving values between functional units avoiding the need of registers at all. However, the current compiler technology is still based on classic register architectures where a nearly optimal register mapping is the key for the quality of the generated assembly code. The Synchronous Control Asynchronous Dataflow (SCAD) architecture is a new exposed datapath architecture where processing units (PUs) are equipped with first-in first-out (FIFO) buffers at their inputs and outputs. Code generation for SCAD machines can be done as known for classic queue machines to completely eliminate the use of registers, and to improve the degree of exploited ILP. However, the SCAD code generated this way is not optimal since compared to queue machines, SCAD machines can contain many PUs and buffers which offers the compiler more freedom to reduce unnecessary computational overhead. In this paper, we map the SCAD code generation problem to a satisfiability problem, and then use SAT solvers to generate code without overhead that works with the minimal number of PUs. The generated optimal code will serve as a reference to judge the quality of heuristics that will be finally used in SCAD compilers.

A concentrator is a circuit with n inputs and m ≤ n outputs that can route any given subset of k ≤ m valid inputs to k of its m outputs. Concentrator circuits are important for many applications, in particular, for the design of interconnection networks. The design of concentrator circuits is however a challenging task that has already been considered in many research papers. All practical implementations aim at configuring the switches of a permutation network so that it behaves as a concentrator. In this paper, we present methods to analyze various properties of permutation networks by means of binary decision diagrams (BDDs). In particular, we can check whether it is possible to use a considered permutation network as a concentrator or even as a binary sorter. While our method can be applied to all permutation networks, we consider some particular permutation networks and verify that some of them can be used as concentrators and even as binary sorters provided that a specific permutation of the outputs is added.

Property directed reachability (PDR) has been introduced as a very efficient verification method for synchronous hardware circuits that is based on induction rather than fixpoint iteration. However, hardware circuits are usually synthesized from more abstract high-level languages like synchronous languages (or synchronous subsets of hardware description languages). In this paper, we show that it is possible to derive from such high-level languages additional control-flow information that can be added to the transition relation to make PDR even more efficient. As will be shown, PDR can benefit from this additional information since many safety properties become inductive only with respect to the enhanced transition relations. The added control-flow information is not needed for the synthesis and is therefore not explicitly encoded in the generated systems, but it can be easily derived from the original programs and used for verification. We present two methods to compute additional control-flow information that differ in how precisely they approximate the reachable control-flow states and also in the runtime required for their computation.

Model-based design flows for embedded systems have been introduced to allow late design changes while still keeping tight time-to-market deadlines. In general, these design flows start with abstract models and refine these to a final implementation maintaining already implemented properties. However, essentially all of these design flows suffer from a deployment gap in the sense that the finally generated files are general program files which assume a particular model of computation (MoC) that may not be provided by the chosen target architecture. For this reason, the final deployment is usually a non-trivial manual design step that can break all correctness-by-construction guarantees of the previous model-based design. In this paper, we therefore introduce the idea of MoC drivers which wraps the real sensor and actuator interaction in a shell that provides the MoC of the generated software. As a particular example, we discuss in this paper how MoC drivers bridge the deployment gap between automatically generated dataflow programs and event-driven behaviors of the target architecture. The approach is illustrated with a Speedometer application on a distributed automotive embedded platform.

Verification condition generators (VCGs) can reduce overall correctness statements about sequential programs to verification conditions (VCs) that can then be proved independently by automatic theorem provers like SMT solvers. SMT solvers became not only more powerful in recent years in that they can now solve much bigger problems than before, they can now also solve problems of less restricted logics, for example, by covering non-linear arithmetic as required by some hybrid systems. However, there is so far still no VCG procedure that could generate VCs of hybrid programs for these SMT solvers. We therefore propose in this paper a first VCG procedure for hybrid systems that is based on induction proofs on the strongly connected components (SCCs) of the underlying state transition diagrams. Given the right invariants for a safety property, the VCs can be automatically generated for the considered hybrid system. The validity of the VCs is then independently proved by SMT solvers and implies the correctness of the considered safety property.

Effectiveness of timing analysis of real-time applications depends on the timing predictability of the underlying execution platform. Modern hardware architectures improve average case performance using complex features. However, these features make Worst Case Execution Time (WCET) analysis complicated often leading to pessimistic derived worst case execution time. We present the preliminary design of Synchronous Control Asynchronous Dataflow (SCAD) - a new model of computation targeting time-predictability and competitive performance. Inorder execution of instructions and capability to bypass memory accesses imparts timing predictability to SCAD computational model. We also motivate a code generation technique to optimally utilize the memory bypassing capability of SCAD and that results in increased instruction level parallelism.

To improve the performance of the memory system, multiprocessors implement weak memory consistency models. Weak memory models admit different views of the processes on their load and store instructions, thus allowing for computations that are not sequentially consistent. Program analyses have to take into account the memory model of the targeted hardware. This is challenging because numerous memory models have been developed, and every memory model requires its own analysis. In this article, we study a prominent approach to program analysis: testing. The testing problem takes as input sequences of operations, one for each process in the concurrent program. The task is to check whether these sequences can be interleaved to an execution of the entire program that respects the constraints of a memory model under consideration. We determine the complexity of the testing problem for most of the known memory models. Moreover, we study the impact on the complexity of parameters, such as the number of concurrent processes, the length of their executions, and the number of shared variables. What differentiates our contribution from related results is a uniform approach that avoids considering each memory model on its own. We build upon work of Steinke and Nutt. They showed that the existing memory models form a hierarchy where one model is called weaker than another one if it includes the latter’s behavior. Using the Steinke-Nutt hierarchy, we develop three general concepts that allow us to quickly determine the complexity of a testing problem. First, we generalize the technique of problem reductions from complexity theory. So-called range reductions propagate hardness results between memory models, and we apply them to establish NP lower bounds for the stronger memory models. Second, for the weaker models, we present polynomial-time testing algorithms that are inspired by determinization algorithms for automata. Finally, we describe a single SAT encoding of the testing problem that works for all memory models in the Steinke-Nutt hierarchy to prove their membership in NP . Our results are general enough to carry over to future weak memory models. Moreover, they show that SAT solvers are adequate tools for testing.

While synchronous system models have many advantages over asynchronous models concerning verification and validation, many implementation platforms do not provide efficient means for synchronization. For this reason, we consider a design flow that starts with a synchronous system model that is then transformed into an asynchronous one for synthesis. In essence, it partitions the synchronous system into a set of asynchronous components that communicate with each other via FIFO buffers. Of course, the synthesized system still has to behave as the original synchronous model, i.e., for each variable exactly the same flow of data values must be observed and only the membership to synchronous reaction steps is no longer explicitly given. In this paper, we prove that this correctness guarantee is given provided that (1) each component knows which of the input values have to be used for the next reaction (endochrony), (2) each component is able to perform the reaction (constructiveness), and (3) components agree on the clocks of their shared variables (isochrony/clock-consistency).

Signed-digit (SD) numbers generalize traditional radix numbers by allowing negative digits within a certain range. Typically, this leads to redundant number representations that can be used to avoid the carry propagation problem of addition of radix numbers. Unfortunately, as proved by Avizienis, the standard algorithm for carry-free addition of SD numbers does not work for the binary case. In this paper, we therefore construct a special algorithm for the carry-free addition and subtraction of binary SD numbers, i.e., addition and subtraction of n-digit numbers are performed with circuits of depth O(1) and size O(n). This is possible by computing in addition to the transfer digits used by the standard algorithm one additional bit that allows us to distinguish relevant cases to avoid propagation of dependencies. The additional bit and the transfer digit used to compute the sum digit at position i depend only on the summands' digits at positions i and i - 1 so that all sum digits can be computed with a hardware circuit of a depth that is independent of the number of digits. We first explain the basics of the standard addition algorithm to derive the additional information needed to fix the algorithm for the binary case. After proving the correctness of our algorithm, we present experimental results that show that our implementation clearly outperforms two's complement addition even for small numbers, and saves 50% of the required chip area compared to other carry-free implementations.

Clock/time-driven models are powerful abstractions of real-time systems, as e.g., provided by the synchronous models of computation which lend themselves well for simulation and verification. At every clock cycle, new inputs are read, computations are performed in zero-time, and results are immediately/synchronously communicated between components. However, such zero-time idealizations are not realistic since computation and communication finally takes time in implementations. For implementations, data-driven execution models have the advantage to impose no timing constraints other than arrival of input data, and thus, these models are perfectly suited for distributed or other kinds of asynchronous implementations. For this reason, modern model-based design flows consider the desynchronization of synchronous models for system synthesis which is possible for the subclass of endochronous systems only. While definitions of endochrony were considered for years, it is shown in this paper how to efficiently verify endochrony by SAT solving. Our procedure consists of two steps: In the first step, we introduce buffers to the interface of a clock-driven component, so that its inputs can arrive at different points of time. After this step, clocks of signals are viewed as ‘instructions’ telling the component which input values have to be consumed for the current reaction.We call such components clock-scheduled. In the second step, we remove the clocks from the interface of the clock-scheduled components, so that the component may now become nondeterministic. We prove in this paper that a synchronous component is endochronous, if and only if the clock signals can be safely removed in this step without destroying determinism. Based on this result, we present a decision procedure based on symbolic system representations to check whether components are endochronous. Preliminary experimental results show the effectiveness of our method.

The lack of formal foundations of UML results in imprecise models since UML only defines graphical notations, but not their formal semantics. However, in safety-critical applications, formal semantics is a requirement for verification. Semantics for the key parts of activities and classes of UML is defined by the semantics of a foundational subset for executable UML models (fUML). Moreover, the base semantics given by fUML defines the formal semantics of UML. In this paper, we evaluate a subset of the base semantics given by fUML covering its formal definition and its use for verification. From the practical perspective, we show with a simple example how the base semantics can support formal verification through theorem proving. The initial results show that the base semantics, when mature, can play an important role in the formal verification of UML models.

This paper presents a method to translate a given synchronous system to a multithreaded system where process nodes communicate via channels with each other. It is well-known that the reduction of communication has been identified to be a crucial key for efficient utilization of multiprocessor systems. For this reason, we first use synchronous elastic design methods to generate a distributed/multithreaded system from a synchronous system, and then, reduce communication overhead between the obtained process nodes. Our benchmarks show that we can save up to 67.5% of communication costs using our method and can achieve an average speed-up of up to 1.09.

The synchronous model of computation requires that in every step, inputs are read and outputs are synchronously computed as the reaction of the program. In addition, all internal variables are updated in parallel even though not all of these values might be required for the current and the future reaction steps. To avoid unnecessary computations, we present a compile-time optimization procedure that computes for every variable a condition that determines whether its value is required for current or future computations. In this sense, our optimizations allow us to identify passive code that can be disabled to avoid unnecessary computations and therefore to reduce the reaction time of programs or their energy consumption.

Modern FPGAs often provide a number of highly optimized hard IP blocks with certain functionalities. However, manually instantiating these blocks is both time-consuming and error-prone, in particular, if only a part of the functionality of the IP block is used. To solve this problem, we developed an algorithm to automatically replace a selected combinational subset of a hardware design with a correct instantiation of a given IP block. Both the IP block and the part of the hardware circuit to be replaced are specified using arithmetic and Boolean operators. Our method is based on higher-order E-unification with an equational theory of arithmetic and Boolean laws. To demonstrate the effectiveness and efficiency of our approach, we present preliminary experiments with various circuits.

In this paper, we show how code can be generated at different levels of abstraction from a single source description. To this end, we use a model-driven development tool called Averest that is based on a synchronous programming language. We illustrate our approach by means of a case study from the domain of distributed real-time automotive embedded systems. This paper focuses thereby mainly on the use of the Averest toolkit to generate code at different levels of abstraction.

This paper presents an embedding of polychronous programs into synchronous ones. Due to this embedding, it is not only possible to deepen the understanding of these different models of computation, but, more importantly, it is possible to transfer compilation techniques that were developed for synchronous programs to polychronous programs. This transfer is nontrivial because the underlying paradigms differ more than their names suggest: Since synchronous systems react deterministically to given inputs in discrete steps, they are typically used to describe reactive systems with a totally ordered notion of time. In contrast, polychronous system models entail a partially ordered notion of time, and are most suited to interface a system with an asynchronous environment by specifying input/output constraints from which a deterministic controller may eventually be refined and synthesized. As particular examples for the mentioned cross fertilization, we show how a simulator and a verification backend for synchronous programs can be made available to polychronous specifications, which is a first step toward integrating heterogeneous models of computation.

The synchronous programming model is perfect for modeling, simulation, verification and implementation of reactive systems. While this paradigm can be directly implemented as hardware circuits, multithreaded software implementations are typically based on asynchronous threads. For this reason, an efficient multithreaded software implementation of a synchronous program requires a so-called desynchronization that could however potentially violate the already verified properties of the synchronous program. In this paper, we therefore present a theory to check whether properties verified for a synchronous system are preserved by a desynchronization. In particular, we prove a theorem based on directed-flow equivalence that specifies the requirements of delay relations among system variables that a desynchronization has to meet.

We propose a new approach to the interactive verification of synchronous systems. Our approach is based on two system representations: Systems to be verified are given as synchronous programs that are considered for the selection of proof rules, while the proof rules are applied on equivalent sets of synchronous guarded actions that are obtained by an automatic translation from the programs. Since the obtained guarded actions contain assumptions and assertions, they are directly used as proof goals in our approach. Due to a back-annotation via control flow locations, there is still a direct correspondence between the two system representations. This way, the user can still consider the more readable program code while the implementation of the proof system on top of the guarded actions allows much more flexible decompositions of the verification goals.

On behalf of the organizing and program committee, we would like to welcome you to the 29thIEEE International Conference on Computer Design 2011. The International Conference on Computer Design (ICCD) encompasses a wide range of technical topics and provides an ideal environment to discuss practical and theoretical work that enables cross-pollination. The ICCD venue and program reflect this goal. This year the conference is being held at the beautiful campus of the University of Massachusetts at Amherst, United States.

The synchronous model of computation (MoC) has been successfully used for the design of embedded systems having a local control like hardware circuits and single-threaded software, while its application to distributed parallel embedded systems is still a challenge. In contrast, other MoCs such as data-flow process networks (DPNs) directly match with these architectures. In this paper, we therefore present a translation of synchronous systems to data-flow process networks, thereby bridging the gap between synchronous and asynchronous MoCs. We use the resulting DPNs to generate CAL code for the Open DF package, which offers important features for embedded system design.

In this paper, we present several optimization techniques to improve the runtime and size of the code generated from synchronous programs. These optimizations work on extended finite state machines (EFSMs) that can be used as intermediate representation for any synchronous system. Our optimizations consists of two phases: First, local optimization guides the EFSM generation and considers the states and edges separately. Second, global optimization is based on a dataflow analysis of the entire EFSM. For both phases, we employ an SMT (Satisfiability Modulo Theories) solver to verify the individual optimization steps. Our experiments show the potential of the presented optimizations: optimized programs generally have a smaller size and a better run-time performance.

Synchronous languages offer a deterministic model of concurrency at the level of actions. However, essentially all compilers for synchronous languages compile these actions into a single thread by sophisticated methods to guarantee dynamic schedules for the sequential execution of these actions. In this paper, we present the compilation of synchronous programs to multi-threaded OpenMP-based C programs. We thereby start at the level of synchronous guarded actions which is a comfortable intermediate language for synchronous languages. In addition to the explicit parallelism given in the source program, our method also exploits the implicit parallelism which is due to the underlying synchronous model of computation and the data dependencies of the guarded actions. We show how viable tasks can be constructed from the actions of a program and show the feasibility of our approach by a small example.

In this paper, we present an extension of the synchronous language Quartz by new kinds of variables, actions and statements for modeling the interaction of synchronous systems with their continuous environment. We present an operational semantics of the obtained hybrid modeling language and moreover show how compilation algorithms that have been originally developed for synchronous languages can be extended to these hybrid programs. Thus, we can automatically translate the hybrid programs to compact symbolic representations of hybrid transition systems that can be immediately used for simulation and formal verification.

Concurrent Action-Oriented Specifications (CAOS) model the be- havior of a synchronous hardware circuit as asynchronous guarded actions at an abstraction level higher than the Register Transfer Level (RTL). Previous approaches always considered the compilation of CAOS, which includes a transformation of the under-lying model of computation and the scheduling of guarded actions per clock cycle, as a tightly integrated step. In this paper, we present a new compilation procedure, which separates these two tasks and translates CAOS models to synchronous guarded actions with an explicit interface to a scheduler. This separation of con- cerns has many advantages, including better analyses and integration of custom schedulers. Our method also generates assertions that each scheduler must obey that can be fulfilled by algorithms for scheduler synthesis like those developed in supervisory control. We present our translation procedure in detail and illustrate it by various examples. We also show that our method simplifies for- mal verification of hardware synthesized from CAOS specifications over previously known formal verification approaches.

To overcome over-synchronization in synchronous programs, we recently introduced clock refinement to our synchronous programming language Quartz. This extension basically allows programmers to refine reaction steps into smaller internal computation steps while maintaining the external behavior. In this paper, we consider the compilation of the extended Quartz programs to synchronous guarded actions. To this end, we first define an intermediate language supporting multiple clocks based on synchronous guarded actions which is the target of the front-end of the compiler and the source of back-end tools that perform efficient analysis and synthesis procedures. We moreover present a compilation scheme to translate the extended Quartz programs to the new intermediate language. We discuss important design considerations and illustrate our approach with the help of some small examples.

The goal of the MEMOCODE conference series, the eighth in a series of successful international conferences, is to gather together researchers and practitioners in the field of the design of modern hardware and software systems in order to explore ways in which future design methods can benefit from new results on formal methods. MEMOCODE is unique in the way it merges the formal community with the hands-on design community, and it creates a forum where principle meets practice. MEMOCODE covers a spectrum of interesting co-design topics, and it attracts industry and academia to engage in an interesting dialog.

The compilation of imperative synchronous languages like Esterel has been widely studied, the separate compilation of synchronous modules has not, and remains a challenge. We propose a new compilation method inspired by traditional sequential code generation techniques to produce coroutines whose hierarchical structure reflects the control flow of the original source code. A minimalistic runtime system executes separately compiled modules.

Synchronous programming languages are well-suited for the design of safety-critical real-time embedded systems. However, the compilers and synthesis procedures are challenged by the synchronous programming paradigm and have to solve additional problems like causality and schizophrenia problems. Algorithms to solve these basic compilation problems have already become mature, but code optimization still lacks behind. Often, code optimization is left to the back-end tools like compilers for sequential software or hardware synthesis tools. In this paper, we develop a static analysis procedure to introduce code optimization techniques to synchronous languages. We develop specialized code optimization procedures that can be applied to all kinds of synchronous languages. Similar to the code optimization techniques used for the compilation of sequential software, our procedures are also based on a static data-flow analysis that is adapted to the synchronous programing model.

We deal with the problem of designing suitable languages for the modeling and the automatic verification of properties over analog circuits. To this purpose, we suitably enrich classical temporal logics with basic formul\ae allowing to model arbitrary functions relating analog variables. We show how to automatically check the resulting CTLf formulæ on analog circuits. In particular, we rely on interval arithmetic methods and we extend to the analog context a number of techniques for the abstraction and the verification of digital systems, based on three-valued temporal logics.

We present a new compilation technique for generating efficient code from synchronous programs. The main idea of our approach consists of computing for each program location an instantaneous statement (called a job) that has to be executed whenever the corresponding program location is active. Given the computed jobs, the overall execution scheme is highly flexible, very efficient, but nevertheless very simple: At each instant, it essentially consists of executing the set of active jobs according to their dynamic dependencies. Besides the required outputs, the execution of the jobs additionally yields the set of active threads for the next instant. As our translation directly follows the structure of the source code, the correctness of the translation can be easily checked by theorem provers. Furthermore, our translation scheme offers new potential for multi-processor execution, modular compilation, and multi-language code generation

In principle, bounded model checking (BMC) leads to semi-decision procedures that can be used to verify liveness properties and to falsify safety properties. If the procedures fail, there is usually no information about the validity of the considered specification. In this paper, we present a new approach to BMC based on three-valued logic that allows us in many cases to falsify liveness properties and to verify safety properties. Moreover, we employ both global and local model checking to take advantage of the different types of specifications that can be handled by these techniques.

Model checking and supervisor synthesis have been successful in solving different design problems related to discrete systems in the last decades. In this paper, we analyze some advantages and drawbacks of these approaches and combine them for mutual improvement. We achieve this through a generalization of the supervisory control problem proposed by Ramadge and Wonham. The objective of that problem is to synthesize a supervisor which constrains a system's behavior according to a given specification, ensuring controllability and coaccessibility. By introducing a new representation of the solution using systems of μ-calculus equations, we are able to handle these two conditions separately and thus to exchange the coaccessibility requirement by any condition that could be used in model checking. Well-known results on μ-calculus model checking allow us to easily assess the computational complexity of any generalization. Moreover, the model checking approach also delivers algorithms to solve the generalized synthesis problem. We include an example in which the coaccessibility requirement is replaced by fairness constraints. The paper also contains an analysis of related work by several authors.

Synchronous programs are well-suited for the implementation of real-time embedded systems. However, their compilation is difficult due to the paradigm that microsteps are executed in zero time. This can yield cyclic dependencies that must be resolved to generate single-threaded code. State of the art techniques are based on a fixpoint computation at compile time that 'simulates' the microstep execution. However, existing procedures do not consider delayed actions that have been recently introduced in synchronous languages. In this paper, we show that the analysis of programs with delayed actions can be performed by two fixpoint computations, one for the initialization and one for the transitions of the system. Moreover, we discuss an implementation using BDDs that is based on dual rail encoding.

Various techniques have been proposed to determine the worst case execution time of real--time systems. For most of these approaches, it is not necessary to capture the complete semantics of the system. Instead, it suffices to analyze an abstract model provided that it reflects the system's execution time correctly. To this end, we present an abstraction technique based on program slicing that can be used to simplify software systems at the level of assembler programs. The key idea is to determine a minimal set of instructions such that the control flow of the program is maintained. This abstraction is essential for reducing the runtime of the analysis algorithms, in particular, when symbolic methods are used to perform a complete state space exploration.

We present a new approach to bounded model checking that extends current methods in two ways: firstly, instead of a reduction to propositional logic, we choose a more powerful, yet decidable target logic, namely Presburger arithmetic. Secondly, instead of unwinding temporal logic formulas, we unwind corresponding /spl omega/-automata. To this end, we employ a special technique for translating safety and liveness properties to /spl omega/-automata with corresponding acceptance conditions. This combination allows us to utilize bounded model checking techniques for the efficient verification of infinite state systems.

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.

In this paper, we present a technique for determining tight bounds on the execution time of assembler programs. Thus, our method is independent of the design flow, but takes into account the target architecture to obtain accurate estimates. The key idea is to compute the maximal number of executed instructions by means of symbolic simulation. To this end, we utilize a slight extension of Presburger arithmetic that can be translated to finite automata. Finite automata are an efficient data structure for symbolically traversing the state space of a program.

We present a generalization of the supervisory control problem proposed by Ramadge and Wonham. The objective of that problem is to synthesize a controller, which constrains a system's behavior according to a given specification, ensuring controllability and co-accessibility. By introducing a new representation of the solution using systems of /spl mu/-calculus equations we are able to handle these two conditions separately and thus to exchange the co-accessibility requirement by any /spl mu/-calculus expression. Well-known results on the complexity of /spl mu/-calculus model checking allow us to easily assess the computational complexity of any generalization. As an example we solve the synthesis problem under consideration of fairness constraints.

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.

Synchronous programming languages have proved to be advantageous for designing software and hardware for embedded systems. Despite their clear semantics, their compilation is remarkably difficult: In particular, one has to take care of potential schizophrenia problems. Although these problems are correctly translated with existing compilers, there is still a need for clean algorithms. In this paper, we present the first solution to eliminate schizophrenia problems by program transformations. These transformations are used for compilation, but also for increasing the readability of programs.

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.

In this paper, we enrich VHDL with new specification constructs intended for hardware verification. Using our extensions, total correctness properties may now be stated whereas only partial correctness can be expressed using the standard VHDL assert statement. All relevant properties can now be specified in such a way that the designer does not need to use formalisms like temporal logics. As the specifications are independent from a certain formalism, there is no restriction to a certain hardware verification approach.