The Versatile Synchronous Observer

  • John Rushby
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


A synchronous observer is an adjunct to a system model that monitors its state variables and raises a signal flag when some condition is satisfied. Synchronous observers provide an alternative to temporal logic as a means to specify safety properties but have the advantage that they are expressed in the same notation as the system model—and thereby lower the mental hurdle to effective use of model checking and other techniques for automated analysis of system models. Model checkers that do use temporal logic can nonetheless employ synchronous observers by checking for properties such as “never(flag 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 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 efficiency in this approach is that it is usually much easier to write recognizers than generators.

The paper describes and illustrates several applications of synchronous observers.


Model Checker Temporal Logic Safety Property Hybrid Automaton Liveness Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE. IEEE Transactions on Software Engineering 18, 785–793 (1992)CrossRefzbMATHGoogle Scholar
  2. 2.
    Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Algebraic Methodology and Software Technology (AMAST 1993). Workshops in Computing, pp. 83–96. Springer, Enschede (1994)CrossRefGoogle Scholar
  3. 3.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: International Conference on Software Engineering, pp. 411–420. IEEE Computer Society, Los Angeles (1999)Google Scholar
  4. 4.
    SAL home page,
  5. 5.
    McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) Advances in Hardware Design and Verification: IFIP WG10.5 International Conference on Correct Hardware Design and Verification Methods (CHARME 1999). LNCS, vol. 1703, pp. 342–346. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Rushby, J.: Formal verification of McMillan’s compositional assume-guarantee rule. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (2001)Google Scholar
  7. 7.
    Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. International Journal on Software Tools for Technology Transfer 4, 224–233 (2003)CrossRefzbMATHGoogle Scholar
  8. 8.
    Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 686–702. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Tiwari, A.: HybridSAL relational abstracter. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 725–731. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  10. 10.
    Bass, E.J., Feigh, K.M., Gunter, E., Rushby, J.: Formal modeling and analysis for interactive hybrid systems. In: Fourth International Workshop on Formal Methods for Interactive Systems: FMIS 2011, Limerick, Ireland. Electronic Communications of the EASST, vol. 45 (2011)Google Scholar
  11. 11.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98, 142–170 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    de Moura, L., Rueß, H.: Lemmas on demand for satisfiability solvers. In: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002), Cincinnati, OH (2002)Google Scholar
  13. 13.
    de Moura, L., Rueß, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 438–455. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    Rushby, J.: New challenges in certification for aircraft software. In: Baruah, S., Fischmeister, S. (eds.) Proceedings of the Ninth ACM International Conference On Embedded Software: EMSOFT, pp. 211–218. Association for Computing Machinery, Taipei (2011)CrossRefGoogle Scholar
  15. 15.
    Rushby, J.: A safety-case approach for certifying adaptive systems. In: AIAA Infotech@Aerospace Conference, Seattle, WA. American Institute of Aeronautics and Astronautics, AIAA paper 2009-1992 (2009)Google Scholar
  16. 16.
    Schlichting, R.D., Schneider, F.B.: Fail-stop processors: An approach to designing fault-tolerant computing systems. ACM Transactions on Computer Systems 1, 222–238 (1983)CrossRefGoogle Scholar
  17. 17.
    Rushby, J.: Composing safe systems. In: Arbab, F., Ölveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 3–11. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  18. 18.
    Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC/FSE 1999. LNCS, vol. 1687, pp. 146–162. Springer, Heidelberg (1999)Google Scholar
  19. 19.
    Hamon, G., de Moura, L., Rushby, J.: Generating efficient test sets with a model checker. In: 2nd International Conference on Software Engineering and Formal Methods (SEFM), Beijing, China, pp. 261–270. IEEE Computer Society (2004)Google Scholar
  20. 20.
    Hamon, G., de Moura, L., Rushby, J.: Automated test generation with SAL. Technical note, Computer Science Laboratory, SRI International, Menlo Park, CA (2005),
  21. 21.
    IEEE Standard 1850–2010: Property Specification Language, PSL (2010)Google Scholar
  22. 22.
    IEEE Standard 1800–2012: SystemVerilog—Unified Hardware Design, Specification, and Verification Language (2012)Google Scholar
  23. 23.
    Littlewood, B., Rushby, J.: Reasoning about the reliability of diverse two-channel systems in which one channel is “possibly perfect”. IEEE Transactions on Software Engineering 38, 1178–1194 (2012)CrossRefGoogle Scholar
  24. 24.
    Rushby, J.: The versatile synchronous observer (abstract only). In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol. 7498, p. 1. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • John Rushby
    • 1
  1. 1.Computer Science LaboratorySRI InternationalMenlo ParkUSA

Personalised recommendations