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

Revision as of 18:07, 29 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.

Revision as of 06:31, 28 August 2021 (view source) KevinTung (talk \| contribs) m (KevinTung moved page PKC Workflow/TLA Workflow/Context to PKC Workflow/System Verification/Context) ← Older edit		Revision as of 18:07, 29 August 2021 (view source) KevinTung (talk \| contribs) Newer edit →
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~~.