Difference between revisions of "PKC Workflow/System Verification by TLA+/Context"

From PKC
Jump to navigation Jump to search
 
(3 intermediate revisions by the same user not shown)
Line 1: Line 1:
#To analyze a system correctly before it is implemented, [[TLA+|a language]] to model the system and [[Tools/TLC Model Checker|automatic tools]] to prove the system is required.
#To analyze a system correctly before it is implemented, [[TLA+|a language]] to model the system and automatic tools to prove the system is required.
#Mathematics is expressive to the model systems and independent of the order of execution.
#TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.

Latest revision as of 05:47, 30 August 2021

  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.
Retrieved from "https://pkc.pub/index.php?title=PKC_Workflow/System_Verification_by_TLA%2B/Context&oldid=10850"