REASONING ASSERTIONALLY ABOUT REAL-TIME SYSTEMS

We consider a real-time system defined by a set of programs that execu te concurrently on one ol more (hardware) processors and interact betw een themselves and with the environment. We show how to reason asserti onally about such real-time systems, using standard (non-real-time) as sertional techniques (i.e., Hoare-logic and lineal-history Temporal lo gic). The key step is to transform the set of programs to a state tran sition system, using ''epoch variables'' to model assumptions on state ment execution times, interprocessor communication times, scheduling p olicy, and allocation of programs to processors. Out method is illustr ated 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 que ry-handler that responds to queries from the environment by accessing the database. We model the system for two different program-to-process or allocations (dedicated processors and shared processors with priori ty scheduling). We prove that the system satisfies desired properties (e.g., bounded query response time and absence of buffer overflow).