ABSTRACT
Real-world systems often depend on quantitative timing. Real-time systems differ from untimed systems in that their behavioral correctness relies not only on the results of their computations but also on when the results are produced. For instance, a pacemaker should not only function in the detection of an abnormal heart condition but it must also react within a small time framework.Modeling and verification of real-time systems are important research topics which have practical implications. System modeling is of great importance as well as highly nontrivial. The choice of modeling language is an important factor in the success of the entire system analysis or development. The language should cover several facets of the requirements and the model should reflect exactly (up to abstraction of irrelevant details) an existing system or a system to be built. The language should have a semantic model suitable to study the behaviors of the system and to establish the validity of desired properties. The latter is extremely important for real-time systems in order to avoid undecidability in system verification.
