Difference between revisions of "PKC Workflow/Software"
Jump to navigation
Jump to search
| Line 12: | Line 12: | ||
=== Workflow === | === Workflow === | ||
[https://lamport.azurewebsites.net/tla/tla.html Download TLA+] | * [https://lamport.azurewebsites.net/tla/tla.html Download TLA+] | ||
[[PKC System Invariants|Define safety and liveness properties]] | * [[PKC System Invariants|Define safety and liveness properties]] | ||
Run TLA+ to check whether the system fits the invariants. | * Run TLA+ to check whether the system fits the invariants. | ||
=== Notes === | === Notes === | ||
Revision as of 14:33, 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, b.c. the complexity is high. Type system fallacy: rely on other language?