ABSTRACT. Concurrency theory suggests the use of fairness as a criterion for a reasonable execution: a transition or a process should not wait an unbounded amount of time to execute if it is enabled continuously (under weak fairness) or indefinitely often (under strong fairness). Unlike multiprocessing, in actual concurrent systems one may rely on the physical nature of the system to act in a ``fair'' manner. However, in many realistic concurrent systems, performing the next transition may involve several smaller steps that can include negotiation and communication, and fairness can be hard to achieve. It is useful to be able to control the global fairness guaranteed by enforcing local constraints on processes. We define local fairness conditions and study their relationship with common notions of global fairness constraints.

ABSTRACT. The synchronous language Esterel provides determinate concurrency for reactive systems. Determinism is ensured by the "signal coherence rule," which demands that signals have a stable value throughout one reaction cycle. This is natural for the original application domains of Esterel, such as controller design and hardware development; however, it is unnecessarily restrictive for software development. Sequentially Constructive Esterel (SCEst) overcomes this restriction by allowing values to change instantaneously, as long as determinacy is still guaranteed, adopting the recently proposed Sequentially Constructive model of computation. SCEst is grounded in the minimal Sequentially Constructive Language, which also provides a novel semantic definition and compilation approach for Esterel.

ABSTRACT. Multi-rate systems arise naturally in distributed settings where computing units execute periodically according to their local clocks and communicate among themselves via message passing. We present a systematic way of designing and verifying such systems with the assumption of bounded drift for local clocks and bounded communication latency. First, we capture the system model through an architecture definition language (called RADL) that has a precise model of computation and communication. The RADL paradigm is simple, compositional, and resilient against denial-of-service attacks. Our radler build tool takes the architecture definition and individual local functions as inputs and generate executables for the overall system as output. In addition, we present a calendar automata-based encoding of multi-rate systems and describe how to verify real-time properties of these systems using SMT-based infinite-state model checking. Lastly, we discuss our experiences in applying this methodology to building high-assurance cyber-physical systems.

ABSTRACT. Distributed implementation of real-time systems has always been a challenging task. The coordination of components executing on a distributed platform has to be ensured by complex communication protocols taking into account their timing constraints. We propose a novel method for distributed implementation of the application software formally expressed in Behavior, Interaction, Priority (BIP). A BIP model consists of a set of components, subject to timing constraints, and synchronizing through multiparty interactions. The proposed method transforms BIP models into Send/Receive BIP models that operate using asynchronous message passing. Send/Receive BIP models include additional components called schedulers that observe atomic components states. Based on these observations, the schedulers are required to plan as soon as possible the execution of interactions. We propose a method that optimizes the number of observed components, and thus reduces the number of exchanged messages.

ABSTRACT. The concept of liquid clocks introduced in this paper is a significant step towards a more precise compile-time framework for the analysis of synchronous and polychromous languages. Compiling languages such as Lustre or Signal indeed involves a number of static analyses of programs before they can be synthesized into executable code, e.g., synchronicity class characterization, clock assignment, static scheduling or causality analysis. These analyses are often equivalent to undecidable problems, necessitating abstracting such programs to provide sound yet incomplete analyses. Such abstractions unfortunately often lead to the rejection of programs that could very well be synthesized into deterministic code, provided abstraction refinement steps could be applied for more accurate analysis. To reduce the number of false negatives occurring during the compilation process, we leverage recent advances in type theory – with the definition of decidable classes of value-dependent type systems – and formal verification, linked to the development of efficient SAT/SMT solvers, to provide a type-theoretic approach that considers all the above analyses as type inference problems. To simplify the exposition of our new approach in this paper, we define a refinement type system for a minimalistic, synchronous, stream-processing language to concisely represent, analyze, and verify logical and quantitative properties of programs expressed as stream-processing data-flow networks. Our type system provides a new framework for representing logical time (clocks) and scheduling properties, and to describe their relations with stream values and, possibly, other quantas. We show how to analyze synchronous stream processing programs (à la Lustre, Signal) to enable previously described analyses involved in compiling such programs. We also prove the soundness of our type system and elaborate on the adaptability of this core framework by outlining its extensibility to specific models of computations and other quantas.

ABSTRACT. To offset the high engineering cost of digital circuit design, hardware engineers are looking increasingly toward high-level languages such as C and C++ to implement their designs. To do this, they employ High-Level Synthesis (HLS) tools that translate their high-level specifications down to a hardware description language such as Verilog. Unfortunately, HLS tools themselves employ sophisticated optimization passes that may have bugs that silently introduce errors in realized hardware. The cost of such errors is high, as hardware is costly or impossible to repair if software patching is not an option.

In this work, we present a translation validation approach for verifying the correctness of the HLS translation process. Given an initial C program and the generated Verilog code, our approach establishes their equivalence without relying on any intermediate results or representations produced by the HLS tool. We implemented our approach in a tool called VTV that is able to validate a body of programs compiled by the Xilinx Vivado HLS compiler.