Object of certification: The AIA-ITP Load Balancer Implementation
Kind of certificate: Process Behavior Certificate
Level: Model Verified
Date: January, 11, 2008.
What this certificate certifies and how it is certified is stated below. Of course, this certificate does not say anything about those parts of the object of certification that is abstracted from nor does it say anything about those parts of the object of certification that are not considered at all. This certificate is valid for one year under the assumption that no changes to the software are made during that period.
The certification work was performed by
Full Postal
Address: Postbus 513, 5600MB
Affiliation: Laboratory for Quality
Software,
E-mail Address: y.s.usenko@laquso.com
Phone Number: +31 40 2473519
Fax Number : +31 40 247 4252
Full Postal
Address: Postbus 9010, 6500 GL Nijmegen, The
Affiliation: Laboratory for Quality
Software,
E-mail Address: marko@laquso.com
Phone Number: +31 24 3653410
Fax Number : +31 24 3652298
The project has been performed in the following phases:
- In a discussion with two employees of Aia Software (Stefan ten Hoedt en René Schreurs) we obtained the overall idea of the structure and the behavior of the software in general and the parts to be modeled in particular.
- The relevant parts were modeled in mCRL2 [3]. We started out from the C code of the relevant parts. The session layer of the LoadBalancer protocol was modeled quite close to the C code. Both the higher-level application layer and the underlying TCP-socket layer were modeled in an abstract manner.
- The code and the model were reviewed by the LaQuSo-modeler and the Aia-developer in order to achieve the maximal matching. This has lead to a number of changes in the model, as well as to a number of questions about the code and a number of concrete desired properties that could be analyzed.
- The model was analyzed with the help of the model-checking techniques of mCRL2 Toolset w.r.t deadlock-freedom and a number of other starvation and consistency properties that were formulated together with the client. This revealed 5 problems in the C code. These problems were accepted by Aia Software and corrected in the application.
-
The
corrections were also brought into the model. The resulting model was fully
verified with respect to the desired properties for all possible configurations
of at most 4 processes.
-
Errors
had been found only using 3 or less processes. Testing with 4 processes gave to
new errors.
-
The
investigation is published in a technical report (including the full model) [5]
and in an academic publication [4].
The following properties were tested:
-
The
software should be free from deadlocks.
-
Certain log messages are considered to be of
critical importance. These
should never occur as they indicate that there is
something fundamentally wrong with the system.
-
The partnership
links should be consistent, e.g., if the partner of A is B>0 (0 means no
partner), then the partner of B is either A or 0.
-
Waiting for a
partner should only be done if the partner link is not 0$ This
boils down to the fact that a document processor may not be in a sleeping state
if it has no partner (except when a request is pending to it).
-
The number of
times a thread acquires a lock should be limited. In case a lock is acquired a
multiple number of times it has to be released the same number of times. If a
thread acquires a lock in a loop, a certain bound induced by the oprating system can be reached, resulting in an undesired
behavior. Moreover, a high number of nested lock acquisitions may indicate a
logical error in the program.
-
The number of requests that are pending in the
system should be limited.
-
Connection 0 is
changed, 0 is used as a "no partner" in the partnership relation:A process can still
change its partner even if its partner
link is set to 0.
-
Conection is being changed while in STATE_FREE: a free
connection structure should not be changed by another thread
- All
checks for the LaQuSo certificate Source code, Implementation,
Behavorial, Model Verified as introduced in the full LaQuSo Software Product Certification Model [6]. The
certificate used is given below.
All these properties were found to be holding. The
run-time figures are below.
servers-clients
1-1: 237 levels, 368076 states and 796531 transitions. 3m 19s
2-1: 365 levels, 9859665 states and 21474287 transitions. 1h 27m 46s
1-2: 442 levels, 28190636 states and 61106671 transitions. 4h 02m 43s
3-1: 480 levels, 209081725 states and 455637436 transitions. 24h 28m 10s
2-2: 550 levels, 1475879382 states and 3189207161 transitions. 8d 3h 7m. >106Gb RAM
1-3: 637 levels, 1799937602 states and 3889435637 transitions. 7d 7h 46m >136Gb RAM
In total it ran about 16 days and 17 hours using way over a 100 gigabytes.
mCRL2 could be used in this industrial setting of a server for document production. A part of the operating system services (sockets, lock, events, etc.) could also be modeled. Aia has got a working reference model of a crucial part of the LoadBalancer software. In principle the company is now able to incorporate code changes into the model and check whether the properties still hold for the updated version.
Links
[1] Aia Software BV, http://www.aia-itp.com
[2] Laboratory
for Quality Software (LaQuSo), http://www.laquso.com/.
[3] mCRL2 Toolset, http://www.mcrl2.org
[4] Marko
van Eekelen, Stefan ten Hoedt, René Schreurs, Yaroslav S. Usenko. Analysis of a Session-Layer Protocol in mCRL2. Verification of a Real-Life
Industrial Implementation. 12th
International Workshop on Formal Methods for Industrial Critical Systems
(FMICS 2007). 1-2 July.
[5] Marko
van Eekelen, Stefan ten Hoedt, René Schreurs, and Yaroslav Usenko. Modeling
and verifying a Real-Life Industrial Session-Layer Protocol in mCRL2. Technical report: ICIS-R07014,
June, Radboud University Nijmegen, 2007.
[6]
Petra
Heck, Marko van Eekelen, The
LaQuSo Software Product Certification Model. To appear
as Technical University
Process behavior certificates aim to check general or specific progress and safety properties on the software product. We can examine the detailed design or the implementation (source code or running system), which leads to three different certificates. A formal process model is needed to check the desired behavioral properties. The levels and checks (SC1, SC2 and SC3) are explained in [1].
|
Product Area |
Implementation |
|
Properties |
Behavioral |
|
Level |
Model verified |
|
Description |
Check the behavioral properties on the formal models; Check conformance between the source code and the formal models; |
|
Input |
Formal and informal models of the component behavior, source code, safety and progress properties |
The following checks need to be answered with ‘Yes’ or ‘Not applicable’. It is explicitly specified in the table below when an item may be marked as ‘N/A’. Items with ‘-’ in the third column must always be answered with ‘Yes’ to obtain a certificate.
|
Check |
Description |
N/A if: |
|
|
Detailed Design certificate granted |
Source Code based |
|
Required Elements |
||
|
SC1.1 a |
Software system |
- |
|
SC1.2 a |
Technical specification |
- |
|
SC1.3 a |
Process models of the system |
- |
|
Manual checks |
||
|
SC3.1 a till l |
Consistency of elements |
Element not delivered |
|
SC3.1 m |
Relevant and feasible properties |
- |
|
SC3.1 n |
Formal and informal model conform |
- |
|
Formal checks |
||
|
SC 3.3 a, c, d, f |
Consistency of elements |
Element not delivered |
|
SC3.3 b |
Process models are correct |
- |
|
SC 3.3 e |
Code correctly generated |
No generated code |
|
SC3.3 g |
Models match behavioral properties |
- |
A certificate will be handed out if all checks in the above table are answered with ‘N/A’ (if allowed according to the table) or ‘Yes’.
|
Product Area |
Tests (Model Based Testing) |
|
Properties |
Consistency |
|
Level |
Model verified |
|
Description |
Check conformance between the running system and the formal models; check the behavioral properties on the formal models |
|
Input |
Formal models of the component behavior, executable system, safety and progress properties |
The following checks need to be answered with ‘Yes’ or ‘Not applicable’. It is explicitly specified in the table below when an item may be marked as ‘N/A’. Items with ‘-’ in the third column must always be answered with ‘Yes’ to obtain a certificate.
|
Check |
Description |
N/A if: |
|
|
Detailed Design certificate granted |
- |
|
Required Elements |
||
|
SC1.3 a |
System process models |
- |
|
SC1.3 b |
Wrapper to system under test |
- |
|
Manual checks |
||
|
SC3.1 n |
Relevant and feasible properties |
- |
|
SC3.1 o |
Formal model and system conform |
- |
|
Formal checks |
||
|
SC3.3 a |
Process models are correct workflow |
- |
|
SC 3.3 b |
Process models are mutually consistent |
- |
|
SC 3.3 c |
Model-based testing |
- |
|
SC3.3 d |
Models match behavioral properties |
- |
A certificate will be handed out if all checks in the above table are answered with ‘N/A’ (if allowed according to the table) or ‘Yes’.