Due to the complexity of modern software, documentation formalisms like UML are increasingly used as a way of having a general perspective on the architecture of an application, like a hierarchy of classes (Verics features a special UML for BMC module). Here we will discuss a generation of models from common source in Java to:

  • a network of timed automatons for PRISM;
  • an architectural overview represented in AADL.

The representation in AADL won't be as detailed as that of the timed automatons (although AADL has an extension which supports state machines, so theoretically it could be done). Yet, the AADL model will contain enough data for a basic analysis using the OSATE environment.

1 Java source

The prerequisite here is an explicit declaration of the important interconnections in a Java application, so that it is known what is to be represented as a process in AADL. We will do this by extending the producer/consumer components of the MiRelA language, normally used for modelling real-time systems. The components (classes to extend) can be found in the compiler's library.

Let us design a simple video acquisition system, which consists of a camera, an Ethernet bus and finally a video processor. Let the camera produces produces periodically a frame. This can be done by creating a thread, which waits in a loop for a synchronisation with a timer. After each synchronisation it calls an abstract method periodic() which we are going to implement as follows:

    @Override
    public void periodic() {
        Sleep.exact(acqTime);
        Sleep.max(compressMaxTime);
        produce();
    }
The first statement represents a constant acquisition time of a frame (an exposure and digitization in a CMOS matrix) and the second one depicts a variable compression time, the variability expressing a changing complexity of the acquired image. The third statement sends the frame to a consumer, in this case an Ethernet bus. We would like to support an AADL property transmission_time, which defines two values fixed and perbyte, which mean respectively a fixed latency per a single packet and an additional latency per each byte in the packet. In order to compute the total time from these two values, let us put the following code in a method addProducer, called on a consumer whenever a producer (in this case the camera) is added:
    transmissionTotal = transmissionFixed.getSum(
        transmissionPerByte.getProduct(packetSize));
The library provides that the value packetSize is automatically inherited by consuments from producers.

See that we multiply the transmission time per byte with the packet size not with a simple operator, but with a call to a method getProduct(). This is because any time definition in MiRelA is in general an abstract delay and not a concrete value. Different implementations provide e.g. a simple, fixed period or a probabilistic distribution of a number of periods, suitable for a probabilitic model checking with Prism.

The thread method of the discussed Bus component is straightforward:

    @Override
    public void run() {
        while(true) {
            sync.consume();
            transmissionTotal.sleep();
            produce();
        }
    }

The call produce() will in this example be connected to another custom class VideoProcessor.

All the producer/consumer connections are specified in the main method:

    public static void main(String[] args) {
        Mirela m = new Mirela();
        Camera cam = new Camera(m, new Delay(0), FRAME_PERIOD,
                CAMERA_ACQ_TIME, CAMERA_SEND_MAX_TIME);
        Bus eth = new Bus(m,
                new Delay(ETH_TRANSMISSION_TIME_FIXED),
                new Delay(0, ETH_TRANSMISSION_TIME_PER_BYTE_MAX));
        cam.addOut(eth, FRAME_SIZE);
        VideoProcessing vp = new VideoProcessing(m,
                new Delay(VIDEO_PROCESSING_PHASE),
                FRAME_PERIOD, VIDEO_PROCESSING_MAX_TIME);
        eth.addOut(vp);
        m.enable();
    }    

2 Output

After a compilation with Verics with enabled AADL output, we get an architectural overview with computed respective properties, e.g. the bus definition

    bus m_Bus_0
    properties
        transmission_time => [ fixed => 2 ms .. 3 ms; ];
    end m_Bus_0;
The same bus, compiled from the same sources to a state machine for Prism, is represented as follows
    module m_Bus_0

        s0 : [0..2] init 0;
        x0 : clock;

        invariant
            (s0=1 => x0 <= 3)
        endinvariant

        [PairBarrier1_0] (s0=0) -> (s0'=1) & (x0' = 0);
        [] (s0=1) & (2 <= x0) & !enabled_urgent -> (s0'=2);
        [PairBarrier3_0] (s0=2) -> (s0'=0);

    endmodule
See the elsewhere defined guard !enabled_urgent, which enables a synchronisation urgency.

The compiler takes care of finding all possible end-to-end flows automatically, e.g. here our AADL system definition is as follows:

    system implementation ImageAcquisitionSystem_sys.i
    subcomponents
            m_Camera_0_prs  : process m_Camera_0.i;
            m_Bus_0_bus     : bus m_Bus_0;
            m_VideoProcessing_0_prs : process m_VideoProcessing_0.i;
    connections
            c0: port m_Camera_0_prs.dataOut -> m_VideoProcessing_0_prs.dataIn
                    {actual_connection_binding => (reference(m_Bus_0_bus));};
    flows
            f0 : end to end flow m_Camera_0_prs.fOut -> c0 -> m_VideoProcessing_0_prs.fIn;
    end ImageAcquisitionSystem_sys.i;
which produces the following AADL diagram:

3 Conclusion

The multi-format output allows a multitude of analyses and applications using only a single input representation (i.e. the source in Java). The Prism part can be used to compute e.g. complex CTL properties to detect infinite waitings, temporal deadlocks or livelocks. The AADL part can be analysed in the OSATE environment, for example to check if the end-to-end flows respect the specifications.


Files:


Command line:

  • hc -U -v0 -op -sh -i -Da Camera.java VideoProcessing.java ImageAcquisitionSystem.java