Seven-pro is my PhD project which is done in collaboration between Software Technology group at Darmstad University of Technology (Germany) and ReDCAD research unit at National School of Engineers of Sfax (Tunisia).
Seven-pro is a holistic and generic approach that combines formal methods and aspect-oriented programming for specifying and runtime enforcing nonfunctional safety properties. Seven-pro covers the whole development process of nonfunctional properties and avoids the gap between the specification and the implementation by automatically generating aspects from a high-level specification. The generated aspects will be integrated, in modular way, in the functional application code for enforcing the formally specified properties at runtime. Seven-pro covers different types of non-functional properties in distributed applications. This approach is applied to structural, qualitative and quantitative behavioral non-functional properties: Software architectural proeprties, access control policies, and temporal properties in Web service compositions.
Contributors: Slim Kallel, Anis Charfi, Mohamed Jmaiel, and Mira Mezini
Web site (My PhD Thesis): TUD Library link


AO4AADL is an aspect oriented architectural language for embedded systems. Our language manipulates aspect oriented concepts at the software architecture level in order to master complexity and ensure scalability of such systems. AO4AADL is an aspect oriented extension for AADL. This language considers aspects as an extension concept of AADL components called aspect annex. Instead of defining a new aspect oriented ADL, we extend AADL, a well-known ADL, with an aspect annex. So we consider, in this work, that aspects can be specified in a language other than AADL, and then integrated in AADL models as annexes. Based on the annex extension mechanism, we propose to enrich AADL specifications with aspect concepts.
Contributors: Sihem Loukil, Slim Kallel, Bechir Zalila, and Mohamed Jmaiel
Web site:


Meidya is an “end-to-end” approach that supports dynamic reconfiguration of software architectures taking advantage of graphical modeling, formal methods and aspect-oriented programming. There are three ingredients of the proposal. The specification end of the solution is covered by a new UML profile enabling to specify the desired architectural style (model), its invariants and the intended reconfiguration operations. In order to verify the consistency of the model and the preservation of the invariants after every reconfiguration,weautomatically generate formal specifications in Z notation from the defined model. At the runtime enforcing end of the solution, we propose to encode the enforcement logic as aspect in the AspectJ language. The third important ingredient that makes our approach end-toend is the automatic translation of formal specifications into aspect-based enforcement code.
Contributors: Slim Kallel, Mohamed Hadj Kacem, and Mohamed Jmaiel
Web site:

Secure Mobile Agent System

This project consists of proposing a methodology for specifying and enforcing secure mobile agnet systems. First, we proposed an approach for enforcing a formal security model of Mobile agent system, which is proposed in the PhD thesis of Monia Loulou. A Z specification of the security model is automatically translated to JBOSS-AOP for enforcing the defined constraints. Second, we propose a new approach, which profits from MDA approach and combined their powers with those of Aspect Oriented Programming. We proposed two UML profiles for modeling the security and the mobility aspects of Mobile agent systems. We propose a mechanism for transforming a PIM model into a PSM model describing partially the AGLETS platform (Model2Model). After that, we automatically generate two type of code: (i) A Java code which corresponds to the main functionalities of the systems, (ii) a skeleton of aspects for enforcing the defined constraints specified in OCL language (Model2Code).
Contributors: Molka Rekik, Houssem Aloulou, Slim Kallel, Monia Loulou, and Ahmed Hadj Kacem