Publications internationales

2021
Toufik Benouhiba. (2021), A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models. Fundamenta Informaticae : IOS Press, https://content.iospress.com/articles/fundamenta-informaticae/fi2011

Résumé: Probabilistic models play an important role in many fields such as distributed systems and simulations. Like non-probabilistic systems, they can be synthesized using classical refinement-based techniques, but they also require identifying the probability distributions to be used and their parameters. Since a fully automated and blind refinement is generally undecidable, many works tried to synthesize them by looking for the parameters of the distributions. Syntax-guided synthesizing approaches are more powerful, they try to synthesize models structurally by using context-free grammars. However, many problems arise like huge search space, the complexity of generated models, and the limitation of context-free grammars to define constraints over the structure. In this paper, we propose a multi-step refinement approach, based on meta-models, offering several abstraction levels to reduce the size of the search space. More specifically, each refinement step is divided into two stages in which the desired shape of models is first described by context-sensitive constraints. In the second stage, model templates are instantiated by using global optimization techniques. We use our approach to a synthesize a set of optimal probabilistic models and show that context-sensitive constraints coupled with the multi-level abilities of the approach make the synthesis task more effective.

2014
Toufik Benouhiba, Amina Boudjedir. (2014), On using pre and postconditions to tackle the aspect scheduling problem by rewriting systems: a design-level approach. Journal of Object Technologyhttp://www.jot.fm/issues/issue_2014_12/article1.pdf

Résumé: The aspect-oriented paradigm promises separation of crosscut- ting concerns by modularizing them as aspects. This paradigm allows then weaving aspects upon some points in the base system. Unfortunately, the interaction of aspects may have an undesirable effect on each other and/or on the base system if they are executed in any order. Many works tried to solve this problem but the proposed solutions were either limited to some simple models of aspects or used to check if a set of temporal properties is preserved when aspects are introduced. In this paper, we propose a framework based on extended UML diagrams (class and state/transition diagrams) in order to make the detection of undesirable interaction more powerful and realistic. This framework relies on finite state automata (FSA); it transforms the interaction problem into a reachability issue. In fact, bad interaction is expressed as a generic LTL property which is inde- pendent of the system to be verified. This property can be checked using any model-checker like Maude. To concretize the proposed framework, we propose a rewriting system that allows an implicit construction of the FSA of the base system and the aspects in addition to the aspects composition and the weaving mechanism. Therefore, the proposed system defines a translation scheme of UML models into rewriting logic specifications writ- ten in Maude language. Thanks to the advances of the on-the-fly technique in Maude, the use of its LTL model-checker avoids a systematic exploration of all possible combinations of the aspects. The approach will be illustrated by a case study in order to explain how it works.

2006
Toufik Benouhiba, Jean-Marc Nigro. (2006), An Evidential Cooperative Multi-Agent System. Expert systems with applictions : Elservier,
2005
(2005), An Evidential and Genetic Method for Cooperative Learning Systems. Multi-agent and Grid Systems—An International Journal, Vol 1(1) : IOP Press,

Communications internationales

2018
Moncef Trima, Toufik Benouhiba. (2018), Graphical notation and tool to design JCSP programs. ISPS'2018https://ieeexplore.ieee.org/abstract/document/8379013

Résumé: Java for CSP (JCSP) is a library based on Communicating Sequential Processes (CSP) which is a formalism used for describing and formally verifying concurrent systems at a high level of abstraction. JCSP does not require advanced mathematical skills. However, the design, verification and test of JCSP systems can be hindered when done at the source code level. In this paper, we suggest an intermediate level of abstraction between CSP and JCSP in the form of a graphical notation close to JCSP components. This enables reasoning about the behavior of the developed system by using a familiar, abstract and yet executable notation. Hence, CSP models can still be abstracted when a formal verification is required, and the translation to JCSP code is simplified. A prototype tool supporting the notation is presented together with a design example. The tool enables the reuse of designed models as new building blocks, which may accelerate the design process.

2014
(2014), Specifying and verifying Aspect-Oriented systems in rewrite logic. ICAASE'2014, Constantine
2012
(2012), Learning Invariants Using Association Rules Technique. Sousse, Tunisie : ICITeS'12 (IEEE),
(2012), Targeted test adequacy criteria for search-based software testing. Sousse, Tunisie : ICITeS'12 (IEEE),
2011
(2011), A semi-formal approach for Java programs verification. Alger, Algérie : ISPS'11 (IEEE),
2010
(2010), Verification of Aspect Composition And Integration Using Rewriting Systems. Constantine, Algérie : MISC'10,
2006
(2006), Preventive Maintenance Optimisation Using Evolutionary Hybrid Algorithm. Troyes, France : IEEE International Conference on Service Systems and Service Management,
2004
(2004), Evidential Classifier System. Metz, France : MCO'2004 (Hermes),
2003
(2003), Uncertainty Management in Rule Based Systems, Application to Maneuvers Recognition. Oxford, England : KES'03 (Springer-Verlag),