Soleil framework is based on the Hulotte experience and apply it to the Real-time and Embedded Java applications. The basic goal of the framework is to alleviate Real-time Java system development through a systematic architecture design and automatic generation of real-time Java source code.
asdfasd ads asd fasd fasdf
As already said, Soleil, Hulotte is integrating two model checking tools - Java PathFinder and BPChecker. Both the tools are cooperating in order to successfully verify a component implementation.
Because Soleil, Hulotte is able to verify a component itself, without need for any addition code implementing an environment of the component, it was necessary to modify the JPF implementation which is available to verify only a closed system. Therefore, we introduce the second model checker - BPChecker which is replacing the missing environment, generates incoming activities on component interfaces and thus simulates the environment.
The idea of the environment simulation, together with the integration of two autonomous model checkers, are the key features of the implemented solution.
The biggest challenge of the solution is to make the model checkers cooperate on the verification process. We achieve this by introducing an arbitrating unit called Manager which is managing the communication between both the tools and controls the process of verification.
On the following picture we can see an architecture of the whole system. The component under discussion is represented by the inner state of JPF, which is being traversed in search for property violations. JPF is reporting the state of the verification through the special connecters to the Manager that is together with BPChecker evaluating the state of the verification. During this process Manager directs the verification, simulates the component's environment and evaluates component's behavior.
To show the quality of our framework, we have conducted several benchmark tests to measure performance of the framework. The main goal was to show that our framework does not intro- duce any non-determinism and to measure the performance/memory-consumption overhead of the framework.
As one of the means of evaluation, we compare differently optimized applications developed in our framework against a manually written object-oriented application.
This diagram shows that the overhead of the framework is minimal when considering the highly-optimized distribution(the most right measurements) with the same application implemented manually(the most left measurements).
Also, we demonstrate a fitness for embedded platforms by achieving a memory footprint reduction (ULTRA MERGE) that provides better results than the OO-approach.
v