Publications internationales
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.
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.
Communications internationales
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.