On Implementation of the Improved Assume-Guarantee Verification Method for Timed Systems
Hoang-Viet Tran, Quang-Trung Nguyen, Phạm Ngọc Hùng · 2019
The two-phase assume-guarantee verification method for timed systems using TL algorithm implemented in the learner has been known as a potential method to solve the problem of state space explosion in model checking thanks to its divide and conquer strategy. This paper presents three improvements to the verification method. First, we remove the untimed verification phase from the verification process. This removal reduces the time complexity of the verification process because of the great time complexity of this phase. Second, we introduce a maxbound to the equivalence queries answering algorithm implemented in the teacher which acts as a method for the teacher to return "don't know" results to the learner to prevent the verification process from many endless scenarios. Finally, we introduce a technique to analyze the counterexample received from the teacher and another one implemented in the equivalence queries answering algorithm which helps the teacher not return a counterexample that has been returned to the learner. This technique keeps the verification process from running forever in several circumstances. We give primitive experimental results for both two-phase assumption generation method and the improved one with some discussions in the paper.