Previous: Mapping Patterns, Up: Petri Net Mapping Rules


8.2 Examples

Like code generation, the Petri net mapping does not directly handle behavioral description: such descriptions must be provided using AADL properties and then merged with the generated net.

Here is an example of an AADL model:

     
     thread micro_broker end micro_broker;
     
     thread implementation micro_broker.receiver
     subcomponents
       buffer : data data_buffer;
     calls
       listen : {get_data : subprogram protocol.simple;};
       compute : {execute : subprogram execution.simple;};
     connections
       data access buffer -> get_data.buffer;
       data access buffer -> execute.buffer;
     properties
       Dispatch_Protocol => background;
       Ocarina::formal_implementation => "broker.pn";
     end micro_broker.receiver;
     
     data data_buffer end data_buffer;
     
     subprogram protocol
     features
       buffer : requires data access data_buffer;
     end protocol;
     
     subprogram implementation protocol.simple
     calls
       {get_data : subprogram transport;};
     connections
       data access buffer -> get_data.buffer;
     end protocol.simple;
     
     subprogram transport
     features
       buffer : requires data access data_buffer;
     end transport;
     
     subprogram execution
     features
       req : in parameter message;
     end execution;
     
     subprogram implementation execution.simple
     calls
       {get_message : subprogram arguments;
         process_message : subprogram application;};
     connections
       data access buffer -> get_message.buffer;
       parameter get_message.req -> process_message.msg;
     end execution.simple;
     
     subprogram arguments
     features
       req : out parameter message;
       buffer : requires data access data_buffer;
     end arguments;
     
     subprogram application
     features
       msg : in parameter message;
     end application;

By applying the mapping, we obtain the following Petri net:

images/mubroker_complet.png