PKC Workflow/System Verification by TLA+/Context

From PKC
Jump to navigation Jump to search
  1. To analyze a system correctly before it is implemented, a language to model the system and automatic tools to prove the system is required.
  2. TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.