DocumentCode :
517969
Title :
A probabilistic framework for fairness notions
Author :
Wang, Jinshuang ; Yang, Huabing ; Zhang, Ningrong
Author_Institution :
State Key Lab. for Novel Software Technol., Nanjing Univ., Nanjing, China
Volume :
2
fYear :
2010
fDate :
16-18 April 2010
Abstract :
Fairness is a convenient and popular tool when modelling and specifying concurrent systems, many fairness notions exist in the literature. However, there was no fully satisfactory abstract characterisation of fairness. In order to show fairness definitions are reasonable, a probabilistic framework for fairness notions was proposed, where concurrent systems were modelled inductively in the theorem prover Isabelle/HOL, and a general fairness notion was defined. It was shown that the set of fair infinite executions of concurrent systems has probability 1. Finally, the usage of this framework was argued. All formalisations and proofs have been carried out with Isabelle/HOL/Isar.
Keywords :
concurrency control; formal specification; probability; theorem proving; HOL; Isabelle; Isar; abstract characterisation; concurrent system specification; fairness notion; probabilistic framework; theorem prover; Computer languages; Concrete; Logic programming; Network address translation; Probabilistic logic; Programmable logic arrays; Safety; Software tools; Writing; Fairness; Probabilistic Framework; Theorem Proving; Verification;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Engineering and Technology (ICCET), 2010 2nd International Conference on
Conference_Location :
Chengdu
Print_ISBN :
978-1-4244-6347-3
Type :
conf
DOI :
10.1109/ICCET.2010.5485329
Filename :
5485329
Link To Document :
بازگشت