The current picture of the specification and validation environment under construction is given in Figure 1. In this environment, several analysis and model-checking tools are interfaced with the common model description language. These tools use various decision procedures and symbolic representation packages. The names of the packages and tools we have developed which are elements of this environment are shown on the picture. We give hereafter a description of each of these components.