Mocking Temporal Logic

Gordon, Colin S.

SPLASH-E, October 2024, doi: 10.1145/3689493.3689980

pdf doi acm youtube

Abstract

Temporal logics cover important classes of system specifications dealing with system behavior over time. Despite the prevalence of long-running systems that accept repeated input and output, and thus the clear relevance of temporal specifications to training software engineers, temporal logics are rarely taught to undergraduates. We motivate and describe an approach to teaching temporal specifications and temporal reasoning indirectly through teaching students about \emph{ mocking dependencies}, which is widely used in software testing of large systems (and therefore of more obvious relevance to students), less notationally intimidating to students, and still teaches similar reasoning principles. We report on 7 years of experience using this indirect approach to behavioral specifications in a software quality course.

Bibtex

@inproceedings{splashe24,
	author = {Gordon, Colin S.},
	title = {Mocking Temporal Logic},
	abbr = {SPLASH-E},
	booktitle = {SPLASH-E},
	year = {2024},
	address = {Pasadena, California, USA},
	month = {October},
	doi = {10.1145/3689493.3689980},
	bibtex_show = {true},
	youtube = {https://youtu.be/oS-WwQY7Bw4},
	acm = {https://dl.acm.org/doi/10.1145/3689493.3689980},
	abstract = { Temporal logics cover important classes of system
	            specifications dealing with system behavior over time. Despite
	            the prevalence of long-running systems that accept repeated input
	            and output, and thus the clear relevance of temporal
	            specifications to training software engineers, temporal logics
	            are rarely taught to undergraduates. We motivate and describe an
	            approach to teaching temporal specifications and temporal
	            reasoning indirectly through teaching students about \emph{
	            mocking dependencies}, which is widely used in software testing
	            of large systems (and therefore of more obvious relevance to
	            students), less notationally intimidating to students, and still
	            teaches similar reasoning principles. We report on 7 years of
	            experience using this indirect approach to behavioral
	            specifications in a software quality course. },
}