PKC Workflow/System Verification by TLA+/Process

From PKC
Jump to navigation Jump to search


Planning

As TLA+ is well-suited to model and verify a system, I think it has differences from other monitoring tools. These tools analyze the operational data(dynamic) to decide whether the system reach the desired status, while TLA+ analyzes the specification (static) before a system is running. To integrate with PKC, the Success Criteria is a good start as it can contain Criteria:Safety and Criteria:Liveness conditions. After we specified Success Criteria, we start designing the Process. The TLA+ can then verify the design after the process is specified. In order to bridge the success conditions with the design, we should describe the design from a proper perspective. After that, the code could be abstracted into states and states transformations. We can then use the TLC model checker to get the analysis of the specification.


BOOK/Specifying Systems Notes

A specification is a mathematical model of a particular view of some part of a system. When writing a specification, the first thing you must choose is exactly what part of the system you want to model.

It can be used to write a precise, formal description of almost any sort of discrete system. It’s especially well suited to describing asynchronous systems—that is, systems with components that do not operate in strict lock-step.

List of current TLA+ examples

Producer-Consumer example [1]

Take an example to show how success criteria bridge the code.


Logic Model (Producer-Consumer System) Template:LogicModel 08 29, 2021
Abstract Specification
Context The inherent non-determinism of concurrent systems results in bugs that occur extremely rarely and are not reproducible.
Goal A buffer holds the data created by producing threads until they are retrieved by consuming threads. The buffer acts as a synchronizer, blocking and suspending threads when there is nothing for them to do. When the buffer is empty, any consuming thread needs to be blocked until there is data in the buffer. Conversely, if the buffer has a finite capacity, producing threads must be suspended when the buffer is full.
Success Criteria
  • At least one producer
  • At least one consumer
  • No thread is both consumer and producer
  • Buffer capacity is at least 1
  • The type of data is nonempty


Concrete Implementation
Given Inputs When Process is executed... Then, we get Outputs
  • the (nonempty) set of producers
  • the (nonempty) set of consumers
  • the maximum number of messages in the bounded buffer
  • the set of values that can be produced and/or consumed
 A shared buffer in a system of producers and consumers
Boundary/Safety Conditions of Producer-Consumer System
Producer-Consumer System/Boundary 



 
EXTENDS Naturals, Sequences

CONSTANTS Producers,   (* the (nonempty) set of producers                           *)
          Consumers,   (* the (nonempty) set of consumers                           *)
          BufCapacity, (* the maximum number of messages in the bounded buffer      *)
          Data         (* the set of values that can be produced and/or consumed    *)

ASSUME /\ Producers # {}                      (* at least one producer *)
       /\ Consumers # {}                      (* at least one consumer *)
       /\ Producers \intersect Consumers = {} (* no thread is both consumer and producer *)
       /\ BufCapacity > 0                     (* buffer capacity is at least 1 *)
       /\ Data # {}                           (* the type of data is nonenpty *) 
...

Meta

  • Links are crucial to fill in the information and optimize a paragraph's structure
  • It could be useful to automatically recognize the information entity behind the natural language.
  • The quote of a pdf could be structured using annotation tools
  • [Decision point]: When naming Producer-Consumer System, it is difficult to decide whether to add the prefix of TLA Workflow/Process/Planning. If we do, then the page will be hidden in the hierarchy (though it could be solved by ignoring the hierarchical structure); if not, the page is lift up to the top with the context eliminated so we might need to add the context back in the logic model. In Namespace Management , it might be the correct way to think whether the page contains the context.
  • The intention primitive

Discussion

  • We can see that software and content becoming more indistinguishable as more content could be structured or formalized. For example, the Book/Provisional_Patent_Application#3.2/Conceptual Modules use fuzzy logic to translate each piece of opinion into a string of alpha-numeric text.
  • In AI field, researchers try to find the "right representation" which enable the machine to understand knowledge and perform more advanced knowledge task such as reasoning. The Logic model that we work on is currently not intended to express all the knowledge. Instead, it aims to provide a high-level abstraction of knowledge which helps the search for domain specific language.
  • Once a domain-specific language structures a domain well, then the domain is computable.
  • The strength of TLA+ is to enumerate all the states of a temporal system.
  • A knowledge engine could do inferencing and reasoning over knowledge. The corresponding language, such as rewrite system, type system, etc, will also be integrated in the future.


Retrieved from "https://pkc.pub/index.php?title=PKC_Workflow/System_Verification_by_TLA%2B/Process&oldid=10831"