Liveness Property Safety Rules of Multi-Action Based on TLA+
2010
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:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
5
References
0
Citations
NaN
KQI