References of "Amrani, Moussa 40020942"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailModel Transformation Intents and Their Properties
Lúcio, Lévi; Amrani, Moussa UL; Dingel, Jürgen et al

in Software & Systems Modeling (2014)

The notion of model transformation intent is proposed to capture the purpose of a transformation. In this paper, a framework for the description of model transformation intents is defined which includes ... [more ▼]

The notion of model transformation intent is proposed to capture the purpose of a transformation. In this paper, a framework for the description of model transformation intents is defined which includes, for instance, a description of properties a model transformation has to satisfy to qualify as a suitable realization of an intent. Several common model transformation intents are identified and the framework is used to describe five of them in detail. A case study from the automotive industry is used to demonstrate the usefulness of the proposed framework for identifying crucial properties of model transformations with different intents and to illustrate the wide variety of model transformation intents that an industrial model-driven software development process typically encompasses. [less ▲]

Detailed reference viewed: 124 (5 UL)
Full Text
Peer Reviewed
See detailSecurity@Runtime: A flexible MDE approach to enforce fine-grained security policies
Elrakaiby, Yehia UL; Amrani, Moussa UL; Le Traon, Yves UL

in Lecture Notes in Computer Science (2014), 8364 LNCS

In this paper, we present a policy-based approach for automating the integration of security mechanisms into Java-based business applications. In particular, we introduce an expressive Domain Specific ... [more ▼]

In this paper, we present a policy-based approach for automating the integration of security mechanisms into Java-based business applications. In particular, we introduce an expressive Domain Specific modeling Language (Dsl), called Security@Runtime, for the specification of security configurations of targeted systems. The Security@Runtime Dsl supports the expression of authorization, obligation and reaction policies, covering many of the security requirements of modern applications. Security requirements specified in security configurations are enforced using an application-independent Policy Enforcement Point Pep)-Policy Decision Point (Pdp) architecture, which enables the runtime update of security requirements. Our work is evaluated using two systems and its advantages and limitations are discussed. © 2014 Springer International Publishing Switzerland. [less ▲]

Detailed reference viewed: 165 (5 UL)
Full Text
Peer Reviewed
See detailA Survey of Formal Verification Techniques for Model Transformations: A Tridimensional Classification
Amrani, Moussa UL; Lúcio, Lévi; Selim, Gehan et al

in Journal of Technology (2014)

Detailed reference viewed: 230 (8 UL)
Full Text
Peer Reviewed
See detailA Flexible MDE approach to Enforce Fine- grained Security Policies
Elrakaiby, Yehia UL; Amrani, Moussa UL; Le Traon, Yves UL

in Proceedings of the International Symposium on Engineering Secure Software and Systems (2014)

In this paper, we present a policy-based approach for au- tomating the integration of security mechanisms into Java-based business applications. In particular, we introduce an expressive Domain Specific ... [more ▼]

In this paper, we present a policy-based approach for au- tomating the integration of security mechanisms into Java-based business applications. In particular, we introduce an expressive Domain Specific modeling Language (Dsl), called Security@Runtime, for the specification of security configurations of targeted systems. The Security@Runtime Dsl supports the expression of authorization, obligation and reaction policies, covering many of the security requirements of modern applica- tions. Security requirements specified in security configurations are en- forced using an application-independent Policy Enforcement Point (Pep)- Policy Decision Point (Pdp) architecture, which enables the runtime up- date of security requirements. Our work is evaluated using two systems and its advantages and limitations are discussed [less ▲]

Detailed reference viewed: 86 (9 UL)
Full Text
Peer Reviewed
See detailAdvances in Model-Driven Security
Lucio, Levi; Zhang, Qin UL; Nguyen, Phu Hong UL et al

in Memon, Atif (Ed.) Advances in Computers (2014)

Sound methodologies for constructing security-critical systems are extremely important in order to confront the increasingly varied security threats. As a response to this need, Model-Driven Security has ... [more ▼]

Sound methodologies for constructing security-critical systems are extremely important in order to confront the increasingly varied security threats. As a response to this need, Model-Driven Security has emerged in the early 2000s as a specialized Model-Driven Engineering approach for supporting the development of security-critical systems. In this chapter we summarize the most important developments of Model-Driven Security during the past decade. In order to do so we start by building a taxonomy of the most important concepts of this domain. We then use our taxonomy to describe and evaluate a set of representative and influential Model-Driven Security approaches in the literature. In our development of this topic we concentrate on the concepts shared by Model-Driven Engineering and Model-Driven Security. This allows us to identify and debate the advantages, disadvantages and open issues when applying Model-Driven Engineering to the Information Security domain. This chapter provides a broad view of Model-Driven Security and is intended as an introduction to Model-Driven Security for students, researchers and practitioners. [less ▲]

Detailed reference viewed: 347 (24 UL)
Full Text
See detailTowards the Formal Verification of Model Transformations: An Application to Kermeta
Amrani, Moussa UL

Doctoral thesis (2013)

Model-Driven Engineering (MDE) is becoming a popular engineering methodology for developing large-scale software applications, using models and transformations as primary principles. MDE is now being ... [more ▼]

Model-Driven Engineering (MDE) is becoming a popular engineering methodology for developing large-scale software applications, using models and transformations as primary principles. MDE is now being successfully applied to domain-specific languages (DSLs), which target a narrow subject domain like process management, telecommunication, product lines, smartphone applications among others, providing experts high-level and intuitive notations very close to their problem domain. More recently, MDE has been applied to safety-critical applications, where failure may have dramatic consequences, either in terms of economic, ecologic or human losses. These recent application domains call for more robust and more practical approaches for ensuring the correctness of models and model transformations. Testing is the most common technique used in MDE for ensuring the correctness of model transformations, a recurrent, yet unsolved problem in MDE. But testing suffers from the so-called coverage problem, which is unacceptable when safety is at stake. Rather, exhaustive coverage is required in this application domain, which means that transformation designers need to use formal analysis methods and tools to meet this requirement. Unfortunately, two factors seem to limit the use of such methods in an engineer’s daily life. First, a methodological factor, because MDE engineers rarely possess the effective knowledge for deploying formal analysis techniques in their daily life developments. Second, a practical factor, because DSLs do not necessarily have a formal explicit semantics, which is a necessary enabler for exhaustive analysis. In this thesis, we contribute to the problem of formal analysis of model transformations regarding each perspective. On the conceptual side, we propose a methodological framework for engineering verified model transformations based on current best practices. For that purpose, we identify three important dimensions: (i) the transformation being built; (ii) the properties of interest ensuring the transformation’s correctness; and finally, (iii) the verification technique that allows proving these properties with minimal effort. Finding which techniques are better suited for which kind of properties is the concern of the Computer-Aided Verification community. Consequently in this thesis, we focus on studying the relationship between transformations and properties. Our methodological framework introduces two novel notions. A transformation intent gathers all transformations sharing the same purpose, abstracting from the way the transformation is expressed. A property class captures under the same denomination all properties sharing the same form, abstracting away from their underlying property languages. The framework consists of mapping each intent with its characteristic set of property classes, meaning that for proving the correctness of a particular transformation obeying this intent, one has to prove properties of these specific classes. We illustrate the use and utility of our framework through the detailed description of five common intents in MDE, and their application to a case study drawn from the automative software domain, consisting of a chain of more than thirty transformations. On a more practical side, we study the problem of verifying DSLs whose behaviour is expressed with Kermeta. Kermeta is an object-oriented transformation framework aligned with Object Management Group standard specification MOF (Meta-Object Facility). It can be used for defining metamodels and models, as well as their behaviour. Kermeta lacks a formal semantics: we first specify such a semantics, and then choose an appropriate verification domain for handling the analysis one is interested in. Since the semantics is defined at the level of Kermeta’s transformation language itself, our work presents two interesting features: first, any DSL whose behaviour is defined using Kermeta (more precisely, any transformation defined with Kermeta) enjoys a de facto formal underground for free; second, it is easier to define appropriate abstractions for targeting specific analysis for this full-fledged semantics than defining specific semantics for each possible kind of analysis. To illustrate this point, we have selected Maude, a powerful rewriting system based on algebraic specifications equipped with model-checking and theorem-proving capabilities. Maude was chosen because its underlying formalism is close to the mathematical tools we use for specifying the formal semantics, reducing the implementation gap and consequently limiting the possible implementation mistakes. We validate our approach by illustrating behavioural properties of small, yet representative DSLs from the literature. [less ▲]

Detailed reference viewed: 168 (21 UL)
Full Text
Peer Reviewed
See detailTowards a Model Transformation Intent Catalog
Amrani, Moussa UL; Dingel, Jürgen; Lambers, Leen et al

in Proceedings of the First Workshop on Analysis of Model Transformations (2012)

Detailed reference viewed: 63 (0 UL)
Full Text
See detailInvariant Preservation in Interative Modelling (Extended Version)
Amrani, Moussa UL; Lúcio, Lévi; Syriani, Eugene et al

Report (2012)

Detailed reference viewed: 40 (3 UL)
Full Text
Peer Reviewed
See detailInvariant Preservation In Iterative Modeling
Lucio, Levi; Syriani, Eugene; Amrani, Moussa UL et al

in Workshop on Models And Evolution, co-located with MoDELS 2012 (2012)

In a Model-Driven Development project, models are typically built iteratively to better satisfy a set of requirements. Therefore it is crucial to guarantee that one iteration of a model evolution does not ... [more ▼]

In a Model-Driven Development project, models are typically built iteratively to better satisfy a set of requirements. Therefore it is crucial to guarantee that one iteration of a model evolution does not hinder the previous version. In this paper, we focus on invariant preservation of behavioral models expressed in Algebraic Petri Nets. The theory developed is applied to a Multi-Level Security File System modeled iteratively. We also discuss how this approach can be applied on Domain-Specific Languages that are translated to Algebraic Petri Nets. [less ▲]

Detailed reference viewed: 69 (1 UL)
Full Text
Peer Reviewed
See detailA Formal Semantics of Kermeta
Amrani, Moussa UL

in Mernik, Marjan (Ed.) Formal and Practical Aspects of Domain-Specific Languages: Recent Developments (2012)

This chapter contributes to the formal specification of Kermeta, a popular metamodelling framework useful for the design of DSL structure and semantics. The formal specification is tool-/tool syntax ... [more ▼]

This chapter contributes to the formal specification of Kermeta, a popular metamodelling framework useful for the design of DSL structure and semantics. The formal specification is tool-/tool syntax independent; it only uses classical mathematical instruments taught in usual computer science courses. This specification serves as a reference specification from which specialised implementation can be derived for execution, simulation, or formal analysis of DSLs. By providing such a specification, the chapter ensures that each and every DSL written in Kermeta, receives de facto a formal counterpart, making its definition fully formal. This radically contrasts with other approaches that require a new ad hoc semantics defined for every new DSL. The chapter briefly reports on two implementations conducted to demonstrate the feasibility of the approach. [less ▲]

Detailed reference viewed: 79 (7 UL)
Full Text
See detailA Formal Semantics of Kermeta
Amrani, Moussa UL

Report (2012)

Detailed reference viewed: 74 (0 UL)
Full Text
Peer Reviewed
See detailA Tridimensional Approach for Studying the Formal Verification of Model Transformations
Amrani, Moussa UL; Lucio, Levi; Selim, Gehan M. K. et al

in Proceedings of the First Workshop on Verification and Validation of Model Transformations (2012)

Detailed reference viewed: 68 (2 UL)