Hierarchical Design Support Method of Real-time Systems Based on Assume-Guarantee Verification

摘要

In many cases, communication systems and control systems are reactive real-time systems. As designing real-time systems is complex for real-time properties ad reactivity, it is difficult to guarantee their qualities. In designing real-time systems, the hierarchical design method is important and verifying whether lower levels satisfy upper levels or not is important, too. In this paper, we propose the hierarchical design method based on uniform specification tech- niques and Assume-Guarantee verification. Finally, we show the proposed method is effective by some example.