PKC Workflow/Software
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?