ENST
Abstract: this talk is devoted to the presentation of an integrated framework for modeling, implementing and verifying systems with a maximum confidence in the resulting critical system. We will present a semi-automatic approach to test generation which is materialized in the test intention language SATEL (Semi-Automatic Testing Language) for CO-OPN (Concurrent Object Oriented Petri Nets). The approach is semi-automatic in the sense that we allow the test engineer to state test purposes (which we call in our approach test intentions), while using unfolding techniques (introduced by Bernot, Gaudel and Marre) for automatically finding equivalence classes of inputs to operations of the model. While designing the test language it was our intention to explicitly make use of the test engineer's knowledge in the test generation process. He/she is able to express which parts of the model are relevant for testing and to impose limits on how that testing should be performed. With SATEL we have tried to devise a test generation framework that automates the typical approach of a test engineer rather than performing an exhaustive search of the model. The semi-automatic aspect SATEL corresponds to the fact that, given an operation of the model (from a black-box perspective), the test engineer will be also be able to state that the generated tests should include inputs that automatically cover the various behaviors (also called in the literature equivalence classes) of that operation. The test intentions in SATEL correspond to generalizations of the behavior of the SUT and are expressed by writing execution patterns with variables over sequences of input/output events of the specification --- one could also see them as testing macros. The instantiation of these variables by the test language compiler will yield test cases for the specified test intentions. We have also included in SATEL support for non-determinism at two levels. Firstly the formalism in which we express our tests is the HML (Hennessy-Milner logic) which is a branching temporal logic. In this way we are able to express tests which reflect non-deterministism both at the level of the specification and of the SUT. Secondly we have included in our language a means of treating a specific kind of non-determinism of the SUT while it is interacting with the environment. This is done by anticipating a reply (a stimulation) to a given non-deterministic observation by means of a predefined function at the level of the specification. SATEL has been implemented in our framework CoopnBuilder environment and we are currently validating our approach by applying it to an industrial case study.
Abstract: Currently, Web Services are the fitted technical solution to implement Service Oriented Architecture (SOA). However, this technology presents limitations concerning dynamic service adaptabilty. From one side, Web Services providers have no mean to dynamically adapt an existing Web Service to business requirements changes. From the other side, Web Services clients have no way to dynamically adapt themselves to the service changing in order to avoid execution failures. In this presentation, we show how we achieve a dynamic adaptable SOA by introducing the Aspect Oriented Programming (AOP) paradigm and Process Algebra (PA). We apply the main AOP concepts (joinpoint, pointcut and advice) in the Web Service context to modify the behaviour of an existent Web Service without touching its implementation. Then, we propose a Process Algebra formalism to specify a change-prone BPEL process (base service and aspect services). This formalization led us to generate automatically a client which dynamically adapt its behaviour to the service changes.