A synchronous observer is an adjunct to a system model that monitors its state variables and raises a signal when some condition is satisfied. Synchronous observers provide an alternative to temporal logic as a means to specify safety properties but have the benefit that they are expressed in the same notation as the system model. Model checkers that do use temporal logic can nonetheless employ synchronous observers by checking for properties such as “never (signal raised).”
The use of synchronous observers to specify properties is well-known; rather less well-known is that they can be used to specify assumptions and axioms, to constrain models, and to specify test cases. The idea underlying all these applications is that the basic model generates more behaviors than are desired, the synchronous observer recognizes those that are interesting, and the model checker is constrained to just the interesting cases. The value in this approach is that it is usually much easier to write recognizers than generators. The approach is best exploited in languages such as SAL that provide explicit first class operators for synchronous and asynchronous composition.
The paper describes and illustrates these applications of synchronous observers.
John Rushby
SRI Author
Safety Envelope for Security
We present an approach for detecting sensor spoofing attacks on a cyber-physical system. Our approach consists of two steps. In the first step, we construct a safety envelope of the system. Under nominal conditions (that is, when there are no attacks), the system always stays inside its safety envelope. In the second step, we build an attack detector: a monitor that executes synchronously with the system and raises an alarm whenever the system state falls outside the safety envelope. We synthesize safety envelopes using a modifed machine learning procedure applied on data collected from the system when it is not under attack. We present experimental results that show effectiveness of our approach, and also validate the several novel features that we introduced in our learning procedure.
Logic and Epistemology in Safety Cases
SRI Authors: John Rushby
