A number of readers of the book have asked how to show that the Java Program that implements a design model can be shown to be a correct implementation of that model. This supplement addresses this question by showing how FSP models can be derived directly from the source of the Java program. The examples used expose some limitations and bugs in two of the programs published in the book. These are the Bounded Buffer example and the Readers-Writer lock with writer priority.