it is not a specific software reliability problem that TLA+ would be
limited to. You use it to model a _behavior_ which is just a sequence of
_states_. Each state consists of _variables_ and these can have
different _values_ in each state. To specify the behaviors you define
which starting states are acceptable and which transitions (_actions_ in
TLA+) can be taken if a behavior is to be accepted. Then you can state
properties that you think would be true in each behavior (or in each
state). Properties that capture that "nothing bad will happen" are
called safety properties, those that capture "something good will
eventually happen" are called liveness properties. A property that must
be true in each state of any behavior that your specification allows in
called an invariant. If you are specifying a sorting algorithm on an
array you may want to state as an invariant that the elements in the
array viewed as a multiset does not change. Aside from invariants you
can also state properties that you think the entire behavior satisfies.
You then have a tightly integrated model checker available that allows
you to exhaustively check these properties on finite, - model -
behaviors. This gives you a good level of confidence that your
understanding of the behavior resulting from your specification is
correct or it leads you to the issues where your understanding is
lacking. For even higher confidence you could then rigorously prove that
all behaviors (not only the model) allowed by your specification have
the property you want.
Hope this helps and best regards,
Priya Patel <priyab...@gmail.com
> I am just started working with TLA+. I want to know when we use TLA+? what
> software reliability problems it can detect or solve?
> On Wednesday, June 12, 2019 at 9:12:12 PM UTC-4, AmirHossein wrote:
>> Please elaborate on your specific question.
>> On Thu, Jun 13, 2019 at 12:53 AM Priya Patel <priyab...@gmail.com
>>> What are alternatives to achieve similar guarantees?
>>> You received this message because you are subscribed to the Google Groups
>>> "tlaplus" group.
>>> To unsubscribe from this group and stop receiving emails from it, send an
>>> email to tla...@googlegroups.com
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3d01141a-4ae7-458d-aa02-c4f74bfb4159%40googlegroups.com
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681