Difference between revisions of "PKC Workflow/Software"
(Blanked the page) Tag: Blanking |
|||
| Line 1: | Line 1: | ||
== 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. <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 === | |||
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 === | |||
[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, b.c. the complexity is high. | |||
Type system fallacy: rely on other language? | |||
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?