Seminars

  • CosmOpen: Dynamic reverse engineering on a budget

    François Taïani

    Lancaster University

    Abstract: 

    Dynamic reverse engineering uses data captured from a system at runtime to help developers reconstruct high-level models of a system's behaviour. Although it is an active area of research, the approaches proposed so far do not scale well to the complex and layered architectures typically encountered in distributed systems. In this talk, I will present CosmOpen, a reverse engineering tool specifically designed for the dynamic analysis of complex layered software.

    CosmOpen combines cheap and non-intrusive observation techniques with a versatile graph manipulation engine. By programming different graph manipulation scripts, the 'focal length'of CosmOpen can be adapted to different abstraction levels. The talks motivates this approach, presents its salient features, and finally illustrates how it can be used in a concrete case study to extract high-level behavioural models from a complex multi-threaded platform (GNU/Linux, CORBA middleware).

    Where: 
    6.3.5
    When: 
    Monday, May 17 2010
    Time: 
    11:00
  • Parameterised Multiparty Session Types

    Pierre-Malo Deniélou

    Imperial College London

    Abstract: 

    For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Godel's System T to express a wide range of communication patterns while keeping type checking decidable. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.

    Where: 
    6.3.5
    When: 
    Wednesday, May 12 2010
    Time: 
    11:00
  • A Theory of Design-by-Contract for Distributed Multiparty Interactions

    Kohei Honda

    Queen Mary University of London

    Abstract: 

    The approach known as Design by Contract (DbC) promotes reliable software development through elaboration of type signatures for sequential programs with logical formulae. In this talk I will present our recent work on an assertion method which generalises DbC baesd on multiparty session types. Centring on the notion of global assertions and their projections onto endpoints,the framework allows expressive specifications and validation while allowing effective static and dynamic validation. We illustrate the key results on this assertion method, including relative completeness of its proof system. and discuss its theoretical and practical contexts. [Joint work with Laura Bocchi, Emilio Tuosto, and Nobuko Yoshida]

    Where: 
    6.3.5
    When: 
    Tuesday, May 11 2010
    Time: 
    11:00
  • Interactive Experimentation of Objects

    André L. Santos

    ISCTE

    Abstract: 

    Learning and teaching object-oriented programming is generally perceived as being difficult. While teachers are faced with the challenge of efficiently transmitting a set of closely interrelated concepts that cannot be easily taught in isolation, apprentices struggle to grasp those concepts and develop mental models of how object-oriented programs work. In this talk I will present the idea of interactive experimentation of object-oriented programs by means of an adaptive generic user interface application (AGUIA). The approach is based on having a tool that ``gives life" to a set of user-developed classes, providing instant visual feedback through an environment where objects of such classes can be created, and the evolution of their state can be observed as operations are invoked on them. The fundamental object-oriented concepts are metaphorically represented in the user interface elements of the application, in order to help apprentices to develop their understanding and rationale about the several language features. The talk goes along with a demonstration of the work-in-progress in AGUIA/J, an implementation of the proposed tool for the Java language.

    Where: 
    6.3.5
    When: 
    Monday, May 3 2010
    Time: 
    11:00
  • Resource Usage Analysis for the Pi-Calculus

    Kohei Suenaga

    IBM Japan

    Abstract: 

    Learning and teaching object-oriented programming is generally perceived as being difficult. While teachers are faced with the challenge of efficiently transmitting a set of closely interrelated concepts that cannot be easily taught in isolation, apprentices struggle to grasp those concepts and develop mental models of how object-oriented programs work. In this talk I will present the idea of interactive experimentation of object-oriented programs by means of an adaptive generic user interface application (AGUIA). The approach is based on having a tool that ``gives life" to a set of user-developed classes, providing instant visual feedback through an environment where objects of such classes can be created, and the evolution of their state can be observed as operations are invoked on them. The fundamental object-oriented concepts are metaphorically represented in the user interface elements of the application, in order to help apprentices to develop their understanding and rationale about the several language features. The talk goes along with a demonstration of the work-in-progress in AGUIA/J, an implementation of the proposed tool for the Java language.

    Where: 
    6.3.5
    When: 
    Wednesday, January 27 2010
    Time: 
    11:00
  • Demo: Work in Progress in the ConGu Plug-in for Eclipse

    João Martins e Ricardo Mendes

    FCUL.

    Abstract: 

    In this talk we will present the work in progress in the new ConGu plug-in for Eclipse. This new version of the plugin, based on a new version of ConGu, will provide support for the runtime conformance checking of Java programs comprising generic types against abstract data type specifications.

    Where: 
    6.3.5
    When: 
    Wednesday, November 18 2009
    Time: 
    11:00
  • From Local Impact to Global Adaptation of Service Compositions

    Liliana Rosa

    FCUL

    Abstract: 

    The problem of self-optimization and adaptation in the context of customizable systems is becoming increasingly important with the emergence of complex software systems and unpredictable execution environments. Here, a general framework for automatically deciding on when and how to adapt a system whenever it deviates from the desired behavior is presented. In this framework, the adaptation targets of the system are described in terms of a high-level policy that establishes goals for a set of performance indicators. The decision process is based on information provided independently for each service that describes the available adaptations, their impact on performance indicators, and any limitations or requirements. The technique consists of both online and online phases. Offine, rules are generated specifying service adaptations that may help to achieve the specied goals when a given changein the execution context occurs. Online, the corresponding rule is evaluated when a change occurs to choose which adaptations to perform. Experimental results using a prototype framework in the context of a web-based application demonstrate the eectiveness of this approach.

    Where: 
    6.3.5
    When: 
    Wednesday, October 21 2009
    Time: 
    11:00
  • Declaratively and effectively extract, transform, and clean your data

    Helena Galhardas

    IST

    Abstract: 

    Extraction, Transformation, and Loading (ETL) of data stored in different sources into a unique repository is a crucial activity in the context of a data warehousing architecture. A large amount of effort is usually spent for designing a workflow of data operations that is able to produce data items that adequately fit the target data schema. Moreover, special care must be taken so that this workflow is executed within a temporal window that does not affect the performance of the source operational systems.

    An ETL process is also required in other contexts, such as migrating data from an obsolete database into a new database schema, or converting poorly structured data (e.g., Web sites or texts) into structured data. Depending on the nature of the source data and the needs of the target application, the Transformation phase of the process may also include Data Cleaning operations. Data Cleaning aims at removing inconsistencies, correcting erroneous data, and detecting/merging duplicate information.

    Several technological solutions for Extract-Transform-Clean-Load data are available in the market. We identified two important requirements they lack to fulfill. First, the semantics of the operators is not independent of their implementation algorithms. Second, they do not support interactive facilities to tune a program.

    In this talk, I will focus on Extracting, Transforming and Cleaning (ETC) data. I will not address the Loading phase. First, I will give a short overview of the AJAX data cleaning and transformation framework that was the first attempt to overcome the two disadvantages of data cleaning commercial tools mentioned above. Second, I will describe the work we are developing in terms of the extraction phase of the process. Assuming that we have source data in HTML/XML format or even text, we propose to decompose the process of extracting relevant information in several steps. A distinct declarative operator is associated to each step. Third, I will present a proposal for refining and correcting the ETC workflow of operations in such a way that the user interaction is minimized.

    Where: 
    6.3.5
    When: 
    Wednesday, October 14 2009
    Time: 
    11:00
  • Session-Based Communication Optimisation for Higher-Order Mobile Processes

    Dimitris Mostrous

    Imperial College London

    Abstract: 

    In this work we extend our previous work on Session typing for the Higher-order Pi-Calculus, by introducing Asynchronous Subtyping. Session types describe structured communications where the type of messages, and also the order of heterogeneous typed messages, is specified and checked against processes. Asynchronous subtyping allows the order of messages to be changed while still preserving type safety and composability with existing processes that may be using unoptimised types/ Our system enables two complementary methods for communication code optimisation, mobile code (Higher-order processes) and asynchronous permutation of session actions (via Asynchronous subtyping). In order to prove transitivity of our coinductive subtyping relation, we uniformly deal with type-manifested asynchrony, linear functional types, and contravariant components in higher-order communications. For the runtime system we propose a new compact formulation that takes into account stored higher-order values with open sessions, as well as asynchronous commutativity. In spite of the enriched type structures, we construct an algorithmic subtyping system, which is sound and complete with respect to the coinductive subtyping relation. We demonstrate the expressiveness of our typing system with an e-commerce example, where optimised processes can interact respecting the expected sessions.

    Where: 
    6.3.5
    When: 
    Wednesday, September 30 2009
    Time: 
    11:00
  • Typechecking Promela: a Case Study in Applied Type Theory

    Simon Gay

    University of Glasgow

    Abstract: 

    The Spin model checker and its specification language Promela have been used extensively in industry and academia to check logical properties of distributed algorithms and protocols. Model checking with Spin involves reasoning about a system via an abstract Promela specification, thus the technique depends critically on the soundness of this specification. Promela includes a rich set of data types including first-class channels, but the language syntax restricts the declaration of channel types so that it is not generally possible to deduce the complete type of a channel directly from its declaration. We present a case study in applying well-understood techniques from type theory, including constraint-based type inference and recursive types, to build an enhanced typechecker for Promela. We discuss theoretical and practical problems associated with designing a type system and typechecker for an existing language, and formalise our approach using a Promela-like calculus. To enforce the limited form of subtyping which Promela allows, we present a novel unification algorithm to solve a system of equality and subtyping constraints. We use practical Promela examples to illustrate the kind of errors that our enhanced typechecker can detect. [Joint work with Alastair Donaldson.

    Where: 
    6.3.5
    When: 
    Wednesday, May 20 2009
    Time: 
    11:00

Pages

Subscribe to Seminars