This RUI research project studies the issue of specification and verification of computer systems that are both delay-sensitive and distributed. The behaviors of such a system strongly depend upon the timing sequences of events, and failure to meet these timing requirements can either cause severe consequences or affect the correctness and/or performance of the system. Due to the extra dimension of complexity introduced by the time components in these systems, specification and verification of delay-sensitive distributed systems have presented a unique challenge to software practitioners. This project studies a broad range of issues related to specifying and verifying delay-sensitive distributed systems. A new specification model, Time Communicating Finite State Machines (TCFSMs), is proposed. TCFSMs is based on the classical CFSMs model with capability added to express time constraints for specifying and verifying delay sensitive distributed systems. A token passing-based system is studied to demonstrate how to concisely specify and verify self-stabilizing systems with TCFSMs. This research examines a broad spectrum of problems related to TCFSMs: the semantics and alternative semantics of TCFSMs and their effects on applications and efficiencies; methodologies for synthesizing time constraints in TCFSMs; new verification techniques for TCFSMs extending symbolic timing verification techniques; methodologies for modeling self-stabilizing distributed systems with TCFSMs, suitable formalisms for self-stabilization and special classes of TCFSMs that can be efficiently self-stabilized; alternative extensions of TCFSMs related to other popular specification models; and TCFSMs-based tools for simulations and rapid prototyping. A component of this RUI project is th e comparison of TCFSMs with other specification models to identify and evaluate their strengths and weaknesses.
