Next: 6 Related work
Up: Specifying component-based software architectures
Previous: 4 Larch/Java for design
As in [AAG95,GMW96] we recognize components and connectors as basic elements of an architectural description. In the following we show how Larch can be used for the design of a software architecture, with Java as target language for the design of the interface of the modules. The LSL can be used for the formal description of the basic properties of components and connectors. Traits for a general component and a general connector respectively are given below:
component:trait
includes Set(iport, Set[iport]), Set(oport, Set[oport])
component tuple of inports: Set[iport], outports: Set[oport]
connector:trait
includes Set(irole, Set[irole]),Set(orole, Set[orole])
component tuple of inroles: Set[irole], outroles: Set[orole]
Basically, components and connectors are active elements, each owning a set of ports and roles, respectively. A port is an interface between each component and its environment; a role is an interaction point among participating components. Let us concentrate on a particular type of architecture, namely a simple client server system. We start defining the trait for the basic components of the system, client and server, and the trait for the connector describing the interactions among components, in our case a remote procedure call. These traits are obtained reusing the general traits given above and the traits defined in the LSL library [GH93]. Client and server traits are similar but have distinct behaviors.
Client:trait
includes component,
Queue(data, inputstream)
Queue(data, outputstream);
Client tuple of comp:component, inputs: inputstream,
outputs:outputstream
introduces
Initclient: -> Client
Isconnected: Client -> Bool
IsValid: Client -> Bool
asserts
\forall c: Client
IsValid(c) == size(c.comp.inports) =1 /\
size(c.comp.outports) = 1;
Server:trait
includes component,
Queue(data, inputstream)
Queue(data, outputstream);
Server tuple of comp:component, inputs: inputstream,
outputs:outputstream
introduces
Initserver: -> Server
Isconnected: Server -> Bool
Rpc: trait
includes connector,
Queue(data, inputstream)
Queue(data, outputstream);
Rpc tuple of conn:connector, inputs: inputstream,
outputs:outputstream
introduces
Initrpc: -> Rpc
Initinputstream: -> inputstream
Initoutputstream: -> outputstream
IsValid: Rpc -> Bool
asserts
\forall r: Rpc
IsValid(r) == size(r.conn.inroles) =1 /\
size(r.conn.outroles) = 1;
The LIL specification modules describe the functional behavior of each component. A client is responsible for starting the communication and the retrieval of result data. The server, instead, is listening for incoming requests; it services a client as soon as possible. The rpc connector sets up the connection for the exchange of data between the client and the server.
We use the Java socket interface as protocol of communication between hosts on the network [OH97]. The LIL modules for the Server component and the Rpc connector are given in the following:
public class rpc_sock(host,port){
uses rpc;
public void setup_socket(host,port){
ensures self'=initrpc self'.inputs = initinputstream
self'.outputs = initoutputstream;}
public void send_data(data){
modifies self;
ensures self'=set_outputs(self , append(data, self .outputs));}
public Byte get_data(data){
modifies self;
ensures result=head(self .inputs) self'=set_inputs(self , tail(self .inputs));}
public void disconnect(){
modifies self;
ensures self'.inputs = empty self'.outputs = empty;}
}
public class Server{
uses server;
public void setup_server(port){
requires Isconnected(self) port self.comp.inports;
ensures self' =Initserver;}
public data get(port){
requires Isconnected(self);
when self .inputs = empty;
modifies self;
ensures result=head(self .inputs) self'=set_inputs(self , tail(self .inputs));}
public data write(data,port){
requires Isconnected(self);
modifies self;
ensures self'=set_outputs(self , append(data, self .outputs));}
The meaning of the interface specification modules is a collection of Java code files which satisfy their specification [Lea97b]. The following is one Java code module implementing an rpc-socket:
public class rpc_sock(host,port){
public void setup_socket(host,port){
Socket rpc = new Socket(host,port);
Inputstream in = rpc.getInputStream();
OutputStream out = rpc.getOutputStream();}
public void send_data(data){
out.write(data);}
public Byte get_data(data){
in.read();}
public void disconnect(){
rpc.close;}
At this point another level of specification is needed to describe the effective interactions among the computational elements.
A configuration module lists the instance of design elements which form our system, the LIL modules which are used for the specification and the attachments between ports of the components and roles of the connectors. Additionally, functional properties may be added to describe and constrain the system behavior. In our case we have an instance for each component and connector we previously have defined, and state input-output connections between rpc connector and the two components.
c/s-system:configuration
component:
c1:client,s1:server;
connector:
r1:rpc
attached:
r1.conn.irole = c1.comp.oport;
r1.conn.orole = s1.comp.iport;
The implementation of a configuration module may be thought of as a main application module which use the other components of the system and define their behavior when computation progresses
P. Ciancarini and S. Cimato