checking requirements:Sequence Diagrams, Regular Expressions and State Automata

checking requirements:Sequence Diagrams, Regular Expressions and State Automata

Practical information

Requirements

 wholestory.png

Introduction

In this assignment, you will use the UML Class Diagrams, UML Sequence Diagrams, Regular Expressions, and State Automata modelling languages to design and verify a communication protocol of a client-server system. The client part of the system has a user interface from which the user can input messages and send them. The client also receives messages from a chat room which it has subscribed to. A chat room is a server. It receives messages from its clients and broadcasts these messages to subscribed clients. A chat room can have 0 or more clients. A client can be connected to 0 or more chat rooms at any time. In your design, there will be no actual interaction with the human user. Rather, the clients simulate human operations (i.e., sending connection requests and sending messages) in a random way.

You are given an implementation along with the object-interaction trace (in a file) obtained from the existing implementation. You need to model first a set of Regular Expressions, and then a set of FSAs, which you will subsequently encode, to automatically verify whether the system implementation complies with the system (protocol) specification given in the requirements below (and modelled visually in Sequence Diagram form).

The following is a textual description of a simple protocol:
Interaction behaviour to be verified (use cases):
  1. When a client sends a connection request to a chat room, the chat room immediately responds by printing to the output.
  2. On receiving a connection request, the chat room immediately makes a decision whether to accept the client or reject it.
  3. When a chat room accepts a client, the client immediately receives the acceptance and dumps to the output.
  4. When a chat room rejects a client, the client also immediately dumps the rejection.
  5. When a client sends a message, the chat room immediately receives it and prints the message to the output.
  6. When a chat room receives a message, it broadcasts it to all connected clients except the sender.
  7. The sender cannot receive its own message after it sends it.
Six tasks you need to finish step by step:
  1. Design the dynamic interaction behaviour in UML Sequence Diagrams for ONLY use cases 2 and 7 (using e.g., the drawing tool Inkscape, or scanning a drawing on a piece of paper); Use the right classes and method calls, by looking at the implementation (chatprotocol.py). It would be a good idea to start by drawing a class diagram for the implementation.
  2. Write regular expressions (refer to the format of the given output trace) for verifying the above use cases (in this assignment, you only need to verify TWO use cases: use case 2 and use case 7); the following is an example:
    Regular expression pattern for rule 1:
    ##[^\n]*\n\(CL (\d+)\) RS (\d+)\.\n##[^\n]*\n\(CR \2\) RR \1\.\n
    
    The following output will match the above pattern (multiple lines thanks to the \n):
    ## (Client 2) A connection request is sent to chat room 1.
    (CL 2) RS 1.
    ## (Chat room 1) Received connection request from client 2.
    (CR 1) RR 2.
    
    Clarification: the above uses a Regular Expression notation commonly used in UNIX Regular Expressions (as used in the stream editor sed for example) which differs from the examples given in class. In addition to the slightly different notation, the expressive power of these Regular Expressions is also higher as it allows for memory of matched expressions making the patterns context dependent. You are welcome to use different variant notations (such as the one used in the Python Regular Expression module) as long as you explain your notation.
  3. Design a FSA which encodes the regular expressions for verification;
  4. Implement this FSA for verification in the provided code framework (see scanner.py);
  5. Run this FSA implementation (which in turn implements the Regular Expressions which in turn encode the checking of interaction behaviour use cases which were modelled as Sequence Diagrams) on the given output trace to verify the specification.
  6. There is an intentional bug in the implementation (chatprotocol.py) which makes it fail to satisfy the system specification. You need to figure it out by verifying the output trace with your FSA implementation, and fix it (just one line).
  7. Write a report that explains your solution of this assigment. Include your models (scan them if they are drawings) and discuss them.
Starting Point:

Material

UML2 Sequence Diagrams

Quick intro to sequence diagrams

Tutorial on regular expressions

Feel free to find your own material

Examples

Regular Expression patterns recognition

Hans Vangheluwe. 2014.