what software reliability problem TLA+ is solving?
49 views
Skip to first unread message
Priya Patel
Jun 12, 2019, 4:23:39 PM6/12/19
to tlaplus
What are alternatives to achieve similar guarantees?
Amir A.H.S.A
Jun 12, 2019, 9:12:12 PM6/12/19
to tla...@googlegroups.com
Please elaborate on your specific question.
AmirHossein
On Thu, Jun 13, 2019 at 12:53 AM Priya Patel <priyab...@gmail.com> wrote:
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 tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4070df7d-9b57-4d73-8588-e1691f77db6c%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Priya Patel
Jun 13, 2019, 10:24:29 AM6/13/19
to tlaplus
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.AmirHossein
On Thu, Jun 13, 2019 at 12:53 AM Priya Patel <priyab...@gmail.com> wrote:
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.
Marko Schuetz-Schmuck
Jun 13, 2019, 11:36:36 AM6/13/19
to Priya Patel, tlaplus
Dear Priya,
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,
Marko
Priya Patel <priyab...@gmail.com> writes:
> 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.
>>
>> AmirHossein
>>
>>
>> On Thu, Jun 13, 2019 at 12:53 AM Priya Patel <priyab...@gmail.com
>> <javascript:>> wrote:
>>
>>> 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 <javascript:>.
>>> .
--
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681
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,
Marko
Priya Patel <priyab...@gmail.com> writes:
> 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.
>>
>> AmirHossein
>>
>>
>> On Thu, Jun 13, 2019 at 12:53 AM Priya Patel <priyab...@gmail.com
>> <javascript:>> wrote:
>>
>>> 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
>>> To post to this group, send email to tla...@googlegroups.com
>>> <javascript:>.
>>> Visit this group at https://groups.google.com/group/tlaplus.
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/tlaplus/4070df7d-9b57-4d73-8588-e1691f77db6c%40googlegroups.com
>>> <https://groups.google.com/d/msgid/tlaplus/4070df7d-9b57-4d73-8588-e1691f77db6c%40googlegroups.com?utm_medium=email&utm_source=footer>
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/tlaplus/4070df7d-9b57-4d73-8588-e1691f77db6c%40googlegroups.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.
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3d01141a-4ae7-458d-aa02-c4f74bfb4159%40googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
--
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681
Amir A.H.S.A
Jun 13, 2019, 10:25:58 PM6/13/19
to tla...@googlegroups.com
We hereby welcome you to the TLA+ community.
TLA+ is a formal "specification" language.
A specification is a written description of what a "system" is supposed to do.
Any digital system (an algorithm, a hardware circuitry or software systems) can be specified precisely in TLA+.
Once a system is specified precisely, there is the "TLC Model Checker" that we can use to better understand the correctness of our specification.
There is much fun possible when playing with systems and TLA+.
I suggest you begin either by studying the reference book or by attending the video course online, for which the hyperlinks are given below.
Specifying Systems Book: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
Video course: http://lamport.azurewebsites.net/video/videos.html
Best Regards,
AmirHossein
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3d01141a-4ae7-458d-aa02-c4f74bfb4159%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages