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

• المؤلفون الرئيسيون: 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...