CPS: Synergy: Safety-Aware Cyber-Molecular Systems
When dealing with safety-critical programmed molecular systems, it is essential to be able to observe the behavior of a system. The capability to log the states of a system over time, for later observation, is critical to help determine when and how faults have occurred.
The work presented here describes the design of a logging device to record the state of a molecular system. Logs are widely used in software systems to record a history of events or system variables. They have a multitude of uses once they are recorded. A log can be read by another system or an external user to determine if a fault has occurred and to determine the cause and timing of the fault. It can be used as a set of checkpoints for future rollback if a fault occurs. We define a log of a molecular system as a copy of the chemical concentrations of each critical system variable. That is, we record a copy of the concentration of any species determined to be essential to the system behavior.
We present two logging devices. The first device receives an input signal, from an external user or another system, and records the concentrations of any monitored signals. The second device only records the system state if it is deemed “valid.” To that end, we define validity properties over sys- tem states using concentration bounds and logical operators, AND, OR, and NOT. We utilize validity detectors to determine when each monitored signal meets various concentration bounds. We then utilize a validity gate to ensure that the set of monitored signals satisfies the state validity property.
1Samuel J. Ellis, James I. Lathrop, and Robyn R. Lutz. 2017. State Logging in Chemical Reaction Networks. In Proceedings of ACM NanoCom ’17, Washington D.C., DC, USA, September 27-29, 2017, 6 pages.
We verify the correctness and accuracy of the logging devices through formal proofs about their system behavior. We provide formal analysis for each component using the ordinary differential equations that model the behavior of their chemical reaction networks. We show that each device will robustly and correctly log the system state given a log request.
This research was supported in part by National Science Foundation Grants 1247051 and 1545028. An earlier version of this work was presented at ACM NanoCom 2017.