Directed by: David C. Kung and Bill Carroll
Funded by: Texas Advanced Research Program
The overall objectives of this research are: 1) to invent an object-oriented (OO) modeling and specification methodology for real time systems; 2) to invent a proof system for formally verifying that a model satisfies desired timed temporal properties; and 3) to validate the research results through applications to realistic case studies. Existing researches in real time systems specification and verification have several limitations: 1) most researches are meant for the conventional function-oriented paradigm, they cannot be easily adapted to the OO paradigm; 2) most researches are content with event and/or timing modeling and analysis, ignoring object modeling and application modeling; and 3) most reseaches deal with either temporal aspect modeling or time modeling, but not both; 4) most researches use a simulation approach that covers only the simulated cases and hence the system so built is not safe. The proposed research will produce an innovative approach to OO real time systems modeling and analysis. It will support informal specification, integrated object modeling, system/subsystem modeling, object temporal behavior modeling, and timing requirements modeling. A stepwise methodology based on the principle of separation of concerns will be invented to reduce the complexity of each of the modeling steps. Algorithms for converting an informal specification to a timed temporal logic (TTL) language for formal reasoning and the reasoning system will be invented, prototyped, and validated through scalable case studies. The proposed research will enhance our understanding of the OO philosophy and the mathematical basis for specifying and reasoning OO real time systems. It is expected to discover effective and efficient ways to specify, verify, and test such systems.