Program Director, Formal Methods and Dependable Systems, Computer Science Laboratory
John Rushby, program director for Formal Methods and Dependable Systems at SRI International, works on automated methods for analyzing correctness properties of software designs. In this approach, designs are treated as logical formulas, and their properties are calculated using techniques from automated theorem proving.
Under his leadership for the last 15 years, the Formal Methods program in the Computer Science Laboratory is recognized worldwide as one of the leaders in this field, and has developed techniques and tools that are widely used in teaching and research. His own specialty is in the application of these methods to security and safety-critical systems and has been influential in their adoption by industry.
Rushby was named an SRI Fellow in 2004.
The paper describes and illustrates these applications of synchronous observers.
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. In…