摘要: TLA+ is a specification language for concurrent and reactive systems that combines the temporal logic TLA with full first-order ZF set theory. TLC new model checker debugging by checking invariance properties of finite-state specification. It accepts subclass specifications should include most descriptions real system designs. has been used engineers to find errors in cache coherence protocol Compaq multiprocessor. We describe their models, how works, our experience using it.
springer.com
core.ac.uk
researchgate.net 
sci-hub.st 参考文章(21)
Leslie Lamport, A Temporal Logic of Actions ,(2000)
Ralf Steinbrüggen, M. Broy, Calculational system design IOS Press. ,(1999)
Martín Abadi, Leslie Lamport, Stephan Merz, A TLA Solution to the RPC-Memory Specification Problem Formal Systems Specification, The RPC-Memory Specification Case Study (the book grow out of a Dagstuhl Seminar, September 1994). pp. 21- 66 ,(1996) , 10.1007/BFB0024426
R. P. Kurshan, Leslie Lamport, Verification of a Multiplier: 64 Bits and Beyond computer aided verification. pp. 166- 179 ,(1993) , 10.1007/3-540-56922-7_14
Edmund M. Clarke, E. Allen Emerson, DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC 25 Years of Model Checking. ,vol. 131, pp. 196- 215 ,(2008) , 10.1007/978-3-540-69850-0_12
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
Ulrich Stern, David L. Dill, Using Magnatic Disk Instead of Main Memory in the Murphi Verifier computer aided verification. pp. 172- 183 ,(1998) , 10.1007/BFB0028743
David L. Dill, The Murphi Verification System computer aided verification. pp. 390- 393 ,(1996)
J. P. Queille, J. Sifakis, Specification and verification of concurrent systems in CESAR Proceedings of the 5th Colloquium on International Symposium on Programming. pp. 337- 351 ,(1982) , 10.1007/3-540-11494-7_22
Susan Owicki, David Gries, Verifying properties of parallel programs Communications of the ACM. ,vol. 19, pp. 279- 285 ,(1976) , 10.1145/360051.360224