Analysis and checking of controllable property transition system based on TLA+

In investigating concurrent system specification based on TLA+ (Lamport, 2002), the question of states transition and the properties and their correlation is a important branch. Always we check the properties of the concurrent system after system beginning transfer. But we thought to add the property into the transition system, that is to say the system has the property before transfer, and so the system has some properties from beginning to the end. For this purpose we bring forward some concepts, such as transition condition, controllable action, controllable state, and controllable property transition system, in addition we give a theorem and prove it. Then formalizing the Needham-Schroeder protocol and the Internet banking system based on TLA+ and checking them using TLC. The results show the theories are appropriate.