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.

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.