无忧论文网
当前位置: 无忧论文网 > 自然科学论文 > 计算机科学论文 > JAVA论文 > Liveness and Fairness
点击提交论文指导需求
高薪诚聘老师
Liveness and Fairness
时间:2011-01-23 浏览次数:986次 无忧论文网
点击这里在线咨询我

1 Introduction

This note is devoted to liveness and progress properties. They are properties stating intuitively that “something good will eventually happens”. For instance, the absence of starvation for any of the dining philosophers in [1] is a liveness property and so is the possibility of being allowed to copy in the printer and scanner example also presented in [1].
We shall see how progress and liveness properties can be specified in the recursive extension of HML [1], however as it turns out, these kind of properties we must specify using minimal fixed points instead of as for safety properties using the maximal fixed points.
For illustration purposes, we shall use the classical example of readers and writers as our running example.
The examples of models to be run in MWB in this note are presented with emphasis on readability and may thus not compile due to extra line breaks.

References本论文由无忧论文网www.51lunwen.net整理提供
[1] J.C. Godskesen. Deadlocks and safety properties (version 1.2), 2005. Teaching notes, IT University of Copenhagen.
[2] B. Victor. The mobility workbench user’s guide, polyadic version 3.122. Technical report, SICS, Stockholm, Sweden, 1995.

关于我们 | 老师招聘 | 版权声明 | 联系我们 | 付款方式 | 返回顶部 | 

COPYRIGHT ©2001 - 2013 51LUNWEN.NET. ALL RIGHTS RESERVED.
【免责声明】:本网站所提供的信息资源如有侵权、违规,请及时告知
无忧论文网提供毕业论文指导 硕士论文指导服务