Extending Java PathFinder with Behavior Protocols

The Component-based programming is an aproach to efficient development of software applications, where Behavior protocol is a formalism used for behavior specification of components. To further ease the development of a component application, System Correctness analysis is employed to discover errors at the designe time. However, without verifying that a component implementation complies with its behavior protocol, the analysis of the system could be based on unsatisfied property. This thesis addresses the problem of verification that a component implementation adheres to its behavior protocol. By employing Java PathFinder Model Checker it offers an ambitious solution which is successfully addressing one of the issues of the software component development