There have been many analysis methods proposed for the verification of safety properties of real-time systems. Most of these methods, however, are not powerful enough for complex and safety-critical real-time systems due mainly to the lack of language primitives for specifying complex requirements (e.g., ESM) or heuristic verification procedures that do not provide verification results with certainty (e.g., Statechart and Modechart). A new approach for the verification of safety properties of real-time systems is introduced. This approach adopts Statechart to specify real-time systems behaviors. The authors redefined the step semantics of Statechart to address the problems of the synchrony hypothesis inherent to the original step semantics. A operational semantics of Statechart is defined based on the step semantics and a verification method for safety properties is developed based on the operational semantics of Statechart. This method verifies safety properties using a reachability graph derived from a Statechart diagram. They did not sacrifice the practicality or expressive power of Statechart for the simplification of analysis. Useful event and action primitives including the timeout event tm() and scheduled-action sc!() are included in the analysis. A train gate system is used as an example to illustrate the concepts in the paper.

Areasof computer application are being broadened rapidly due to the rapid improvement of the performance of computer hardware.Applications that were not feasible before are now becoming feasible with

Areas of computer application are being broadened rapidly due to the rapid improvement of the performance of computer hardware. This results in increased demands for computer applications that are large and have complex temporal characteristics. This paper introduces a real-time systems anlaysis method named PARTS. PARTS supports analyses from two viewpoints: external viewpoint, a view of the system from the user's perspective, and internal viewpoint, a view from the developer's perspective. These viewpoints are specified using formal languages, which are Real-Time Events Trace (RTET) for the external viewpoint, and Time Enriched Statechart (TES) and PARTS Data Flow Diagram (PDFD) for the internal viewpoint. All PARTS languages are based on the Metric Temporal Logic (MTL), and consistency of the specifications made from the two different viewpoints are analyzed based on the same MTL formalism.

Areas of computer application are being broadened rapidly due to the rapid improvement of the performance of computer hardware. This results in increased demands for computer applications that are large and have complex temporal characteristics. This paper introduces a real-time systems analysis method named PARTS. PARTS supports analyses from two viewpoints: external viewpoint, a view of the system from the user's perspective, and internal viewpoint, a view from the developer's perspective. These viewpoints are specified using formal languages, which are: Real-Time Events Trace (RTET) for the external viewpoint, and Time Enriched Statechart (TES) and PARTS Data Flow Diagram (PDFD) for the internal viewpoint. All PARTS languages are based on the Metric Temporal Logic (MTL), and consistency of the specifications made from the two different viewpoints are analyzed based on the same MTL formalism.>