Deriving the behavioral properties from UML designs as LTL for model checking

Design models help the system development to analyze and visualize its working scenario as a blueprint or a prototype. A successful or error free design leads to an efficient implementation. Thus ensuring the design correctness is a crucial factor in a complex system development like communication protocols. They are reactive in nature and the general verification like correctness evaluation will not yield an effective design because they change their behaviors from time-to-time. One of the way to overcome this problem is to verify their functional behaviors based on the time interval i.e., temporal ordering. To achieve this, an approach called verification property generator is proposed in this paper. The possible functional behaviors are captured in linear temporal logic for the given unified modeling language diagram based on the assumption rules. Here, the safety and liveness properties are defined independently that reduces the verification overhead. The approach is presented in general and hence the properties can be evaluated under any model checking environment.