Inter-Organizational Workflow

Abstract Specification
Context	This is the 2021 summer project of Tz-Chuang starting from June 27, 2021 to August 21,2021. Despite the various models for domain knowledge, there isn't a high-level model which is expressive, compact, practical, and independent of domains. This gives rise to Logic Model.
Goal	Utilize formal methods to prove the system's soundness Use Logic Model to describe the project itself. Theorize Logic Model based on the implementation.
Success Criteria	An example of how the formal method could integrate into Logic Model is demonstrated. The Logic Models of the project are defined correctly The core concepts which explain the Logic Model is defined.

Concrete Implementation
Given Inputs	When Process is executed...	Then, we get Outputs
System Verification Software/TLA+ Tools PKC System Specification Knowledge/TLA+ Tools Jenkins Integration Jenkins setup A service namespace Docker Registry Docker Docker registry tutorial Image Naming	System Verification by TLA+ Jenkins Integration Docker Registry Meeting and Communication Issues Updates All activities	PKC Workflow/Knowledge PKC Workflow/Drafts PKC Workflow/Project Conclusion PKC Workflow/Presentation

Boundary/Safety Conditions of PKC Workflow
6 weeks of project time.

Notes

When writing a logic model, one should be aware of the difference between concept and instance.
A logic model is composed of lots of submodels. When not intending to specify the abstract part of them, one could only use Function Model.
What is the relationship between the model submodules, and the relationships among all the subfunctions?
Note: Sometimes, the input and process are ambiguous. For example, the Service namespace is required to achieve the goal. It might be an input or the product along the process. In general, both the input and process contain uncertainty and need a decision.
The parameter of Logic Model is minimized to its name, which is the most important part of it. The name should be summarized from its value.
Note that, when naming as Jenkins, it means the resource itself, but when naming as Jenkin Implementation On PKC, it consists of more context information therefore is more suitable.