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:
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:
- Camera.java, Bus.java, VideoProcessing.java, ImageAcquisitionSystem.java: source of the model;
- ImageAcquisitionSystem.nm: resulting timed automatons;
- ImageAcquisitionSystem.aadl: architecture;
Command line:
hc -U -v0 -op -sh -i -Da Camera.java VideoProcessing.java ImageAcquisitionSystem.java