• Skip to primary navigation
  • Skip to main content
SRI logo
  • About
    • Press room
    • Our history
  • Expertise
    • Advanced imaging systems
    • Artificial intelligence
    • Biomedical R&D services
    • Biomedical sciences
    • Computer vision
    • Cyber & formal methods
    • Education and learning
    • Innovation strategy and policy
    • National security
    • Ocean & space
    • Quantum
    • QED-C
    • Robotics, sensors & devices
    • Speech & natural language
    • Video test & measurement
  • Ventures
  • NSIC
  • Careers
  • Contact
  • 日本支社
Search
Close
Information & computer science publications September 1, 2014 Article

The Versatile Synchronous Observer

SRI Authors: John Rushby

Citation

Copy to clipboard


Rushby, J. (2014). The versatile synchronous observer. Lecture Notes in Computer Science, 8373, 110-128.

Abstract

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.

↓ View online

Share this

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you.

Expect a response within 48 hours.

Career call to action image

Make your own mark.

Search jobs

Our work

Case studies

Publications

Timeline of innovation

Areas of expertise

Institute

Leadership

Press room

Media inquiries

Compliance

Careers

Job listings

Contact

SRI Ventures

Our locations

Headquarters

333 Ravenswood Ave
Menlo Park, CA 94025 USA

+1 (650) 859-2000

Subscribe to our newsletter


日本支社
SRI International
  • Contact us
  • Privacy Policy
  • Cookies
  • DMCA
  • Copyright © 2022 SRI International