Comanche with a Multi Thread Scheduler

The C-U system - Comanche is a system composed of a the Comanche Web Server (an extremely minimal HTTP server) and its Clients. The presented model of Comanche Web Server is based on the application in Java (component oriented) and the component architecture published in [1]. The model of Client is created as an model of an basic client, which uses the server. Comanche Web Server is able to receive a request. If the request is of the shape "GET file_name" then it tries to find the file "file_name". If the file is found than it prints the file, else it prints warnings "HTTP/1.0 404 Not Found", "Document not found".

C-U model: The Comanche Web Server is a composition of the primitive components Request receiver, Scheduler, Request analyzer, Request dispatcher, Logger, File request handler, Error request handler. Because this Comanche Web Server is multithreaded, the Comanche Web Server composed with n clients contains:
- 1 component: Request receiver, Scheduler,

- n components: Request analyzer, Request dispatcher, Logger, File request handler, Error request handler, Client .
Thus the control component of the system models only a parts Request receiver, Scheduler. And a user is the composition of components Request analyzer, Request dispatcher, Logger, File request handler, Error request handler, Client . It is illustrated in the next figure (primitive components of Comanche Web Server are green, primitive components modelling clients are red).

Modelling: Some modelled methods, e.g. schedule(), is assigned a tuple of action names: sch denotes the call of the method, and sch' the return from the method. These two determine the start and the end of the method's execution. Some parts of the Java application (particularly some uninteresting internal activity) is modelled using one action only.

The control component: The control component models Request receiver and Scheduler. It is able to receive a request and then ti is able to make the action "sch" (shortcut for scheduler).

A user component: it is a Client of the server together with a part of the Comanche Web Server model (components Request analyzer, Request dispatcher, Logger, File request handler, Error request handler) which the Client is able to use. At first the Client can send a request (write some input stream and send it to the request receiver) and after that it calls the scheduler (performs action "sch") and then it is able to start using the part of the Comanche Web Server (it models creating a new thread). After that the request analyser (composed in the user) reads the input stream, using logger the stream is logged and if the input stream starts with GET the request analyser calls request dispatcher. Request dispatcher first using file request handler tries to find a file which name is in the input stream (after "GET ") and prints it. Providing it is not successful it using error request handler prints the error message.

Shortcuts: In the models, name of the method schedule() is shortened to sch, handleRequest() of the class RequestAnalyzer to ra, handleRequest() of the class RequestDispatcher to rd, handleRequest() of the class FileRequestHandler to Frh, handleRequest() of the class ErrorRequestHandler to Erh, and the functions r.out.write(data) and out.print("HTTP/1.0 200 OK") of the class FileRequestHandler to out.

Numbers of states: The control component model has 4 states and models of users have 20 states.

CI model of the system with 5 users: ComancheMT5.cdve.

Models

Component-Interaction automata model / Labelled Kripke structure model:

CI control component model CI user model

Size

size of the system with the control component and n users without symmetry reduction.

n	1	2	3	4	5
size of the system with n users	20	391	7 514	142 476	2 672 672

Extended information

- information involving verification of the reachability properties on the model.

Cutoffs

l	0	1	2	3	4	5
Cutoff	1	2	3	4	5	6

Reachable states, Unreachable l+1-tuples

- The following table describes all reachable states in the system with any number of clients. For example

           1  2  3  4  5  6  7  8  9  10 11 12 13 14 15 16 17 18 19 20
B          *  1  -  -  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *

describes that if the control component is in the state B then it is possible that an arbitrary number of users are in the local states 1, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20 (symbol "*"), no user is in the states 3, 4 (symbol "-"), and exactly one user is in the state 2 (symbol "1").

- The (l+1)-tuples after each line denotes all unreachable (l+1)-tuples which do not contain an unreachable i+1-tuple for some i < l. An interesting fact is that such tuples are only 1+1-tuples and 2+1-tuples

                                Reachable states                                       Unreachable l+1-tuples 
           1  2  3  4  5  6  7  8  9  10 11 12 13 14 15 16 17 18 19 20
A          *  -  -  -  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *              (A,2),   (A,3),   (A,4)
B          *  1  -  -  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *              (B,2,2), (B,3),   (B,4)
C          *  -  1  -  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *              (C,2),   (C,3,3), (C,4)
D          *  -  -  1  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *  *              (D,2),   (D,3),   (D,4,4)

"*" - an arbitrary number of users, 
"-" - no user,
"1" - exactly one user.

[1] http://fractal.objectweb.org/tutorial/index.html.