Abstract The automated planning community has developed a defacto standard planning language called PDDL. Using the PDDL tools, the reliability of PDDL descriptions can only be posterior examined. However, the Event-B method supports a rich refinement technique that is mathematically proven. Indeed, the Event-B method relies on a first-order predicates language and sets (including mathematical functions and relations) to model the data and on a simple action language to model the treatments. A model described in Event-B includes static modeling elements (sets, constants, axioms and theorems) and dynamic modeling elements (variables, invariant properties and events). Moreover, the Event-B method allows the step-by-step correct construction of Event-B models. To specify and solve the planning problems, a development process based on the combination of Event-B and PDDL is proposed. Our development process favors the obtaining of reliable PDDL description from an ultimate Event-B model using our Event-B2PDDL Eclipse plugin. Our process is successfully experimented on the sliding puzzle game.

The formal Event-B method makes it possible to obtain systems or software correct by construction. The modeling activity aims to establish formal models in Event-B. As for the proof activity, it aims at correcting these models. A proven Event-B model is not necessarily valid. We propose to open the Event-B formal method on PDDL in order to further validate Event-B models. We aim to validate the dynamic properties related to the sequence of events authorized on Event-B models. PDDL is a de facto standard language for planning problems. It is equipped with planners to automatically generate solution-plans. To achieve this, we successfully used the MDE approach, Xtext to create an integrated development environment specific to the Event-B language and the Xtend tool to implement our transformation EventB2PDDL and produce PDDL descriptions using a top-down approach.

Automatic planning has a de facto standard language called PDDL for describing planning problems. The dynamic analysis tools associated with this language do not allow sufficient verification and validation of PDDL descriptions. Indeed, these tools, namely planners and validators, allow a posteriori error detection. In this paper, we recommend a formal approach coupling the two languages Event-B and PDDL. Event-B supports a formal development process based on the refinement technique with mathematical proofs. Thus, we propose a refinement strategy for obtaining reliable PDDL descriptions from an ultimate Event-B model that is correct by construction. The correctness is guaranteed via the verification and validation tools supported by Event-B. We have chosen the MICONIC application managing modern elevators to illustrate our approach while recognizing that the MICONIC application is already modeled in PDDL without formal proof of its correctness.

In this paper, we investigate how patterns could be used in order to generate Event-B refinements automatically through DSL(s) for temporal, timed or distribution patterns. Our ultimate goal is to generate code for a concurrent, or distributed framework, e.g., BIP.

Behavioral consistency of cloud architectures is one of the pivotal challenges in cloud computing. In this paper, we propose a new approach for checking the behavioral consistency of the topology and orchestration of cloud computing. To do so, we choose TOSCA language in order to describe the cloud application. Then, we exploit the Wright ADL that encompasses the CSP language to check the consistency of cloud architectures using FDR2 model-checker.

Service Component Architectures (SCA) is widely used for the integration of heterogeneous applications. This heterogeneity, added to the distributed aspect of SCA, can be a source of behavioral mismatches. In this paper, we present a new approach for behavioral verification of SCA software architectures. More precisely, we propose a translation of a SCA source model to a Wright ADL configuration. In order to facilitate this translation, a guiding script and translation rules are introduced. Then, by using the wr2fdr tool, the translation of this wright configuration to a CSP specification is done. Finally, the FDR2 model-checker simulates and checks the obtained specification.

Today, a critical issue for complex systems design is the modeling and analysis of its architectures. Different ADLs support analyzers of different properties. For example, Unicon and MetaH allow the analysis of specific qualitative properties such as safety and security levels, while Rapide is focused on the dynamic aspect of architectures. However, the Wright ADL defines eleven standard properties related to the consistency and completeness of software architectures. These standard properties are automated and analyzed by the Wr2fdr tool accompanying the Wright ADL. In addition, the Wr2fdr tool can translate a Wright specification into another CSP acceptable by the FDR2 model-checker. Following the importance of this Wr2fdr tool, a maintenance activity of this tool was proposed in this paper. Our maintenance activity was mainly related to the implementation of these Wright standard properties. To achieve this, a functional testing and a reverse engineering were used.

Currently, much research looks at treating the behavior properties beginning with the architectural design phase in SCA (Software Component Architectures) based applications. In this paper,we propose to map SCA onto the Wright ADL in order to verify the behavioral consistency of SCA software architectures. To achieve this goal, we suggest translating this source software architecture into a Wright configuration. Using Wr2fdr tool, this Wright configuration can be automatically translated to a CSP specification acceptable by the FDR2 model-checker.

The component approach aims at reutilization by an easy and efficient component assembly. A coherent component assembly requires that the atomic components be correct. Where, an atomic component is said correct if and only if its partial behaviors associated with the interfaces offered by this component are ensured by the global behavior of the said component. In this paper, our purpose was the verification of the behavioral consistency between the interfaces of a component and the component itself. Our proposed approach combined UML2.0, Port State Machine (PoSM), Wright and CSP to check the behavioral consistency of UML2.0/PoSM components. To achieve this, we proposed to translate each UML2.0/PoSM component to a Wright Component. Using Wr2fdr tool, these Wright components were automatically translated to a CSP specification acceptable by the FDR2 model-checker. Thus, the consistency of a component was checked thanks to FDR2.

The qualitative properties are conventionally considered after completing the software. Currently, many research look at treating those properties as soon as the architectural design phase. In this paper, the modeling and the verification of these properties in UML2.0 software architectures are aimed. In order to achieve this, we proposed a profile that extends the UML2.0 component meta-model. The new profile, called CUMLQoS, is able to model the UML2.0 software architectures equipped with qualitative properties. Our verification approach, which is based on the qualitative contracts established between both server and client components, propose to use the Acme/Armani ADL as a checking machine of UML2.0 software architectures that derives from our CUMLQoS profile. This choice of this ADL is justified by its ability to formal verification of different types of properties related to software architectures.

Verifying Web service composition in a dynamic environment remains one of the most difficult tasks despite the efforts and the previous proposed research works because new services can be composed during the execution step and others can automatically appear, disappear, or be updated. To achieve the Web service composition specification and verification, we introduce a new concept, called dynamic pattern. A dynamic pattern is an extension of a static one. Then, we propose to formalize dynamic Web Service composition in Event-B using dynamic patterns. The resulting model is progressively verified using proofs. We use animator of model (ProB) to detect a variety of problems, such as deadlocks or other unexpected behavior of a model.

Service Component Architecture specification (SCA) is an emerging and promising technology for the development, deployment and integration of Internet applications. This technology supports the management of dynamic availability and treats the heterogeneity between the components of distributed applications. However, this technology is not able to solve all problems. Currently, software systems are evolving. This factor makes development, verification and maintenance of systems more complex than before. One solution to remedy this was the use of the Model Driven Engineering (MDE) approach in the development and verification process. The purpose of this paper is to apply an approach MDE to obtain SCA models and to verify the properties of these models. To reach our purpose, we applied two transformations: The first one to obtain SCA models using UML 2.0 metamodel and the second transformation to ensure the verification of the properties of these models using event-B metamodel. To achieve this, we study the UML 2.0 component metamodel, the SCA metamodel and the event-B metamodel. We have defined transformation rules in ATL language.

In this paper, the work developed aims at contributing to the research related to the Quality of Service (QoS) for Web services. The aim of this research is twofold, first, it helps the designers and developers to provide better web services and second, and it helps ensure consistent software architecture as a reference model for many applications. To achieve this, we model, first, the meta-QoS model of the Web services. Then, we formalize the QoS of the Web services by referring to ARMANI. We also, handle the mediation of the composite Web services with the ACME using an automatic MDE approach and implementing a tool for this aim: Web services compositions are transformed onto ACME specifications.

SOA (Service Oriented Architecture) defines a new Web services cooperation paradigm in order to develop distributed applications using reusable services. The handling of such collaboration has different problems that lead to many research efforts. In this paper, we address the problem of Web service composition. Indeed, various heterogeneities can arise during the composition. The resolution of these heterogeneities, called mediation, is needed to achieve a service composition. In this paper, we propose a sound approach to formalize Web services composition mediation with the ADL (Architecture Description Language) ACME. To do so, we first model the meta model of composite service manager and mediation. Then we specify semi formal properties associated with this meta model using OCL (Object Constraint Language). Afterwards, we formalize the mediation protocol using Armani, which provides a powerful predicate language in order to ensure service execution reliability.

The components based approach aims at the re-use by an easy components assembly. Vis-a-vis to the objects based approach, the component based approach moves the complexity of a graph of classes (hierarchy of classes and client relationship) to connection points of between the components. The principal lock of the components based approach is the difficulty of deduction of the components assembly properties from the components themselves taken individually. In this paper, we present an MDE (Model driven Engineering) checking approach of component assembly based on the ADL (Architecture Description language) Acme/Armani. The proposed approach can be applied on several component models such as UML 2.0. We aim to check the structural and non-functional properties on a component assembly. Thereafter, we apply the proposed checking approach to the UML 2.0 component model.