Search

Communicating real-time state machines (CRSM's) are a new, complete, and executable notation for specifying concurrent real-time systems including the monitored and controlled physical environment. They are essentially state machines that communicate synchronously in a manner much like the input-output in Hoare's CSP. In addition, CRSM's have a novel and small set of facilities for describing timing properties and accessing real time. The paper defines the CRSM language, gives many examples of its use in requirements specification, outlines an algorithm for executing or simulating CRSM's, introduces some techniques for reasoning about the specifications, and discusses some open problems and issues. [ABSTRACT FROM AUTHOR]

A methodology for specifying and proving assertions about time in higher-level language programs is described. The approach develops three ideas: the distinction between, and treatment of, both real-time and computer times; the use of upper and lower bounds on the execution times of program elements; and a simple extension of Hoare logic to include the effects of the passage of real-time. Schemas and examples of timing bounds and assertions are presented for a variety of different statement types and programs, such as conventional sequential programs including loops, time-related statements such as delay, concurrent programs with synchronization, and software in the presence of interrupts. Examples of assertions that are proven include deadlines, timing invariants for periodic processes, and the specification of time-based events such as those needed for the recognition of single and double clicks from a mouse button. [ABSTRACT FROM AUTHOR]

Flow expressions describe sequential and concurrent flows of entities, such as control, messages, commands, jobs, and resources, through system software components, such as programs, procedures, modules, and processes. They consist of regular expressions extended with cyclic and interleaving operators and a synchronization facility. The language of flow expressions is defined and some of its formal properties are presented. Applications are exhibited in the modeling of concurrent programs, the description of operating system architectures, the specification and solution of synchronization problems, the flow and description of command languages, and in systems analysis and verification. [ABSTRACT FROM AUTHOR]