A software tool that generates symbolic model verifier (SMV) input language from a predicate transition net

The purpose of this research was to apply model checking by using a symbolic model checker on Predicate Transition Nets (PrT Nets). A PrT Net is a formal model of information flow which allows system properties to be modeled and analyzed. The aim of this thesis was to use the modeling and analysis power of PrT nets to provide a mechanism for the system model to be verified. Symbolic Model Verifier (SMV) was the model checker chosen in this thesis, and in order to verify the PrT net model of a system, it was translated to SMV input language. A software tool was implemented which translates the PrT Net into SMV language, hence enabling the process of model checking. The system includes two parts: the PrT net editor where the representation of a system can be edited, and the translator which converts the PrT net into an SMV program.

Evidence of climate variability and tropical cyclone activity from diatom assemblage dynamics in coastal southwest Florida

Estuaries are dynamic on many spatial and temporal scales. Distinguishing effects of unpredictable events from cyclical patterns can be challenging but important to predict the influence of press and pulse drivers in the face of climate change. Diatom assemblages respond rapidly to changing environmental conditions and characterize change on multiple time scales. The goals of this research were to 1) characterize diatom assemblages in the Charlotte Harbor watershed, their relationships with water quality parameters, and how they change in response to climate; and 2) use assemblages in sediment cores to interpret past climate changes and tropical cyclone activity. ^ Diatom assemblages had strong relationships with salinity and nutrient concentrations, and a quantitative tool was developed to reconstruct past values of these parameters. Assemblages were stable between the wet and dry seasons, and were more similar to each other than to assemblages found following a tropical cyclone. Diatom assemblages following the storm showed a decrease in dispersion among sites, a pattern that was consistent on different spatial scales but may depend on hydrological management regimes. ^ Analysis of sediment cores from two southwest Florida estuaries showed that locally-developed diatom inference models can be applied with caution on regional scales. Large-scale climate changes were suggested by environmental reconstructions in both estuaries, but with slightly different temporal pacing. Estimates of salinity and nutrient concentrations suggested that major hydrological patterns changed at approximately 5.5 and 3 kyrs BP. A highly temporally-resolved sediment core from Charlotte Harbor provided evidence for past changes that correspond with known climate records. Diatom assemblages had significant relationships with the three-year average index values of the Atlantic Multidecadal Oscillation and the El Niño Southern Oscillation. Assemblages that predicted low salinity and high total phosphorus also had the lowest dispersion and corresponded with some major storms in the known record, which together may provide a proxy for evidence of severe storms in the paleoecological record. ^