I've been thinking a lot about systems recently, and specifically about how to model them formally. A lot of ink has been dropped on how to approach them qualitatively, but so far I'm finding much less information on approaches to modeling complex engineered systems in a mathematical fashion. Some of the people I've been talking to about this are at the intersection of formal methods and mathematics; they have the greatest need for a formal language to describe their systems because they require absolute guarantees of correctness which can only be satisfied by a logical proof.

For my purposes, a formal model for systems architecture needs to provide a way to model subcomponents and a way to combine them - that is, I need some kind of contract on the component level and composition operations which enable building up in a principled way. The formal methods folks use known modeling formalisms like process calculi to do this, and they are able to then demonstrate that the composition of multiple reactive processes yields a desirable overall system property, like "for any possible input stream, I will not allow outsiders access to the system outside of the application sandbox."

While that's a very useful thing to be able to do, it's only half of the story. In a certain sense the "dual" of proving that one property holds is to enumerate all of the extant properties of an object. For example, one might want to interrogate a system model and see not only that its construction entails certain desirable properties and prevents certain undesirable ones, but also to uncover unforeseen properties that may be useful or troublesome. Unfortunately the space of possible behaviors of a system is, for our purposes, infinite; we couldn't reasonably do such an enumeration for even a small system.

But what if we could pull out the top most interesting ones? Could we do some kind of best-first, guided enumeration of them? Given some priors about the likelihood of certain configurations of subcomponents and their failure modes, we can infer the most likely ways that a malfunctioning system might be broken. Can we do something similar for a *model* of a system to predict the most likely overall behaviors? How would that guide our design choices for things like computers, aircraft, or even political systems?

I don't have the answers to these questions, and I'm not even convinced that these types of queries are possible to answer - but imagine how useful it would be if we could.