Abstraction refinement for non-zeno fairness verification of linear hybrid automata

• Yanase Ryo

• 栁瀨 龍

抄録

金沢大学新学術創成研究機構

Linear hybrid automaton is a specification language for hybrid systems. For verification of hybrid systems, it is important to check fairness assumptions. For example, an embedded system keeps running forever when it starts to move by turning on the switch. Such a system has to be checked not only system safety but also fairness and non-Zenoness. The state space explosion is a fundamental problem in model checking, since it is a method that performs an exhaustive search of states. To avoid state space explosion problem in model checking, CEGAR (Counter Example Guided Abstraction Re?nement) is an effective technique. In this paper, we propose transition predicate abstraction and CEGAR verification algorithm for linear hybrid automata. © 2017 IEEE.

収録刊行物

• Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017

  Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017 2017-May 567-568, 2017-05-15

  Institute of Electrical and Electronics Engineers Inc.

詳細情報

• CRID: 1390290699937196800
• NII論文ID: 120006457641
• DOI: 10.24517/00050514
• Web Site: http://hdl.handle.net/2297/00050514
• 本文言語コード: en
• データソース種別:
  • JaLC
  • IRDB
  • CiNii Articles