Formal way to model or describe distributed systems architecture I've been tasked to create the systems architecture for a distributed system.

One approach to designing this system is to pick systems architecture patterns, and then evaluate different technologies that implement those architectural patterns.

For example, a particular architecture might call for a message bus, and given that, I could choose between various off-the-shelf open source or commercial projects that implement a message bus.

While this approach yields a nice white-board diagram, and a high-level understanding of how the system will work, some drawbacks are:


its difficult to gauge the performance of the system as a whole without fully implementing it
its difficult to determine how well each pattern / implementation will mesh with the other components
because of that, choosing between patterns tends to be gut feelings similar to "Kafka is cool, I used it on project X and it did really well"
there are no hard guarantees about the performance of the system as a whole (consistency, availability, etc)


Is there a formal approach to modeling distributed systems?  Ideally one that provides a way to abstract patterns, and provide analytic tools for making predictions about the behavior of the system?
I am not sure what you mean by "formal approach" but have you looked at Petri Nets? Many consider Petri Nets to be a "formal approach".

Personally, I use Petri's net elements (Place, Transition, Input, Output) to organize my computer program (logic annotations to net elements). I also use it to organize requirements (annotations meant for human interpretation). I find it useful to begin with a diagram (technically, graphical annotations to net elements but if each graphic represents one and only one net element then the diagram may be used to generate the net elements). Then to aid my memory I use forms to create the annotations. Based on the diagrams and the forms, I create my computer programs.  For more information about this check out "Net Elements and Annotations for Computer Programming: Computations and Interactions in PDF".

Sometimes, I create a "high-level" diagram based on a Petri Net diagram to create a view of the system. [A high-level (Petri Net) diagram is a Petri Net diagram where one or more than one graphic object represented more than one net element]. Sometimes, I begin with a high-level diagram and break it down to a Petri Net diagram. In the "high-level" case, the form views are also applicable.