Summary

This chapter has consolidated the model-based approach used in previous chapters. It has described the process of progressing from system requirements through modeling to programming. The main activities were identified, including system decomposition into a model structure and model elaboration, analysis and revision, if necessary. The stage at which properties are checked was also discussed. Safety properties can be checked on system or subsystem models as appropriate. Progress checks need to be performed on the overall system model. The mapping of a model structure into an implementation was also described. No particular design method is imposed. We advocate modeling in association with every design method. Modeling complements program design and is particularly useful when constructing concurrent programs.

A cruise control system for a car was used to illustrate the model-based design approach. This system was briefly introduced in Chapter 1 to motivate model-based design; it was dealt with in detail in this chapter, giving both the model details and an implementation in Java.