Network::Protocol Notation

Introduction

This Protocol Notation is designed to notate protocols based on TCP. It therefore supports the following actions of the TCP protocol.

TCP action	statement
bind	???
connect	???
recv	???
send	???
sendall	???

Processes And Channels

A protocol is defined by a number, mostly 2, processes that use channels between them to communicate. There is only one channel between two processes and one channel connects two processes. A process corresponds to a communication partner, while a channel corresponds to the connection.

A process can send messages into a channel. The channel holds them in the order they are send and passes them on to the process receiving in the same order. When describing a channel's contents using a sequence (m1; m2; m3; ...), the first message of that sequence corresponds to the first message send in which will be received by the receiving process next. A channel is able to hold an unlimited number of messages.

The Attributes of a process

A process has different constants (const) that he can't change, while they might be changeable by other processes. A process also has variables (var) and actions. The variables can be changed by the actions of the process.

Both constants and variables can be one of following types: boolean, integer, text, range and array. Text is a special type of integer. Constants are defined using the keyword const in the definition block of a process and variables using var:

var is_true : boolean
    txt     : text

type	Notation
boolean	true or false
integer	1, 2 or any other decimal number hexadecimal numbers:0x1F2 or 1F2h binary numbers: 110010b
text	"some text in quotes"
range	10-34 that is <n1>-<n2> [ 10 - 34 ] that is [ <n1> - <n2> ]
array	( e1 ; e2 ; e3 ) or ( e1 , e2 , e3 )

Actions

Actions consist of a guard determining whether the action is executed, an arrow --> and the statement to be executed:

    <guard> --> <statement>

The guard can be a local guard being a boolean expression using the constants and variables of the process. The statement will in that case only be executed if the expression is true. A receiving guard will try to receive a message and execute the statement afterwards. Here <to> is the variable that should be read into and <process name> the name of a existing process. The message will be received from the channel connecting the current process with the process :

    rev <to> from <process name> --> <statement>

The skip statement is executed by doing nothing.

skip

An assignment statement assigns a value E to a variable v. Both have to be the same type.

v := E

The send statement sends a message to a process.

send <message> to <process name>

A selection or if statement selects a <boolean expression> whose value is true and executes it.

if <boolean expression> --> <statement>
[] <boolean expression> --> <statement>
...
fi

The iteration statement executes a statement while a <boolean expression> is true. If the condition isn't met (anymore) the iteration statement exits.

do <boolean expression> --> <statement>
od

A sequence statement executes two statements after each other.

<statement> ; <statement>

Defining A Simple Process

# Basic Mesage Chattool Protocol
# Version 1.0

process client
const   version : version number
        name : str
        role : str[user]

var     connected : boolean

connect server : server

Messages [send]
 def info
        INFO <version>

 def register
        REGISTER <name> AS <role>

        <name> : any str
        <role> : str("user")

def message
        MSG <type> <from> <to> WITH <length>\n

        <content> \EOF

        <type>    : str("text/unicode|text/ascii")
        <from>    : str
        <to>      : str
        <length>  : int {number of bit in content}
        <content> : bit


Messages [receive]
def info 
        INFO <version> <ok>

        <ok> : boolean

def ok
        OK

def error
        ERROR <type> <message>

        <type> : {kind of error}
        <message> : str (optional)

def message
        MSG <type> <from> <to> WITH <length>\n 

        <content> \EOF

        <type>    : str("text/unicode|text/ascii")
        <from>    : str
        <to>      : str
        <length>  : int {number of bit in content}
        <content> : bit

def connect
        UPDATE USER <user> <connect>

        <user> : str
        <add>  : boolean {wether the user connected or disconnected}

state #Connect:start

        send info[version] to server

        receive info[-v, -ok]
        not -ok --> close

        {Check Info, prepare stuff}

        send register[name; role] to server

        receive ok()/error(-type;) from server

        {process error}
        {error is returned when user name is already registered}
        {change name and try again}

        enter #Wait


state #Wait

        do connected:
                receive message->-msg from server --> enter #RecvMSG -msg

                receive error from server --> {process error}

                receive connect from server --> {process new user/disconnect}
        od


state #RecvMSG

        msg[type; from; to; length]

        receive bytes(length)->-content from server

        {process msg}


state #Send:command

        content = any
        length = length(content)

        send message[any, any, any, length, content] to server


state #END:close

        exit

state :end

        {pass}


process server
const   port : int
        version : version number

        names : list of str

var     connected : boolean
        user : str

bind port

listen for client

Messages [recv]
 def info
        INFO <version>

 def register
        REGISTER <name> AS <role>

        <name> : any str
        <role> : str("user")

def message
        MSG <type> <from> <to> WITH <length>\n

        <content> \EOF

        <type>    : str("text/unicode|text/ascii")
        <from>    : str
        <to>      : str
        <length>  : int {number of bit in content}
        <content> : bit


Messages [send]
def info 
        INFO <version> <ok>

        <ok> : boolean

def message
        MSG <type> <from> <to> WITH <length>\n 

        <content> \EOF

        <type>    : str("text/unicode|text/ascii")
        <from>    : str
        <to>      : str
        <length>  : int {number of bit in content}
        <content> : bit

def connect
        UPDATE USER <user> <connect>

        <user> : str
        <add>  : boolean {wether the user connected or disconnected


state #Connect:start

        receive info[-v] from client

        {process version; make -ok}

        receive info[version, -ok] from client
        not -ok --> close

        {prepare stuff}

        receive register[-name; -role] from client

        {process -name and -role}

        user = -name

        if -role = {user role} --> send connect[user, 1] to {all clients}

        enter #Wait


state #Wait

        do connected:
                receive message->-msg from server --> enter #RecvMSG -msg
        od


state #RecvMSG

        msg[type; from; to; length]

        receive bytes(length)->-content from server

        {process msg}

        {do #Send with msg for each connected client}


state #Send:command

        content = any
        length = length(content)

        send message[any, any, any, length, content] to client


state #END:close

        if -role = {user role} --> send connect[user; 0] to {all clients}
        exit

state :end

        {pass}