PKC Workflow/System Verification by TLA+

From PKC
Jump to navigation Jump to search

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"