Liste des événements uniques du groupe GT Génie Logiciel


2012-11-14Eval Begone! Semi-Automated Removal of Eval from JavaScript Programs
10:30-11:30
salle 71
Eval endows JavaScript developers with great power. It allows developers and end-users, by turning text into executable code, to seamlessly extend and customize the behavior of deployed applications as they are running. With great power comes great responsibility, though not in our experience. In previous work we demonstrated through a large corpus study that programmers wield that power in rather irresponsible and arbitrary ways. We showed that most calls to eval fall into a small number of very predictable patterns. We argued that those patterns could easily be recognized by an automated algorithm and that they could almost always be replaced with safer JavaScript idioms. In this paper we set out to validate our claim by designing and implementing a tool, which we call Evalorizer, that can assist programmers in getting rid of their unneeded evals. We use the tool to remove eval from a real-world website and validated our approach over logs taken from the top 100 websites with a success rate over 97% under an open world assumption.
 Plus d'infos  


2012-10-08Pré-présentation à la conférence WCRE par Cédric Teyton
14:00-15:00
Salle 73
Mining Library Migration Graphs

Abstract—Software systems intensively depend on external libraries, chosen at conception time. However, relevance of any library irremediably changes during projects and/or library life cycle. As a consequence, projects developers must periodically reconsider the libraries they depend on, and must think about library migration. When they want to migrate their libraries, they then have to identify candidate libraries that offer similar facilities and thus can substitute to each other. They also have to compare candidates to choose the one that best fits their needs. Finding a relevant library replacement is a well known tedious and time-consuming task. In this paper, we propose an approach that identifies sets of similar libraries and that produces what we call library migration graphs that show how existing projects have performed migrations among them. These graphs, constructed from the observation of a large number of software projects, ease the discovery and selection of library replacements.
 Plus d'infos  


2012-09-19Geographical Treemaps: Cartographic Metaphors for Laying out Hierarchical Data
10:00-11:00
salle 73
The emergence of huge taxonomies due to the increase in available data raises numerous problems of visualization and navigation through the corresponding hierarchies. On datasets of such scale, classical graph drawing methods do not take advantage of some human cognitive skills such as shape recognition, which easily remember the global structure of the data. In this paper, we propose a method based on a geographic map metaphor. By employing human perception mechanisms developed by handling geographic maps, this technique facilitates the visualization and navigation through a hierarchy. The algorithm has been designed to preserve regions containment according to the arborescent hierarchy and to set the leaves’ sizes proportionally to a property, in such way the size of non-leaf regions correspond to the sum of the sizes of their children. Moreover, the input ordering of the hierarchy’s nodes is preserved, i.e. the areas representing two consecutive children of a node in the hierarchy are adjacent. This property is particularly useful as it guarantees some stability to our algorithm. We illustrate our technique by providing example visualizations of the repartition of the tax money in the U.S. over time. Furthermore, we validated the use of the geographical metaphor in a professional documentation context. We show the stability and the ease of memorisation of this type of map.
 Plus d'infos  


2012-07-06Etude de l'activité des développeurs impliqués dans Gnome
10:00-11:00
salle 178
Dans le cadre de notre étude des communautés associées aux
écosystèmes open source, nous avons analysé la manière dont les
développeurs faisant partie de la communauté de GNOME structurent leur
travail. Plus précisément, nous nous sommes attachés à l'étude des
différents types d'activités menées par ces personnes et à celle de la
manière dont leur comportement évolue au cours du temps.
 Plus d'infos  


2012-05-15introduction au "multi-stage programming"
16:00-17:00
Salle Ada Lovelace, Bât. A29
introduction au multi-stage programming proposé par Walid Taha
 Plus d'infos  


2012-05-15[GTGL] The Quest for Future Proof Interoperability
10:00-11:00
salle 178
Abstract:
Over the history of distributed systems, a number of interoperability
solutions have emerged both in terms of proposed standards for
interoperability and solutions to bridging between standards.
Distributed systems have, however continued to evolve and we
particularly note two important trends: the dramatically increasing
level of heterogeneity coupled by the increasing dynamism in
contemporary distributed systems. The end result is that it is very
difficult to achieve interoperability in any systematic way. Indeed, we
can say that distributed systems are in crisis with no principled
solutions to interoperability for such complex and dynamic distributed
systems structures. This talk discusses the problems of achieving
interoperability in the complex distributed systems of today, and
highlights the role of emergent middleware as a possible solution to
this problem. Emergent middleware is an interoperability solution
whereby the required connectivity is generated at run-time to match the
current context and requirements. A models@runtime approach is put
forward as a solution towards achieving the run time generation of
middleware; and in particular the Starlink software framework is
investigated. Finally, the talk also considers the potential role of
ontologies in supporting meaning and reasoning in the connection of
networked services.

Bio:
Paul Grace is a senior research associate in the School of Computing and
Communications at Lancaster University; he has previously spent time
working as a research scientist at Katholieke Universiteit Leuven. At
Lancaster, he’s currently working on the Connect project investigating
dynamic interoperability solutions in complex distributed systems. His
research interests are in distributed systems architecture and
middleware, adaptive software solutions, and the application of
model-driven engineering in systems software. He received his PhD from
Lancaster in 2004, an MSc from the same institution in 2000 and a BSc
from the University of York in 1999.
 Plus d'infos  


2012-05-02A formally verified SSA-based middle-end - Static Single Assignment meets CompCert.
13:00-14:00
Salle Ada Lovelace, Bât. A29
CompCert is a formally verified compiler that generates compact and efficient PowerPC, ARM and x86 code for a large and realistic subset of the C language. However, CompCert foregoes using Static Single Assignment (SSA), an intermediate representation that allows for writing simpler and faster optimizers, and is used by many compilers. In fact, it has remained an open problem to verify formally a SSA-based middle-end compiler.
We report on a formally verified, SSA-based, middle-end for CompCert. Our middle-end performs conversion from CompCert intermediate form to SSA form, optimization of SSA programs, including Global Value Numbering, and transforming out of SSA to intermediate form. In addition to provide the first formally verified SSA-based middle-end, our work addresses two problems raised by Leroy: giving a simple and intuitive formal semantics to SSA, and showing how to leverage the global properties given by SSA to reason locally about program optimizations.
 Plus d'infos  


2012-04-13[GTGL] Nicolas Loriant
16:00-17:00
salle 76
Présentation en vue d'une candidature MCF au LaBRI
 Plus d'infos  


2012-04-12Intégration des activités de vérification formelle aux processus de développement de logiciels pour les systèmes embarqués
09:30-10:30
salle 178
En dépit de l’efficacité des méthodes formelles, en particulier les techniques d’analyse de modèles (model checking), à identifier les violations des exigences dans les modèles de conception, leur utilisation au sein des processus de développement industriel demeure limitée. Ceci est dû principalement à la complexité des modèles manipulés au cours de ces processus (explosion combinatoire) et à la difficulté de produire des représentations formelles afin d’exploiter les outils de vérification existants.
Fort de ce constat, mes travaux de thèse contribuent au développement d’un volet méthodologique définissant les activités conduisant à l’obtention des artefacts formels. Ceux-ci sont générés directement à partir des exigences et des modèles de conception manipulés par les ingénieurs dans leurs activités de modélisation. Nos propositions s’appuient sur les travaux d’exploitation des contextes pour réduire la complexité de la vérification formelle, en particulier le langage CDL. Pour cela, nous avons proposé une extension des cas d’utilisation, afin de permettre la description des scénarios d’interaction entre le système et son environnement directement dans le corps des cas d’utilisation. Aussi, nous avons proposé un langage de spécification des exigences basé sur le langage naturel contrôlé pour la formalisation des exigences. Cette formalisation est opérée par transformations de modèle générant des propriétés CDL formalisées directement des exigences textuelles des cahiers des charges ainsi que les contextes CDL à partir des cas d’utilisations étendus. L’approche proposée a été instanciée sur un cas d’étude industriel de taille et de complexité réelles développé par notre partenaire industriel.
 Plus d'infos  


2012-04-05école Coq GT-GL
15:30-17:00
salle 178
4 sessions for learning Coq (3/4):
Modelling and verifying algorithms in Coq: an introduction

The Coq system provides a functional programming language and a
reasoning framework based on higher order logic to perform proofs on
programs. The expressive power of the language is such that
advanced notions of mathematics (such as the graph theory in the four
color theorem) or programs of high complexity (such as a compiler for
a significant kernel of the C Programming language) can be described
formally. In this school, we address the basic programming techniques
and approaches to prove properties of the programs. The covered
notions involve structural recursive programming, list and integer
handling, proof by induction, in the key definition of data-types,
pattern matching constructs and case-based reasoning, and inductive
properties.
 Plus d'infos  


2012-03-30Évolution perpétuelle de systèmes logiciels : Les langages et les architectures au service du génie logiciel
10:00-11:00
salle 178
Les systèmes logiciels doivent évoluer pour prendre en compte de
nouveaux besoins des utilisateurs ou de nouveaux contextes de
déploiement et d'utilisation. Certaines de ces évolutions peuvent être
anticipées par les développeurs alors que d'autres peuvent nécessiter
des changements conséquents dans le code du système. Il en résulte 2
défis : (1) Permettre le développement de systèmes qui évoluent en
permanence et (2) Faciliter l'évolution non anticipée de systèmes
existants. Dans cet exposé, je présenterai principalement mes travaux
de thèse qui combinent langages dédiés et support de programmation
pour relever le premier défi. Dans une deuxième partie, je présenterai
comment j'envisage d'utiliser les langages dédiés et les
environnements de développement pour relever le second.
 Plus d'infos  


2012-03-28Maîtriser l'évolution des écosystèmes logiciels
17:00-18:00
salle 178
Je présenterai en 15 minutes mes travaux et mon projet de recherche, dans l'objectif d'améliorer mon discours avant les auditions de Maître de conférence.
 Plus d'infos  


2012-03-08école Coq GT-GL
16:00-17:30
salle 178
4 sessions for learning Coq (2/4):
Modelling and verifying algorithms in Coq: an introduction

The Coq system provides a functional programming language and a
reasoning framework based on higher order logic to perform proofs on
programs. The expressive power of the language is such that
advanced notions of mathematics (such as the graph theory in the four
color theorem) or programs of high complexity (such as a compiler for
a significant kernel of the C Programming language) can be described
formally. In this school, we address the basic programming techniques
and approaches to prove properties of the programs. The covered
notions involve structural recursive programming, list and integer
handling, proof by induction, in the key definition of data-types,
pattern matching constructs and case-based reasoning, and inductive
properties.
 Plus d'infos  


2012-03-05Reverse Engineering Variability Models
10:30-12:00
salle 71
Software-intensive systems are now declined in many
variants, offering to customers flexible solutions and a wide range of
configuration options. Variability, as "the ability of a software
system to be efficiently extended, changed, customized or configured
for use in a particular context", makes it possible to tailor software
to specific customers' needs without having to develop entirely new
applications.
When variability is properly managed, economies of scale can be
achieved by engineering several related products (i.e., software
family or software product line) as a whole.

However, with the added flexibility also comes additional complexity.
The number of variants might be huge -- exponential in the number of
configuration options.
Therefore support for the comprehension, maintenance, correctness and
evolution of variability-intensive systems is crucial. For this
purpose, high-level representations (i.e., variability models) are
commonly used to identify variation points and specify their legal
combinations. Unfortunately, the manual elaboration of a variability
model for an existing system is time-consuming, error-prone and
requires substantial effort from a modeler.
We rather want to reverse engineer the variability from software
artifacts in an automated way.
Reverse engineering has a long tradition (recovering architectures and
design patterns, identifying reusable assets, building traceability
between software artifacts, re-modularizing existing systems,
migrating toward new architectures and platforms, etc.) but the
extraction of variability is still in its infancy.

In this talk, I will first review existing works that have developed
reverse engineering procedures for the purpose of deriving variability
models. These works consider various kinds of artifacts (legacy system
documentation, textual requirements, pre-processor directives in C
code, configuration files, etc) and have been applied in various
domains (e.g., operation system domain for Linux, eCos, FreeBSD).
Then, I will report progress made with other colleagues in three
directions.
The first is related to the extraction and evolution of architectural
variability models in plugin-based systems, using FraSCAti as a case
study.
The second concerns the extraction of variability models from product
descriptions, typically organized in tabular data.
The third aims at reverse engineering variability models from user
interfaces (e.g., web configurators).
I will notably explain the role of FAMILIAR, a language dedicated to
the management of feature models (the defacto standard for modeling
variability).
 Plus d'infos  


2012-02-02Generation of Debugging Interfaces for Linux Kernel-level Services
10:00-12:00
salle 71
The Linux kernel does not export a stable, well-defined kernel interface,
complicating the development of kernel-level services, such as device
drivers and file systems. While there does exist a set of functions that
are exported to external modules, these are continually changing, and
have non-trivial implicit, ill-documented pre and post conditions, which, if not satisfied,
can cause the entire system to crash or hang. We have observed the prevalence of such
safety holes in a study of several recent releases of the Linux kernel.
However, no specific debugging support is provided.

We present Diagnosys, a new approach to automatically constructing a debugging
interface for the Linux kernel. Diagnosys relies on static analysis of kernel source
code to infer usage preconditions of functions exported to kernel-level services. Service
developers can then use the Diagnosys interface generator to produce a debugging interface that
is specialized to their code. This interface is then included within a service implementation such
that when the service is tested it records information about potential problems. Thanks to Diagnosys
crash resilient logging system, the recorded information is then made available on reboot to the service
developer on reboot after a kernel crash or hang.

We use our approach on 10 services from a range of kernel level services including file systems, network adapters,
USB device drivers, multi-media drivers, and show that the debugging interfaces provide useful information in case of faults,
while incurring only a slight performance overhead.
 Plus d'infos  


2012-01-31An Observational Study of a Scripting Language: R
14:00-15:30
salle 64
R is a dynamic language for statistical computing that combines lazy
functional features and object-oriented programming. This rather unlikely
linguistic cocktail would probably never have been prepared by computer
scientists, yet the language has become surprisingly popular. With millions
of lines of R code available in repositories, we have an opportunity to
evaluate the fundamental choices underlying the R language design. Using a
combination of static and dynamic program analysis we can assess the impact
and success of different language features.
 Plus d'infos  


2012-01-19[GTGL] Mixing logic and functional programming styles
10:00-12:00
salle 64
We have been designing a language in which programmers can mix
the logic and functional styles. In the functional style
programmers introduce variables and assign the variables
values be describing a computation that evaluates to the
answer desired.

In our language one can also introduce variables by describing
what properties their values should have using first order
logic. The language implementation automatically searches for
solutions.

The language lets the programmer mix computation based
programs with search based programs in a completely
transparent manner.

The kind of search is directed by the type of value being
sought, and the particular operands in the logic used to
describe its properties. we use general purpose tools like
SAT solvers, SMT solvers, the Simplex algorithm, and
Narrowing to actually perform the search.

Creation of the search tree, and the strategy of searching
the tree are separated, and the user can specify a different
strategy for each search, yet a single answer may involve
several searches, and all these are coordinated in a
transparent manner.
 Plus d'infos  


2011-11-23Stochastic Models for Quality of Service of Component Connectors
10:00-12:00
salle 178
The intensifying need for scalable software has motivated modular development and using systems distributed over networks to implement large-scale applications. In Service-oriented Computing, distributed services are composed to provide large-scale services with a specific functionality. In this way, reusability of existing services can be increased. However, due to the heterogeneity of distributed software systems, software composition is not easy and requires additional mechanisms to impose some form of a coordination on a distributed software system.

Besides functional correctness, a composed service must satisfy various quantitative requirements for its clients, which are generically called its quality of service (QoS). Particularly, it is tricky to obtain the overall QoS of a composed service even if the QoS information of its constituent distributed services is given.

For this, Stochastic Reo is proposed to specify software composition with QoS aspects and its compositional semantic models. These semantic models are also used as intermediate models to generate their corresponding stochastic models for practical analysis. Based on this, we have implemented the tool Reo2MC. Using Reo2MC, we have modeled and analyzed an industrial software, the ASK system. Its analysis results provided the best cost-effective resource utilization and some suggestions to improve the performance of the system.
 Plus d'infos  


2011-10-14Supporting change analysis and integration with Torch and Ring
10:00-12:00
salle 178
Software developers working on non-trivial systems frequently need to integrate contributions originating from various sources.
This task of integrating changes is nowadays performed mostly manual: developers need to study a submitted patch, assess its impact and dependencies on the system and integrate the actual source code.
Especially in the context of multiple, individually evolving branches, applying a patch - that was not necessary developed in the same branch - can be a daunting task.
In my work, I focus on the investigation and development of tools that support developers in understanding the nature and impact of changes.

In this talk we focus on two of the artifacts developed during my research.
First, we discuss Torch, which is an extension to the Pharo Smalltalk environment that offers developers - by means of visualizations - proper support for understanding the structure and scope of changes.
Second, we take a look at Ring, our ongoing work on the representation of source code and changes, both from the perspective of individual snapshots as well as the history of a software system.
 Plus d'infos  




Liste des événements répétitifs du groupe GT Génie Logiciel


Date Heure de début Heure de fin Titre Résumé Lieu Actif Public Fréquence Plus d'infos
2012-01-26  15:30:00  17:30:00  école Coq GT-GL  4 sessions for learning Coq (1/4):
Modelling and verifying algorithms in Coq: an introduction

The Coq system provides a functional programming language and a
reasoning framework based on higher order logic to perform proofs on
programs. The expressive power of the language is such that
advanced notions of mathematics (such as the graph theory in the four
color theorem) or programs of high complexity (such as a compiler for
a significant kernel of the C Programming language) can be described
formally. In this school, we address the basic programming techniques
and approaches to prove properties of the programs. The covered
notions involve structural recursive programming, list and integer
handling, proof by induction, in the key definition of data-types,
pattern matching constructs and case-based reasoning, and inductive
properties. 
salle 178  actif  public  2 semaines  Plus d'infos


Retour
Retour à l'index