| auxiliary constructs for proving liveness in compassion discrete systems |
| Long Teng; Zhang Wenhui
|
| 2010
|
| 会议名称 | 8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010
|
| 会议录名称 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
|
| 页码 | 276-290
|
| 会议日期 | September
|
| 会议地点 | Singapore, Singapore
|
| 收录类别 | EI
|
| 出版地 | Germany
|
| ISSN | 3029743
|
| ISBN | 3642156428
|
| 部门归属 | (1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (2) School of Information Science and Engineering, Graduate University, China Academy of Sciences, Beijing, China
|
| 摘要 | 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. © 2010 Springer-Verlag Berlin Heidelberg. |
| 主办者 | National University of Singapore
|
| 内容类型 | 会议论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/8678
|
| 专题 | 基础软件与系统重点实验室
|
推荐引用方式
GB/T 7714 |
Long Teng,Zhang Wenhui. auxiliary constructs for proving liveness in compassion discrete systems[C]. Germany,2010:276-290.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论