Formal specifications on temporal behavior of Cyber-Physical Systems (CPS) is essential for verification of performance and safety. Existing solutions for verifying the satisfaction of temporal constraints on a CPS are compute and resource intensive since they require buffering signals from the CPS prior to constraint checking. We present an online approach, based on Timestamp Temporal Logic (TTL), for monitoring the timing constraints in CPS. The approach reduces the computation and memory requirements by processing the timestamps of pertinent events reducing the need to capture the full data set from the signal sampling. The signal buffer size bears a geometric relationship to the dimension of the signal vector, the time interval being considered, and the sampling resolution. Since monitoring logic is typically implemented on Field Programmable Gate Arrays (FPGAs) for efficient monitoring of multiple signals simultaneously, the space required to store the buffered data becomes the limiting resource. The monitoring logic, for the timing constraints on the Flying Paster (a printing application requiring synchronization between two motors), is illustrated in this paper to demonstrate a geometric reduction in memory and computational resources in the realization of an online monitor.

Time is a foundational aspect of Cyber-Physical Systems (CPS). Correct time and timing of system events are critical to optimized responsiveness to the environment, in terms of timeliness, accuracy, and precision in the knowledge, measurement, prediction, and control of CPS behavior. However, both the specification and verification of timing requirements of the CPS are typically done in an ad-hoc manner. While feasible, the system can become costly and difficult to analyze and maintain, and the process of implementing and verifying correct timing behavior can be error-prone. Towards the development of a verification testbed for testing timing behavior in tools and platforms with explicit time support, this paper first describes a way to express the various kinds of timing constraints in distributed CPS. Then, we outline the design and initial implementation of a distributed testbed to verify the timing of a distributed CPS analytically through a systematic framework. Finally, we illustrate the use of the verified timing testbed on two distributed CPS case studies.

In order to test the performance and verify the correctness of Cyber-Physical Systems (CPS), the timing constraints on the system behavior must be met. Signal Temporal Logic (STL) can efficiently and succinctly capture the timing constraints of a given system model. However, many timing constraints on CPS are more naturally expressed in terms of events on signals. While it is possible to specify event-based timing constraints in STL, such statements can quickly become long and arcane in even simple systems. Timing constraints for CPS, which can be large and complex systems, are often associated with tolerances, the expression of which can make the timing constraints even more cumbersome using STL. This paper proposes a new logic, Timestamp Temporal Logic (TTL), to provide a definitional extension of STL that more intuitively expresses the timing constraints of distributed CPS. TTL also allows for a more natural expression of timing tolerances. Additionally, this paper outlines a methodology to automatically generate logic code and programs to monitor the expressed timing constraints. Since our TTL monitoring logic evaluates the timing constraints using only the timestamps of the required events on the signal, the TTL monitoring logic has significantly less memory footprint when compared to traditional STL monitoring logic, which stores the signal value at the required sampling frequency. The key contribution of this paper is a scalable approach for online monitoring of the timing constraints. We demonstrate the capabilities of TTL and our methodology for online monitoring of TTL constraints on two case studies: 1) Synchronization and phase control of two generators and, 2) Simultaneous image capture using distributed cameras for 3D image reconstruction.

Signal processing and multimedia applications are commonly modeled using Static/Cyclo-Static Dataflow (SDF/CSDF) models. SDF/CSDF explicitly specifies how much data is produced and consumed per firing during computation. This results in strong compile-time analyzability of many useful execution properties such as deadlock absence, channel boundedness, and throughput. However, SDF/CSDF is limited in its ability to capture how data is accessed in time. Hence, using these models often leads to implementations that are sub-optimal (i.e., use more resources than necessary) or even incorrect (i.e., use insufficient resources). In this work, we advance a new model called Static Dataflow with Access Patterns (SDF-AP) that captures the timing of data accesses (for both production and consumption). This paper formalizes the semantics of SDF-AP, defines key properties governing model execution, and discusses algorithms to check these properties under correctness and resource constraints. Results are presented to evaluate these analysis algorithms on practical applications modeled by SDF-AP.

Many fuel systems for diesel engines are developed with the help of commercial one-dimensional computational fluid dynamics (1D CFD) solvers that model and simulate the behavior of fluid flow through the interconnected pipes off-line. This paper presents a novel framework to evaluate 1D CFD models in real time on an FPGA. This improves fuel pressure estimation and closes the loop on fuel delivery, allowing for a cleaner and more efficient engine. The real-time requirements of the models are defined by the physics and geometry of the problem being solved. In this framework, the interconnected pipes are partitioned into individual sub-volumes that compute their pressure and flow rate every time step based upon neighboring values. We use timing-based synchronization and multiple Precision Timed (PRET) processor cores to ensure the real-time constraints are met. Leveraging the programmability of FPGAs, we use a configurable heterogeneous architecture to save hardware resources. Several examples are presented along with the implementation results after place and route for a Xilinx Virtex 6 FPGA. The results demonstrate the resource savings and scalability of our framework, confirming the feasibility of our approach -- solving 1D CFD models in real time on FPGAs.

FPGA devices provide flexible, fast, and low-cost prototyping and production solutions for system design. However, as the design complexity continues to rise, the design and synthesis iterations become a labor intensive and time consuming ordeal. Consequently, it becomes imperative to raise the level of abstraction for FPGA designs, while providing insight into performance metrics early in the design process. In particular, an important design time problem is to determine the maximum clock frequency that a circuit can achieve on a specific FPGA target before full synthesis and implementation. This early quantification can greatly help evaluate key design characteristics without reverting to tedious runs of the full implementation flow. In this work, we focus on the predictability of timing delay of circuits composed of high-level blocks on an FPGA. We are well aware of difficulties in tackling uncertainties in early timing estimation, e.g., an inherent gap between a high-level representation and gates/wires; extremely difficult delay estimation due to the randomness in physical design tools, etc. We show that the estimation uncertainties can be mitigated through a carefully characterized timing database of primitive building blocks and refined timing analysis models. We primarily focus on applications composed of data-intensive word-level arithmetic computations from the DSP domain and specified using static dataflow models. Our experiments indicate that for these applications, timing estimates can be obtained reliably within a good error margin on average and in the worst case. As future work, we plan to fine tune the timing database by modeling resource utilization effects and inter-primitive/actor routing delay via variants of Rent's rule and related efforts. We are also interested in exploring dynamic sub-cycle timing characterization.

In this paper we present a graphical programming environment for hardware designs targeted at FPGA devices. We first introduce LabVIEW™, a scientific software system, and its modular virtual instrumentation programming paradigm. Then, we discuss how LabVIEW FPGA enables application domain experts without prior knowledge of hardware description languages (HDLs) to program reconfigurable hardware devices. Initially many LabVIEW FPGA users were high-level (software centric) application domain experts in the area of control with prior knowledge of LabVIEW, where they benefited from a new fast and reliable target, namely FPGAs. Recently, we have found that system level integrators with lower level hardware design interest, but still no working experience in detailed HDL coding, have been able to use LabVIEW FPGA to successfully implement high-speed hardware designs. Here we focus on how LabVIEW facilitates reconfigurable hardware designs for applications of ultra-high speed control, complex timing and synchronization, hardware-in-the-loop (HIL) testing, etc. Specifically, we detail its modeling, simulation, and debugging capabilities as well as its rigorous semantics as a programming and deployment framework. Furthermore, we use application use cases to illustrate how LabVIEW FPGA can support a flexible, reliable and cost-effective hardware design.

Most common real-time embedded programming languages provide a means to specify functionality; however, they have few constructs to specify precise timing constraints. LabVIEW is one example of a graphical programming language that supports timing specifications in the form of timed-loops. In this work, we present a plug-in for LabVIEW Embedded that maps the LabVIEW G graphical programming language and its timing specifications to the PREcision Timed machine (PRET), an architecture that exposes timing instructions in its instruction set architecture. We demonstrate the use of the plug-in with a simple producer/consumer example that uses timing to enforce synchronization.