Taming distributed system complexity through formal patterns

• Solutions to frequently occurring problems in distributed systems can be made generic and reusable as formal patterns.
• Such formal patterns can greatly reduce the complexities of designing, verifying, and implementing a system.
• Formal patterns can be made executable in rewriting logic and come with semantic applicability conditions and formal guarantees.
• The paper defines the semantics of formal patterns and illustrates their usefulness in various cyber-physical, medical, and security applications.

Many distributed systems are real-time, safety-critical systems with strong qualitative and quantitative formal requirements. They often need to be reflective and adaptive, and may be probabilistic in their algorithms and/or their operating environments. All this makes these systems quite complex and therefore hard to design, build and verify. To tame such system complexity, this paper proposes formal patterns, that is, formally specified solutions to frequently occurring distributed system problems that are generic, executable, and come with strong formal guarantees. The semantics of such patterns as theory transformations in rewriting logic is explained; and a representative collection of useful patterns is presented to ground all the key concepts and show their effectiveness.