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).