{'fraction_non_alphanumeric': 0.023480662983425413, 'fraction_numerical': 0.0027624309392265192, 'mean_word_length': 5.245689655172414, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Verification of Protocol Design using UML - SMV

Designing a new protocol, which is reliable and meets all the specifications, is a challenging task. There are many instances of protocol failing (when actually deployed) even after thorough testing. To enhance the correctness of a protocol design, formal verification techniques are used. The formal verification is a complementary approach to testing for detecting subtle design errors. In formal verification, the behavior of the protocol is described using a program like notation, collection of finite state machines or temporal logic formulae and then this description is compared with the specification of the desired behavior. If the verifier detects any flaw in the behavioral description, then it generates a counter example or an error trace that illustrates how the problem has occurred [1]. In this paper, we present a pragmatic semiformal approach for verifying the protocol design. We have considered UML statechart diagrams [2] for describing the behavior of the protocol. The desired behavioral property (safety property) is specified using temporal logic formula [3]. The problem associated with the model verification is “State Explosion” [4]. The state space search technique presented in this paper restricts the exploration of number of states, thereby saves the time and the memory required. We have demonstrated the correctness of our approach by verifying the UML statechart