Comanche with a Sequential 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.

• 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: 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".

  In more details the Comanche Web Server contains seven sub-components - request receiver, logger, scheduler, request analyser, request dispatcher, file request handler, error request handler. Behaviour of Comanche Web Server is the following: after the request receiver is called with an input stream, it calls the scheduler (sequential in this case) with a single Runnable parameter which execute the given Runnable. Afterwards request analyser 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 the 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.

• A user component: it is a Client of the server. A Client can send request or it is able to receive a output file or receive an message that the file is not found.

• 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 20 states and models of users have 7 states.

• CI model of the system with 7 users: ComancheS7.cdve.

Models

Component-Interaction automata model / Labelled Kripke structure model:

Size

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

Extended information

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

Cutoffs

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
R          * - * - * 1 *

describes that if the control component is in the state R then it is possible that an arbitrary number of users are in the local states 1, 3, 5, 7 (symbol "*"), no user is in the states 2, 4 (symbol "-"), and exactly one user is in the state 6 (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
A          * - * - * - *                          (A,2),  (A,4),  (A,6)
B          * 1 * - * - *                          (B,2,2),(B,4),  (B,6)
C          * - * - * - *                          (C,2),  (C,4),  (C,6)
D          * - * - * - *                          (D,2),  (D,4),  (D,6)
E          * - * - * - *                          (E,2),  (E,4),  (E,6)
F          * - * - * - *                          (F,2),  (F,4),  (F,6)
G          * - * - * - *                          (G,2),  (G,4),  (G,6)
H          * - * - * - *                          (H,2),  (H,4),  (H,6)
I          * - * - * - *                          (I,2),  (I,4),  (I,6)
J          * - * - * - *                          (J,2),  (J,4),  (J,6)
K          * - * - * - *                          (K,2),  (K,4),  (K,6)
L          * - * - * - *                          (L,2),  (L,4),  (L,6)
M          * - * 1 * - *                          (M,2),  (M,4,4),(M,6)
N          * - * - * - *                          (N,2),  (N,4),  (N,6)
O          * - * - * - *                          (O,2),  (O,4),  (O,6)
P          * - * - * - *                          (P,2),  (P,4),  (P,6)
Q          * - * - * - *                          (Q,2),  (Q,4),  (Q,6)
R          * - * - * 1 *                          (R,2),  (R,4),  (R,6,6)
S          * - * - * - *                          (S,2),  (S,4),  (S,6)
T          * - * - * - *                          (T,2),  (T,4),  (T,6) 
 

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

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