PKC Workflow/System Verification by TLA+

A Model for System Verification

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