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

Latest revision as of 05:47, 30 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.
TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.

Revision as of 00:43, 14 August 2021 (view source) Benkoo (talk \| contribs) (Created page with "#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 more expressive to...")		Latest revision as of 05:47, 30 August 2021 (view source) KevinTung (talk \| contribs)
(5 intermediate revisions by the same user not shown)
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 automatic tools to prove the system is required.
	#~~Mathematics~~ is ~~more expressive to model system~~ and ~~independent of the order of execution~~.		#TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.