Specifying and verifying real-time systems with timing uncertainty

Modeling timing behaviors of systems and verifying timing constraints again st the model are major tasks in developing real-time systems, However, it i s recognized to be extremely difficult to predict the timing behavior of sy stems precisely in the requirements phase. Timing uncertainty, if not consi dered properly in the modeling and verifying steps, may incur subtle, yet c ritical errors in final products. We propose a method of dealing with such timing uncertainty using an extended duration calculus formalism. The exten ded duration calculus, named fuzzy duration calculus, allows us to specify uncertain timing behavior of the system using the fuzzy theory. Semantics a nd proof system of the duration calculus are redefined in order to accommod ate fuzzy concepts. Based on the semantics and proof system, we can verify timing constraints against the system model. A portion of nuclear power pla nt (NPP) control system is employed to demonstrate the feasibility and the effectiveness of our approach. (C) 2000 Elsevier Science Inc. All rights re served.