PARTS: A Temporal Logic-Based Real-Time Software Specification and Verification Method

摘要

Areas of 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 high-performance computers. This results in increased demands for computer applications that are large and have complex temporal characteristics. Most analysis methods available, however, cannot handle large, complex real-time systems adequately; They do not scale-up, lack formalism to represent complex features and perform analyses with mathematical rigor, do not support analyses from different viewpoints, or are too hard to learn and apply. TVe need analysis methods that support formal specification and verification of real-time systems. Incremental performance of specification and analysis of systems from different viewpoints (e.g., user, analyst ) must also be supported with languages appropriate for each different viewpoint and for the users involved. This paper introduces a real-time systems analysis method, named PARTS, that aims at providing above features. PARTS supports analyses from two viewpoints: external viewpoint, a view of the sys-Permission tern 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 Statecharts (TES) and PARTS Data Flow Diagram (PDFD) for the internal viewpoint. All PARTS languages are based on the Real-Time Temporal Logic (RTTL), and consistency of the specifications made from two different viewpoints are analyzed based on the same RTTL formalism. PARTS converts RTET and TES specifications to RTTL specifications, which are then integrated and analyzed for consistency. All of the PARTS specificaticm languages support the top-down strategy to handle complexity.