Accueil > Verimag > Séminaires
Détails sur le séminaire
Abstract: * 14:00-14:40 Rim El-Ballouli (Team RSD): Modeling and Analysis of Systems with Dynamic Architectures
In general, architecture is essential for mastering the complexity of computer systems and to facilitate their analysis and evolution. Architecture allows the separation between detailed behavior of components and their overall coordination. Although many formalisms were already proposed to describe and reason about dynamic architectures, they are facing serious challenges:
- achieving modeling expressively while based on rigorous semantics; lack of scalable analysis methods we propose a first step towards the modeling of systems with dynamic architectures with dynamic bip. We developed the Dy-BIP formalism into a full-fledged modeling language, including all useful modeling concepts and providing rigorous operational semantics in the dynamic case.
* 14:40-15:20 XU Xiao (Team PACSS): Extended Logics and Automates for the Verification of Container Libraries
Globally the goal of this thesis is to develop some logical tools for the program verification with containers. The first year, I did a lot of researches on different types of automata and some related algorithms, as well as testing different tools. This year, am going to study about the alternating data automata in order to find a better way to solve the problems in the domain, such as the language inclusion checking between alternating data automata.
* 15:20-15:40 Break.
* 15:40-16:20 Benjamin Farinier (Team PACSS): From bugs to exploitability: model generation for quantified formulas
Formal methods demonstrated their effectiveness for bug finding and analysis. If the current techniques are well suited for analyzing critical codes, where a bug is not an option, their interest is less obvious on non-critical applications. Indeed, such programs usually contain numerous bugs and only the most critical ones have to be corrected; this distinction being out of the scope of current tools. The objective of this thesis is therefore to consider such a bug gradation in the context of formal methods.
* 16:20-17:00 [Visioconference] Moustapha Lo (Team SYNCHRONE): Implementing an Health Monitoring System on a many-core platform.
The HMS function monitors vibrations of helicopters components.It was introduced in the helicopter industry for two main reasons: maintenance and operational regulation. Currently, this function is not embedded in the helicopter: a system records the vibration during the flight, then the data are uploaded when the helicopter is on ground, and analyzed off-line.
In this talk, I will cover many challenges we are facing to build a real-time on-line implementation
of HMS function on a many-core processor(MPPA-256). I propose a static-mapping (piece of our application) on Kalray MPPA-256 and some time-measurement.
