TY - JOUR
T1 - Taming distributed system complexity through formal patterns
AU - Meseguer, José
N1 - Funding Information:
I thank the organizers of FACS 2011 for giving me the opportunity of presenting these ideas in Oslo, and all the participants for their interest and comments. I thank the anonymous referees for their constructive criticism and their suggestions, which have all helped in improving the paper. Kyungmin Bae, Jonas Eckhardt, Tobias Mühlbauer, Camilo Rocha and Mu Sun deserve special thanks for their help with various pictures and diagrams in the paper. This work has been supported in part by the Boeing Corporation under Grant C8088-557395 , NSF Grants CNS 08-34709 , CCF 09-05584 , and AFOSR Grant FA8750-11-2-0084 .
PY - 2014/4/1
Y1 - 2014/4/1
N2 - 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.
AB - 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.
KW - Distributed systems
KW - Formal specification and verification
KW - Maude
KW - Rewriting logic
KW - Software patterns
UR - http://www.scopus.com/inward/record.url?scp=84894527885&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84894527885&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2013.07.004
DO - 10.1016/j.scico.2013.07.004
M3 - Article
AN - SCOPUS:84894527885
SN - 0167-6423
VL - 83
SP - 3
EP - 34
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -