Improving model checking stateful timed CSP with non-zenoness through clock-symmetry reduction

• Main Authors: SI, Yuanjie, SUN, Jun, LIU, Yang, WANG, Ting
• 格式: text
• 語言: English
• 出版: Institutional Knowledge at Singapore Management University 2013
• 主題: Model Check; Label Transition System; Symmetry Reduction; Strongly Connected Component; Time Automaton; Software Engineering
• 在線閱讀: https://ink.library.smu.edu.sg/sis_research/4998; https://ink.library.smu.edu.sg/context/sis_research/article/6001/viewcontent/improving_model.pdf
• 機構: Singapore Management University

Real-time system verification must deal with a special notion of ‘fairness’, i.e., clocks must always be able to progress. A system run which prevents clocks from progressing unboundedly is known as Zeno. Zeno runs are infeasible in reality and thus must be pruned during system verification. Though...