The Scope of Modeling: where to read next

This book is an introduction. It gives you enough kinds of model to start, and one discipline — keep the map equal to the territory, so the model stays the interface the fleet reasons through — that makes them pay. It does not teach any single formalism in depth, and the zoo is not the whole field. Modeling software systems is a deep discipline with decades of literature behind it. This chapter is the doorway out: it teaches you to recognize the moment a sketch stops being enough, and points to where each of our models graduates when that moment comes.

3.7.1 When you graduate to a heavier tool

There is a moment when a working sketch stops carrying its weight, and it is worth learning to see it coming. You graduate from a sketch to a heavier analytic modeling tool when your quality goal becomes precise enough — or rises in priority enough — that you need real analytic power to meet it. The sketch is fine while the goal is a soft preference; the analytic tool earns its cost the moment the goal becomes a hard constraint you can measurably fail.

The signal is the goal itself hardening. "Fast is good" is a preference, and a napkin sketch of the call graph carries it fine. Sharpen it to "every frame must finish inside 16 milliseconds" and you have a real-time system — you now need schedulability analysis, not a vibe about which parts look slow. "Less memory is nice" is a preference too. Sharpen it to "this must fit on a board with 64 kilobytes of RAM" and you need an honest memory model, budgeted byte by byte. The concern did not change; the preference became a constraint, and the day a constraint can fail is the day the sketch has to graduate. Learn to feel that hardening, and the rest of this chapter is a map of where to go once you feel it.

3.7.2 Where our models stop

Each view here is a working sketch. When one of your goals hardens past what its sketch can say — the moment above, arriving for a particular concern — an established tool is already waiting, with a literature behind it. Here is where each view sends you when you hit that moment.

• Logical view — structure. Our types and their relations are a thin notation. For the full one — class, sequence, state, and component diagrams as a standard — graduate to UML; for systems that span software, hardware, and requirements together, to SysML.
• Process view — concurrency. We teach automata, safety versus liveness, and bounded model checking as ideas. For machine-checked proofs of them, exhaustive rather than argued, graduate to a real model checker: TLA+ or SPIN.
• Physical view — performance. We model load and cost, and we name our own gap: no request-latency model, no economics of contention. For those, an established field is already there — queuing theory for throughput under load, Petri nets for concurrency-and-resource analysis. Thermal, power, and cooling are past even those, and past this book entirely.
• Continuous and real-time systems. The zoo is discrete: states and transitions, not differential equations. A system whose behavior is continuous or hard-real-time wants timed and hybrid automata — the pointer the opening of this Part already gave, in Alur and Dill. Named again because it is the most common place a reader's real system steps outside the discrete world this book stays in.

3.7.3 A short shelf

If you read a few things past this book, read these. The first is the source of this Part's spine.

• Philippe Kruchten, "The 4+1 View Model of Architecture," IEEE Software, 1995 ¹1. Philippe Kruchten, “The 4+1 View Model of Architecture,” IEEE Software 12, no. 6 (1995): 42–50. — the five views this Part is built on.
• Grady Booch, James Rumbaugh, and Ivar Jacobson, The Unified Modeling Language User Guide ²2. Grady Booch et al., The Unified Modeling Language User Guide, 2nd ed. (Addison-Wesley, 2005). — the standard notation for structure and behavior.
• Sanford Friedenthal, Alan Moore, and Rick Steiner, A Practical Guide to SysML ³3. Sanford Friedenthal et al., A Practical Guide to Sysml: The Systems Modeling Language, 3rd ed. (Morgan Kaufmann, 2014). — MBSE's working vocabulary of blocks, constraint blocks, and traceability.
• Len Bass, Paul Clements, and Rick Kazman, Software Architecture in Practice ⁴4. Len Bass et al., Software Architecture in Practice, 3rd ed. (Addison-Wesley, 2012). — architecture in the large.
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking ⁵5. Christel Baier and Joost-Pieter Katoen, Principles of Model Checking (MIT Press, 2008). — the textbook behind the Process view's insets.
• Leslie Lamport, Specifying Systems ⁶6. Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers (Addison-Wesley, 2002). — TLA+, for specifying and checking concurrent designs.

3.7.4 Digital twins — the branch this book does not enter

One branch of modeling this book leaves untouched is the digital twin: a live model of a physical thing, kept in step with its real counterpart by a stream of sensor data, and used to predict and control it. Digital twins are the modeling practice of embedded and cyber-physical systems — aircraft engines, factory lines, power grids, anything where the model shadows a running machine. Ours shadow a codebase; a twin shadows a turbine. The spine is the same, a model kept equal to its territory and reasoned over in the thing's place, but the territory is physical and the toolkit differs. The concept is commonly credited to Michael Grieves; for the engineering discipline under it, Lee and Seshia's Introduction to Embedded Systems: A Cyber-Physical Systems Approach is the standard on-ramp.

3.7.5 The through-line

One thread ties every entry here to the book behind it. Each named tool is a way to keep a model honest against some territory — code, a schedule, a queue, a turbine. That is the formal definition of The Agent Stack doing its work one last time: whatever the territory, the thing that earns the word model is a deliberately reduced representation that supports an operation — reasoning, derivation, checking — and is held to what it represents. What changes per field is only which operation, and what keeps the map true. This book taught one instance of that move, on software, with an agent paying the upkeep that once buried the practice. The rest of the field is the same move on other territories, and the day your quality goal hardens past the sketch — the day you feel that graduation — it is worth your time.