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

Revision as of 05:43, 28 August 2021

To analyze a system correctly before it is implemented, 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.

Revision as of 05:37, 28 August 2021 (view source) KevinTung (talk \| contribs) m (KevinTung moved page TLA Workflow/Context to PKC Workflow/TLA Workflow/Context) ← Older edit		Revision as of 05:43, 28 August 2021 (view source) KevinTung (talk \| contribs) Newer edit →
Line 1:		Line 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.		#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.
	#Mathematics is ~~more~~ expressive to model ~~system~~ and independent of the order of execution.		#Mathematics is expressive to the model systems and independent of the order of execution.