Difference between revisions of "PKC Workflow/Software"
Jump to navigation
Jump to search
(Created page with "== TLA+ == === Introduction === === Application on PKC === === Workflow === === Discussion ===") |
(→Notes) |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
== TLA+ == | == TLA+ == | ||
=== Introduction === | === Introduction === | ||
TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code. <ref>https://lamport.azurewebsites.net/tla/tla.html</ref> | |||
* Since not all system can be modeled by a function, like an operating system, a program can be modeled by its behavior. | |||
* A program's execution can be represented by a behavior | |||
* A behavior is a sequence of states. | |||
* A state is an assignment of values to variables. | |||
* A program is modeled by a set of behaviors. | |||
=== Application on PKC === | === Application on PKC === | ||
To model the PKC system, a set of variables to represent state and the constraints are required in order to check its liveness and safety. | |||
=== Workflow === | === Workflow === | ||
* [https://lamport.azurewebsites.net/tla/tla.html Download TLA+] | |||
* [[PKC System Invariants|Define safety and liveness properties]] | |||
* Run TLA+ to check whether the system fits the invariants. | |||
=== Notes === | |||
=== | [[Video:Tackling Concurrency Bugs with TLA+" by Hillel Wayne]][https://www.youtube.com/watch?v=_9B__0S21y8] | ||
Unit test cannot fix the problem of potential bugs because the complexity of a system is high. | |||
Latest revision as of 14:34, 19 July 2021
TLA+
Introduction
TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code. [1]
- Since not all system can be modeled by a function, like an operating system, a program can be modeled by its behavior.
- A program's execution can be represented by a behavior
- A behavior is a sequence of states.
- A state is an assignment of values to variables.
- A program is modeled by a set of behaviors.
Application on PKC
To model the PKC system, a set of variables to represent state and the constraints are required in order to check its liveness and safety.
Workflow
- Download TLA+
- Define safety and liveness properties
- Run TLA+ to check whether the system fits the invariants.
Notes
Video:Tackling Concurrency Bugs with TLA+" by Hillel Wayne[1] Unit test cannot fix the problem of potential bugs because the complexity of a system is high.