Section: New Results

NorthBound results

Another key issue in the Amazones architecture was to bring together formal methods and service oriented programming such as OSGi/Java approach. We developped the Logos framework that observes and records communications that occurs between an OSGi client and a corresponding server. This architecture is developed in the LISE ANR project, and we made various improvements to the architecture.

Amazones Protocol

It aims at building automata from running and observing applications. The logos framework observes a running application at builds at run-time an automata that represents the application behavior. Julien Ponge wrote the corresponding Scala code.

Monitored oriented programming

Another Logos extension integrates Monitored Oriented architectures such as JavaMOP and Larva. We are currently using and working with the larva people. Each time we intercept a call, it is transfered to the Larva automata manager.

Real time SOA

Admission control for service oriented application in real time infrastructure. This work led by Lionel Morel tries to bring together real time architecture configuration and component based architectures. The deal is to find a better way of managing the dynamicity of applications in real time context.

B Model Slicing to Generate Tests

In a model-based testing approach as well as for the verification of properties, B models provide an interesting modelling solution. However, for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used. The abstraction is often a domain abstraction of the state variables that requires many proof obligations to be discharged, which can be very time consuming for real applications.

we propose a contribution to this problem that complements an approach based on domain abstraction for test generation, by adding a preliminary syntactic abstraction phase, based on variable elimination. We define a syntactic transformation that suppresses some variables from a B event model, in addition to three methods that choose relevant variables according to a test purpose. This way, we propose a method that computes an abstraction of a source model $M$ according to a set of selected relevant variables. Depending on the method used, the abstraction can be computed as a simulation or as a bi-simulation of $M$. With this approach, the abstraction process produces a finite state system. We apply this abstraction computation to a Model Based Testing process. We evaluate experimentally the impact of the model simplification by variables elimination on the size of the models, on the number of proof obligations to discharge, on the precision of the abstraction and on the coverage achieved by the test generation.

This work is based on a B model approach. However, in the context of AMAZONES, one of our objectives is to extend it, in order to consider models automatically generated from the usage a the tested service on a particular context.

Distributed Data Centric Programs Verification

Netlog is a language designed to describe distributed programs. It has a precise semantics, provides a high-level of abstraction thanks to its datalog flavor and benefits from an efficient implementation. This makes it a very interesting target language for proofs of distributed programs. In [34] , with the Coq proof assistant, we formalized the distributed computation model based on message passing with either synchronous or asynchronous behaviors; built the translation of Netlog programs; modeled the embedded machine evaluating Netlog programs, and thus established a framework to formally verify properties of distributed programs in Netlog. To test the framework, we proved the correctness of a concrete distributed program for constructing spanning trees over connected graphs.

Managing dynamic service substitution at runtime

The service oriented approach is a paradigm allowing the introduction of dynamicity in developments. If there are many advantages with this approach, there are also some new problems associated to service disappearance. The particular case of service substitution is often studied and many propositions exist. However, proposed solutions are mainly server-side in the context of web-services.

In this work, we propose a client side API-based approach to allow service substitution without any restart of the client and without any assumption on external services. Our proposition is based on a transactional approach, defined to authorized substitutions of services dynamically, by preserving the current run and collected data.

We designed a framework organized by Julien Ponge [14] .