Auxiliary Constructs For Proving Liveness In Compassion Discrete Systems
ATVA'10: Proceedings of the 8th international conference on Automated technology for verification and analysis（2010）
摘要
For proving response properties in systems with compassion requirements, a deductive rule is introduced in [1]. In order to use the rule, auxiliary constructs are needed. They include helpful assertions and ranking functions defined on a well-founded domain. The work in [2] computes ranking functions for response properties in systems with justice requirements. This paper presents an approach which extends the work in [2] with compassion requirements. The approach is illustrated on two examples of sequential and concurrent programs.
更多查看译文
关键词
compassion requirement,response property,computes ranking function,deductive rule,ranking function,auxiliary construct,concurrent program,helpful assertion,justice requirement,well-founded domain,compassion discrete system
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要