User Tools
start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
start [2017/08/30 21:46] jonathan |
start [2017/08/30 21:50] (current) jonathan |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| [[http://pvs.eecs.yorku.ca|http://pvs.eecs.yorku.ca]] | [[http://pvs.eecs.yorku.ca|http://pvs.eecs.yorku.ca]] | ||
| - | ====== TLA ====== | + | ====== TLA+ ====== |
| - | TLC is a so-called "explicit-state" model checker that computes the state space generated by your specification and can then verify (safety and liveness) properties fully automatically. Its main constraint is state space explosion: the size of the state space grows exponentially with the number of processes etc., and this leads to a corresponding increase in verification time. There are a number of techniques to push back the frontiers of what TLC can handle effectively, including using symbolic constants, symmetry reduction etc., but the most important one is for you to decide how big you need your model to be to have enough confidence in correctness. | + | |
| - | TLAPS is an interactive proof assistant: you provide a proof of why your system satisfies a property, and TLAPS can check if that proof is logically consistent and complete. It uses different automatic back-ends, including SMT solvers, to check proof steps, but it is still the user who designs and writes the proof. Although the effort is independent of the size of the state space, and also infinite-state systems can be verified in this way, I would not recommend using TLAPS for users who do not have sufficient experience with theorem proving. | + | TLA stands for the Temporal Logic of Actions. TLA+ is the TLA specification language and the PlusCal algorithm language, together with their associated tools. TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems. |
| [[http://tla.eecs.yorku.ca|http://tla.eecs.yorku.ca]] | [[http://tla.eecs.yorku.ca|http://tla.eecs.yorku.ca]] | ||
start.1504129608.txt.gz · Last modified: 2017/08/30 21:46 by jonathan
Page Tools
