Timing Verification for Distributed Real-Time Systems

• Main Authors: Fu Jih-Ming, 傅日明
• Other Authors: Chen Sao-Jie
• Format: Others
• Language: en_US
• Published: 2001
• Online Access: http://ndltd.ncl.edu.tw/handle/37597876075110402447

博士 === 國立臺灣大學 === 電機工程學研究所 === 89 === Currently, most of commercial tools and methodologies for hardware-software codesign of distributed real-time systems support only validation techniques in the form of cosimulation, testing, and rapid prototyping of system design results. The results of hardware-software codesign of distributed real-time systems are often not verified, because traditional validation techniques like simulation and testing are neither sufficient nor viable to verify their correctness. Formal methods are becoming a practical alternative to ensure the correctness of designs. In this Dissertation, a formal verification methodology based on the linear hybrid automata and timed automata models is proposed. An algorithm is given for automatically converting the codesign results of distributed real-time systems to a linear hybrid automata or timed automata framework. Our verification approach allows automatic verification of real-time constraints such as hard deadlines. Another advantage is that the proposed approach is suitable for verifying multiprocessor systems with arbitrary communication patterns and system architecture. The feasibility of our approach is demonstrated through several application examples. The proposed approach has also been successfully used in verifying deadline violations when there are inter-task communications between tasks with different period lengths. Besides the main methodology, the issue of state-space explosion encountered in formal verification is also addressed. Techniques for reducing state-space sizes are adapted for timing verification. It is shown how scheduling besides being a design technique for distributed real-time systems can also be used for reducing state-spaces in timing verification. Further, the state-space reduction technique of hiding inactive clocks in a state-space representation is also useful in increasing verification scalability.