Model-driven transformations play a central role in MDE processes, yet their correctness is most often validated through testing or simulation. However, in contexts where critical scenarios may compromise system integrity or certification objectives, stronger guarantees are necessary. This paper investigates how the B method can support transformation engineering through verified formal specifications. To this end, we developed BCerT, an extension of the Meeduse language workbench, originally dedicated to the formal modeling of domain-specific languages. In our approach, transformations are defined as B operations or B events, allowing animation and model checking with ProB, as well as theorem proving with Atelier B. We discuss three complementary specification strategies: (i) a rule-oriented modeling approach optionally controlled with CSP||B; (ii) a property-driven operational B specification in which the transformation is expressed as a relation constrained by invariants; and (iii) an Event-B system capturing the transformation as atomic events focused on the end state. The approach is illustrated through two applications: the verification of a Truth Tables to Binary Decision Diagrams transformation presented at the Transformation Tool Contest, and the development of U2BCerT, a certified transpiler from UML state machines to Event-B.

Federated Learning has been introduced as a new machine learning paradigm enhancing the use of local devices. At a server level, FL regularly aggregates models learned locally on distributed clients to obtain a more general model. Current solutions rely on the availability of large amounts of stored data at the client side in order to fine-tune the models sent by the server. Such setting is not realistic in mobile pervasive computing where data storage must be kept low and data characteristic can change dramatically. To account for this variability, a solution is to use the data regularly collected by the client to progressively adapt the received model. But such naive approach exposes clients to the well-known problem of catastrophic forgetting. To address this problem, we have defined a Federated Continual Learning approach which is mainly based on distillation. Our approach allows a better use of resources, eliminating the need to retrain from scratch at the arrival of new data and reducing memory usage by limiting the amount of data to be stored. This proposal has been evaluated in the Human Activity Recognition (HAR) domain and has shown to effectively reduce the catastrophic forgetting effect.

Pervasive computing promotes the installation of connected devices in our living spaces in order to provide services. Two major developments have gained significant momentum recently: an advanced use of edge resources and the integration of machine learning techniques for engineering applications. This evolution raises major challenges, in particular related to the appropriate distribution of computing elements along an edge-to-cloud continuum. About this, Federated Learning has been recently proposed for distributed model training in the edge. The principle of this approach is to aggregate models learned on distributed clients in order to obtain a new, more general model. The resulting model is then redistributed to clients for further training. To date, the most popular federated learning algorithm uses coordinate-wise averaging of the model parameters for aggregation. However, it has been shown that this method is not adapted in heterogeneous environments where data is not identically and independently distributed (non-iid). This corresponds directly to some pervasive computing scenarios where heterogeneity of devices and users challenges machine learning with the double objective of generalization and personalization. In this paper, we propose a novel aggregation algorithm, termed FedDist, which is able to modify its model architecture (here, deep neural network) by identifying dissimilarities between specific neurons amongst the clients. This permits to account for clients' specificity without impairing generalization. Furthermore, we define a complete method to evaluate federated learning in a realistic way taking generalization and personalization into account. Using this method, FedDist is extensively tested and compared with three state-of-the-art federated learning algorithms on the pervasive domain of Human Activity Recognition with smartphones.

In this paper, we present a model-based testing tool resulting from a research project, named TASCCC. This tool is a complete tool chain dedicated to property-based testing in UML/OCL, that integrates various technologies inside a dedicated Eclipse plug-in. The test properties are expressed in a dedicated language based on property patterns. These properties are then used for two purposes. First, they can be employed to evaluate the relevance of a test suite according to specific coverage criteria. Second, it is possible to generate test scenarios that will illustrate or exercise the property. These test scenarios are then unfolded and animated on the Smartesting's Certify It model animator, that is used to filter out infeasible sequences. This tool has been used in industrial partnership, aiming at providing an assistance for Common Criteria evaluations, especially by providing test generation reports used to show the link between the test cases and the Common Criteria artefacts.

This paper describes the Tobias tool. Tobias is a combinatorial test generator which unfolds a test pattern provided by the test engineer, and performs various combinations and repetitions of test parameters and methods. Tobias is available on-line at tobias.liglab.fr . This website features recent improvements of the tool including a new input language, a traceability mechanism, and the definition of various ``selectors'' which achieve test suite reduction.

.Design and development scalability, in any engineering, requires information hiding and a specific composition mechanism in which composite items are made-up of other items. This paper shows that scalability is currently ill supported and that software engineering composites are rather special with respect to other engineering disciplines. Indeed, a software engineering composite is simultaneously a model element, an engineering artifacts and a real object, which is unprecedented in the history of engineering. This paper analyzes the requirements that composites must satisfy in order to support scalability in software engineering. We have developed CADSE (Computer Aided Domain Specific Environment) in which composites are first class elements from which workspaces, concurrent engineering and view point support are provided. The paper discusses our experience with using the proposed system over the last years.

Computer aided software engineering tools represent one the main successes of software engineering in the past decades. They however need to be improved along several dimensions in order to face new challenges due to ever more complex applications, more heterogeneous technologies and more stakeholders involved. In this paper, we present an approach based on the concept of domain. We define a domain as an area in which a number of stakeholders is repeatedly performing similar activities. In a project, an arbitrary number of domains can be identified, being business, technical, or related to life cycle activities. In our metamodel-based approach, any domain can be easily modelled and the corresponding computer aided domain specific engineering environment (CADSE) can be generated. Using CADSE composition, complete and wide scope engineering environments can be built as a composition of an arbitrary number of domains. The paper presents the approach, the technology and draws a few lessons of the first years of use in a number of real projects.

Product Data Management (PDM) and Software Configuration Management (SCM) are the disciplines of building and controlling the evolution of a complex artifacts; either physical or software. Surprisingly, these two fields have evolved independently; their respective solutions to the same problems are incompatible and their properties are different. PDM is good at modeling while SCM is good at building and supporting concurrent engineering. From a software engineering perspective, the challenge is to take the full potential of strong modeling capabilities, while preserving good concurrent engineering support. The paper shows that rich modeling, flexible evolution, and concurrent engineering supports have conflicting requirements and that a solution requires rethinking the concepts of evolution, versioning and modeling. We have developed a system, called CADSE (Computer Aided Domain Specific Environment), in which a product (software, physical or both) is modeled in a way similar to PDM and in which concurrent engineering and evolution is supported in the SCM way. To that end, the system is driven by models; evolution alone being defined through different models. The paper describes our system and discusses the early lessons of its first years of practical use.

Reuse has always been a major goal in software engineering, since it promises large gains in productivity, quality and time to market reduction. Practical experience has shown that substantial reuse has only successfully happened in two cases: libraries, where many generic and small components can be found; and product lines, where domains-specific components can be assembled in different ways to produce variations of a given product.In this paper we examine how product lines have successfully achieved reuse of coarse-grained components, and the underlying factors limiting this approach to narrowly scoped domains. We then build on this insight to present an approach, called software federation, which proposes a mechanism to overcome the identified limitations, and therefore makes reuse of coarse-grained components possible over a larger range of applications. Our approach extends and generalizes the product line approach, extending the concepts and mechanisms available to manage variability. The system is in use in different companies, validating the claims made in this paper.