John Rushby

Presented at SAS 2014: Specification, Algebra, and Software, A Festschrift Symposium in Honor of Kokichi Futatsugi. Proceedings published as Springer LNCS vol. 8373, S. Iida, J. Meseguer, and K. Ogata (Eds.), pp. 110-128, April 2014

Abstract

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.

PDF

Slides

PDF

Citations from Google scholar

BibTeX Entry

@INPROCEEDINGS{Rushby:SAS14,
	AUTHOR = {John Rushby},
	TITLE = {The Versatile Synchronous Observer},
	BOOKTITLE = {Specification, Algebra, and Software,
		  A Festschrift Symposium in Honor of {Kokichi Futatsugi}},
        EDITOR = {S. Iida and J. Meseguer and K. Ogata},
	YEAR = 2014,
	PUBLISHER = {Springer-Verlag},
	ADDRESS = {Kanazawa, Japan},
	MONTH = apr,
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 8373,
	PAGES = {110--128}
}