This thesis is focused on creating a formal architectural specification of a software system. I have used the computer system at the Everglades National Park (ENP) to conduct a case study. The formal method used is called Z ("zeta"). The case study used was performed on some of the software on the ENP computing system. The software is the Hydrology System and consists of a relational database called Data For Ever and several subsystems that support it. The Data For Ever system is a relational database that stores hydrology data from the Everglades. The supporting software tools are the programs and files that manipulate this hydrology data. The hydrology data were collected from the Everglades swamp. The data collected are water level, water salinity, water temperature, etc. The data were then checked and stored in the Data For Ever database. The system is up and running and in use every day (that is 365/366 days a year) of the year. I added some software tools to it. There was little or no change to the existing database, however the database was redefined in Z specifications. This process is called Reverse Engineering. New modules to test and manipulate the data were defined. At present the data are not being tested or verified automatically as they are being collected from the field. The new modules test and/or verify the incoming data to examine the quality of them. The data are tested to see if they are within preset limits. If they are not, a possible error is recorded. These errors are presented during the daily report that is already in use.
