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

From PKC
Jump to navigation Jump to search
m (KevinTung moved page TLA Workflow to PKC Workflow/TLA Workflow)
 
(3 intermediate revisions by the same user not shown)
Line 1: Line 1:
A Model for TLA Workflow
A Model for System Verification
{{LogicModel | name=TLA Workflow}}
{{LogicModel | name=PKC Workflow/System Verification}}

Latest revision as of 18:07, 29 August 2021

A Model for System Verification

Logic Model (PKC Workflow/System Verification) Template:LogicModel 08 29, 2021
Abstract Specification
Context
  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.
Goal
  1. To state the system's preferred conditions and determine them.
Success Criteria
  1. The specified properties are determined.
Concrete Implementation
Given Inputs When Process is executed... Then, we get Outputs
  1. Software/TLA+ Tools
  2. PKC System Specification
  3. Knowledge/TLA+ Tools
  1. PKC System Result
  2. Producer-Consumer System example
Boundary/Safety Conditions of PKC Workflow/System Verification
  1. Determine what the PKC system should achieve.
  2. Finish within 1 week of time
Retrieved from "https://pkc.pub/index.php?title=PKC_Workflow/System_Verification_by_TLA%2B&oldid=10817"