Download Component Reliability Extensions for Fractal component model

User's manual
6.4.4. Case Study: Applying runtime-checker on the Airport
internet lounge demo
To demonstrate the runtime-checking on a non-trivial case study, we have used the implementation
of the airport internet lounge demo described in the Demo description
[http://kraken.cs.cas.cz/ft/doc/demo/Demo-Description.pdf]; technical details of the implementation
are
described
in
the
separate
document
Demo
implementation
notes
[http://kraken.cs.cas.cz/ft/doc/demo/ftdemo.html]. We assigned runtime protocols to all demo components. There are minor differences between protocols for static and runtime checking.
In the runtime protocols, we had to remove the numbered suffixes from method names (e.g., TokenInvalidated_1 or TokenInvalidated_2) for methods where they were required for static checking. The
suffixes are used to distinguish processing of several parallel calls of the same method. As they all
represent a single method in the implementation, the Julia interceptor will know only the method name
without a suffix when passing it to the runtime checker. As the core of the runtime checker is the same
as the core of the static checker, which does not interpret the method suffixes (i.e., TokenInvalidated_1
and TokenInvalidated_2 are simply two different methods for the static checker core), the runtime
checker would not be able to match a method name from the interceptor (without suffix) to a method
name from a static behavior protocol (with suffix). This is the reason why we had to remove the suffixes
and to create the separate runtime protocols.
Another feature used in static procotols are atomic actions. In the protocols for demo components,
they are used to specify the synchronization behavior for some methods and to distinguish the initialization stage and "running" stage of components, as these two behaviors are much more easy to describe
and comprehend with atomic actions. As an atomic action requires that all the methods it contains are
processed at the same time (note that this is stronger than just a "simple" parallel operator). However,
the runtime checker is not multithreaded, and all method callbacks from the Julia interceptors are
processed in a sequential order. This means that is makes no sense to use the atomic actions in runtime
protocols. Our solution was to replace all atomic actions with other "standard" behavior protocol
constructs.
The Fractal implementation demo is in fact a set of "independent" components that are only connected
to communicate with each other. However, as the components are designed to serve to the users of the
system, none of them is able to work autonomously. In order to function, the components must receive
requests from the "outer" world (their environment). The three components responsible for such
communication are the DhcpServer component (more precisely, one of its subcomponents, the DhcpListener), the Arbitrator and the AccountDatabase. To simulate the environment of these components,
we created the Simulator component. It implements a simple hard-wired test of all the "client" accessible
methods of the demo components - i.e., it emulates requests accepted from 3 virtual clients passed to
the Arbitrator component (via a virtual web server) and also calls several methods on the DhcpListener
component simulating the DHCP protocol packets coming from clients. Here is the main part of the
Simulator run method:
iArbitratorLifetimeController.Start();
byte[] mac1=new byte[] { 0, 0, 0, 0, 0, 0 };
byte[] mac2=new byte[] { 0, 0, 0, 0, 0, 1 };
byte[] mac3=new byte[] { 0, 0, 0, 0, 0, 2 };
InetAddress addr1=dhcpListener.RequestNewIpAddress(mac1);
iLogin.LoginWithAccountId(addr1,"","");
InetAddress addr2=dhcpListener.RequestNewIpAddress(mac2);
InetAddress addr3=dhcpListener.RequestNewIpAddress(mac3);
65