Modeling, Validation and Verification of Concurrent Behavior in Canal System Using LTSA and UPPAAL

Abstract

A complex system is composed of subsystems. Common sense dictates complex systems in the physical world are reactive and concurrent in nature. The procedure to model a concurrent system and the procedure to validate its performance are complex because of the presence of the interactions between and among the subsystems, calling for an integrated approach from the viewpoint of systems engineering. In this thesis, a canal system is the object of study. The main objectives are to achieve a deadlock free and safe architectural model of a canal system, as measured by transportation criteria. Specifically, the Panama Canal is used as a case study where a procedure has been developed to model this waterway. This thesis models the scenario-based specifications, system behavioral model, animated verification and validation of the Panama Canal with LTSA and with the help of UPPAAL brings time constraints into the canal behavioral model.