4 ms·
SPIN has long been used for similar stuff in academia and industry. They have published a lot of their specs and results. http://spinroot.com/spin/whatispin.ht
by nickpsecurity 8y ago
SPIN has long been used for similar stuff in academia and industry. They have published a lot of their specs and results.
http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html
http://www.imm.dtu.dk/~albl/promela.html http://www.imm.dtu.dk/~albl/promela.html
There were many projects using Pi Calculus, too. One of my project ideas is something that converts TLA+ to SPIN and Pi Calculus to use their tools and works. Or just otherwise integrates them.
- Karrot_Kream 8y agoWhich model checkers use Pi Calculus? I've thought about learning Pi Calculus but an much less interested if there's no checker.
- pron 8y agoI don't think TLA+ is far too expressive to translate to Promela. There are, however, tools that translate subsets of TLA+ to ProB: https://www3.hhu.de/stups/prob/index.php/TLA https://www3.hhu.de/stups/prob/index.php/TLA