The purpose is to develop a language and methodology for specifying the requirements and design of concurrent distributed real-time systems, including the monitored and controlled physical environment. A new, complete, and executable notation, called communicating real-time state machines (CRSM), is proposed as a basis. They are essentially state machines that communicate synchronously over one-directional channels; in addition, CRSM has a novel and small set of facilities for describing timing properties and for accessing real time. The research consists of five related parts. The first is to define further and implement the basic CRSM model. Another is to develop a structuring scheme that permits the composition of machines and their parts into higher level entities. A third is to design a methodology that combines the state-based CRSM approach with an object-oriented model. A fourth part of the research is to develop formal reasoning methods and tools, for proving and testing assertions about specifications. Lastly, specification experiments will be performed on some substantial applications.
