Reasoning assertionally about real-time systems

We consider a real-time system defined by a set of programs that execute concurrently on one or more (hardware) processors and interact between themselves and with the environment. We show how to reason assertionally about such real-time systems, using standard (non-real-time) assertional techniques (i.e. Hoare-logic and linear-history temporal logic). The key step is to transform the set of programs to a state transition system, using “epoch variables” to model assumptions on statement execution times, interprocessor communication times, scheduling policy, and allocation of programs to processors. Our method is illustrated on a nontrivial example consisting of three concurrent programs: a sensor that buffers inputs from the environment, an integrator that periodically integrates the buffered inputs into a database, and a query-handler that responds to queries from the environment by accessing the database. We model the system for two different program-to-processor allocations (dedicated processors and shared processors with priority scheduling). We prove that the system satisfies desired properties (e.g. bounded query response time and absence of buffer overflow)