Ansprechpartner:
Prabhu Shankar Kaliappan (prabhuShankar.Kaliappan(at)b-tu.de)

Design verification is an important stage in a protocol development life cycle to ensure that the developed design models are error-free. On a successful veri­fication, the models can be used for code generation, and test case derivation. The verifica­tion process is not carried out directly over the design models be­cause none of the speci­fication or description languages will permit it. For this, the design models have to be transformed into an intermediate format and later appropriate verification mechanism need to be applied. Besides, design models only makes sense if it is proved for the correctness properties like deadlock freedom, livelock freedom, completeness, termination, etc. commonly known as safety and liveness properties. The safety and liveness properties can also used to check whether the designed model fulfills the requirement specification or not. Generally, the design engineer formulates these properties manually from the designs through a concrete assumption. Further, the properties are supplemented to the verification mechanism along with the verification model. Formulizing the properties manually is a straightforward method by discov­ering the protocol behaviors in a design model. This is applicable if the designer is familiar with the property notations, but is difficult for the designers with less knowledge. One of the open problems during the manual property formuli­zation is the interpretation. It is difficult to understand the property sense to an anonymous designer, i.e. on what basis the properties are formulized. Only the core protocol designer can sense the meaning. This also makes a reusability problem while verification. For this, a pre-defined automated prop­erty formulization may be introduced by defining a set of assumption properties with the inference rules. Based on the inference rules, the protocol design behaviors can be defined in a formal way as verification properties. This can be a design aid for the protocol developers with less knowledge.

In principle, UML Sequence and activity diagrams are used to model the protocol functions like the successful connection set up, data transfer, error control, flow control, and others. Intuitively, the activity model could define whether a sequence model is correct or not; and a sequence model may be used to verify that an activity model really does show the activities necessary or not. Hence, an objective is to consider the frequently applied protocol functions in UML sequence diagram and a template should be developed to generate the safety and liveness properties.

An algorithmic method is available. Student must develop the tool in JAVA. This is probably a logic based approach.