DocumentCode
1984257
Title
Liveness Property Safety Rules of Multi-Action Based on TLA+
Author
Wan Liang ; Li Juntao ; Tang Zhengyi
Author_Institution
Inst. of Comput. Software & Theor., Guizhou Univ., Guiyang, China
fYear
2010
fDate
20-22 Aug. 2010
Firstpage
1
Lastpage
4
Abstract
In this paper, we put forward the definitions of safety transition system and the theorem which proof that every state in safety transition system is safe; Then we put forward safety multi-actor Liveness property rules under weak and strong fairness and prove them, the example of multi-user´s mutually exclusive action of drawing out in Internet bank based TLA+ to check the rules.
Keywords
Internet; safety systems; temporal logic; Internet; TLA+; liveness property safety rule; multiuser mutually exclusive action; safety transition system; Business; Cognition; Computer languages; Online banking; Safety; Semantics; Syntactics;
fLanguage
English
Publisher
ieee
Conference_Titel
Internet Technology and Applications, 2010 International Conference on
Conference_Location
Wuhan
Print_ISBN
978-1-4244-5142-5
Electronic_ISBN
978-1-4244-5143-2
Type
conf
DOI
10.1109/ITAPP.2010.5566605
Filename
5566605
Link To Document