Representation of a Discretely Controlled Continuous System in Tense Arithmetic
Tetsuya Mizutani, Shigeru Igarashi, Masayuki Shio · Electronic Notes in Theoretical Computer Science · 2001
Specifications for a vehicle control system, as an example of discretely controlled continuous systems, are represented and verified in a formal system called tense arithmetic for concurrent programs with rational number time. In this formalism, computational sequences are characterized, or indexed, by spurs that are generalizations of program schedulers and that are also temporal propositions. Our formalism describes analysis of the wake-up time of the next action from an observation time, and we obtain the actual rational time value for when the next action will occur. Additionally, we introduce the continuous variables with their first- and second-order derivatives, to analyze and verify programs that control discretely certain continuously physical or other external systems.