1. TMA, a runtime verification method for CPS
In order to be confident about the behavior of a CPS design or implementation, its timing behavior must be tested and verified. Prior to performing testing of the temporal behavior, timing constraints must be expressed in a formal language that enables robust analysis of constraint satisfiability and consistency. The formal expression also enables the application developer to explicitly specify timing requirements in the design phase and provide the basis to automate the generation of the application and associated test code to enable a more systematic, rigorous, and iterative verification process of the System Under Test (SUT).
TMA (Timestamp-based Monitoring Approach) is a light-weight monitoring tool that evaluates the temporal behavior of CPS in either offline or online manner by utilizing the event timestamps. There are some other temporal monitoring tools in which the evaluation of timing constraints is performed at each time-step. In such monitoring approaches, since the evaluation is done based on the sampling frequency (at every time-step) they comprise computing intensive process. However, since they work with future temporal logics, the implementation of timing operators becomes problematic because they need a buffer proportionate to their intervals. TMA is an efficient method to have run-time monitoring of temporal specification in Cyber-Physical Systems (CPS) in either offline or online. It receives the required timing constraints for SUT and returns the time durations in which the timing constraints are met. In online monitoring, application constraints are continuously monitored during runtime. Online monitoring can be used to analyze the system behavior in the field and check for bugs in the design. In contrast, offline monitoring in real systems utilizes forensic analysis and therefore does not offer the ability for timely correction of system deviations. The “TMA tool” in MATLAB is an implementation of TMA method in offline manner used to reveal the temporal violations after running CPS. The method receives the timing constraints of CPS written in Timestamp Temporal Logic (TTL) that is a temporal logic working on the events and their timing constraints. Since it is after the operation, it needs the captured signals from the SUT and the timing constraints to be monitored. It does not need to know the system sates or even knowing the structure of the SUT. After providing the signal values and the timing constraints for the tool, it shows the time intervals in which the system timing constraints have not been met.
In general, for a constraint that is defined over a time interval of T, and must be monitored for the duration of experiment d, with a sampling frequency of f, the conventional approach requires O(T f d) computation time. The requirements of both, computation time and memory, depending on the interval size and the sampling rate. In contrast, TMA has a complexity of O(k), where k is the maximum number of events during time d. This is because TMA uses the last two timestamps of the events-of-interest and the last two timestamps of the result are needed. Therefore, four 32 − bit variables for each operator is needed, which is independent of interval length and sampling rate, and a small memory footprint for the state machine. We need one state machine per operator and the size of each state machine is very small since it needs only 2 bits to store the state.
2. TMA, a tool to check the consistency for the Timing constraints of CPS.
In order to have a meaningful monitoring approach, it is needed to make sure the system’s timing constraints are correct and there is no inconsistency among all. The TTL deduction system (TTL Natural Deduction System) has been proposed to verify the consistency among TTL statements and simplify the monitoring logic. The TTL reasoning system is able to combine and accumulate errors in the combined and cascaded statements and thus, support a rigorous and correct monitoring process. We have developed a tool, using Python and Z3 theorem prover, to verify the consistency of a set of timing constraints. The monitoring technique also considers the error tolerance in expressing CPS temporal requirements. The error tolerance is intended to capture the aggregate error of the system, including the measurement error of the monitoring device.
TTL Consistency Checker Manual