MeFoSyLoMa
Méthodes Formelles pour les Systèmes Logiciels et Matériels
Friday, January 23, 2009Aoumeur Nasreddine (University Magdeburg), Sana Younes (LACL Paris 12 & Prism-UVSQ)
14h00-15h00: Aoumeur Nasreddine (University Magdeburg) "Separation of concerns and composition for mastering today's multi-dimensional adaptive service-oriented business applications"
Abstract: As service technology is maturing, world-wide organizations are embracing it at rapid pace, by publishing, requesting and cooperating their know-how mainly through Web-services. As a consequence, complexity and competitiveness are tending to shift from pure monolithic process-centricity and rigidity towards dynamic agility and multi-dimensional knowledge-intensiveness. To conceptually address these emerging and pressing challenges, this presentation discusses a progressive and model-driven architectural approach. As key drivers behind this proposal, we emphasize particularly the following milestones. Firstly, we promote event-driven cross-organizational and multi-concern business rules to intrinsically tackle evolution and adaptability. Secondly, we respect a fine-grained activity-based vision instead of the mostly adopted holistic business process view. Thirdly, as certification underpinnings, we demonstrate how techniques akin to rewriting logic could best fitting the approach. Finally, for deployment phase we recapitulate on the strengths of aspect-orientation and XML-based rules. The approach is illustrated using a simplified case from E-banking.
15h00-15h30 : Sana Younes (LACL Paris 12 & Prism-UVSQ) "Stochastic model checking by stochastic comparison" Abstract: We propose a new method to verify Markov chains. The verification is performed by transient or steady-state distributions of the considered chain. We use stochastic comparison techniques to obtain bounding measures in order to verify the considered chain. These measures are obtained by the construction of a bounding chain to the initial chain that can be very large. Bounding models have to be easier to analyze that let to consider models for which numerical analysis are difficult or impossible. We have explored some schemes of construction of bounding chains as lumpability and class C matrices. We have also developed other methods of construction of bounding chains for censored Markov chains. Clearly, bounding measures can not always lead to a conclusion. In this case, the bounding model must be refined if it is possible. We have showed that bounding techniques that we propose are appropriate for the verification of Markov chains and they may reduce drastically the verification time.
More details here …
kamel.barkaoui (at) nullcnam.fr