TLA+ is a general purpose, formal specification language based on the Temporal Logic of Actions, with no built-in primitives for specifying real-time properties. Here, we use TLA+ to define operators for specifying the temporal behavior of physical components obeying integral equations of evolution. These operators, together with previously defined operators for describing timing constraints, are used to specify a toy gas burner introduced by Ravn, Rischel, and Hansen. The burner is specified at three levels of abstraction, each of the two lower-level specifications implementing the next higher-level one. Correctness proofs are sketched.
CITATION STYLE
Lamport, L. (1993). Hybrid systems in TLA+ (pp. 77–102). https://doi.org/10.1007/3-540-57318-6_25
Mendeley helps you to discover research relevant for your work.