Seminars

  • Model Based GUI Testing: research challenges

    Ana Paiva

    Faculdade de Engenharia da Universidade do Porto

    Abstract: 

    Graphical User Interface (GUI) testing is the process of testing a software application with a graphical front-end to guarantee that it meets its specification. Given the myriad of possible (human-computer) interactions in such a user interface, GUI software testing is a rather expensive and cumbersome phase of the whole software development cycle.
    Model based testing (MBT) can increase the systematization and automation of the testing process. Existing research work shows MBT may be also beneficial in the context of GUI testing. However there are some challenges that it is necessary to overcome.
    This talk will present some basic concepts about model based testing, some previous research work in this area, current research work and some trends for the future. In particular it will be described a novel approach, PBGT, that aims to increase the level of abstraction of the GUI models, promote reuse, diminish the effort in the modelling construction, generate test cases from models, assess testing coverage, and execute the generated test cases over a GUI.

    Where: 
    6.3.5
    When: 
    Thursday, December 6 2012
    Time: 
    13:00
  • Communication Safe Parallel Programming with Session C

    Nicholas Ng

    Imperial College London

    Abstract: 

    I'll present Session C, a session-based programming framework for message-passing based parallel programming. The framework consists of three parts: (1) a multiparty global protocol, written in a protocol description language with support for parameterised roles, (2) a runtime library for developers to implement parallel programs based on the given endpoint protocol, and (3) a type checker to ensure conformance between the implemented programs and the protocol. The static type checker allows permutations of asynchronous communication primitives as well as supporting a dynamic number of processes to spawn not known at compile time. Typable programs in the framework is guaranteed communication-safe and deadlock-free by the underlying multiparty session types theory. [Joint work with Kohei Honda and Nobuko Yoshida]

    Where: 
    6.3.5
    When: 
    Wednesday, December 5 2012
    Time: 
    13:30
  • Single-assignment forms as a basis for program verification

    Jorge Sousa Pinto

    U Minho

    Abstract: 

    A mechanism for generating verification conditions (VCs) for the iteration-free fragment of an imperative language is fundamental in any deductive program verification system. In this talk we revisit symbolic execution, weakest preconditions, and bounded model checking as VC-generation mechanisms, and propose a uniform presentation of the corresponding sets of VCs, in terms of (logical encodings of) paths in the control-flow graph of a single-assignment form of the program under analysis. This allows us to compare the mechanisms, in particular with respect to the size of the generated formulas. We finish the talk with some preliminary ideas towards a program logic for single-assignment programs.

    Where: 
    6.3.5
    When: 
    Wednesday, October 31 2012
    Time: 
    11:30
  • PESTT - An Educational Testing Tool

    Francisco Martins

    FCUL & LaSIGE

    Abstract: 

    Our society is built upon technology. TV sets, phones, cars, planes, etc. include dozens of processors that need software to make them behave as we expect. But what happens if the living room TV set software fails? Well, we may miss, say, the UEFA Euro cup final, which for some of us could be disappointing. What about a failure in the software that runs a train or a plane? There, the consequences could be far more catastrophic, potentially with huge social and financial impacts. Software ubiquity and criticality demands for a high quality of its delivery, in which testing plays a central role in detecting and reducing software failures.

    Know how to plan, design, and execute tests are skills that software engineers need to master. In this talk we present PESTT, a tool for assists in the testing activity, ranging from planning to test coverage analysis. Along the talk we go though several use case scenarios of the testing activity and show how the tool can help both the professional test engineer and the student learning how to accomplish the task. The tool is built on top of Eclipse and, as for its current version, supports unit testing based on the control flow graph of Java methods. The talk also addresses, although in less detail, the tool internals, specially the algorithms we devise and the external tools it depends on.

    Where: 
    6.3.5
    When: 
    Wednesday, July 4 2012
    Time: 
    13:30
  • Interaction-Driven Program Comprehension

    André L. Santos

    ISCTE-IUL

    Abstract: 

    In this talk we present a set of useful mechanisms for Program Comprehension that we characterize as Interaction-Driven. This designation comes from the fact that the mechanisms use the GUI of a running application as the means to communicate developer intent with respect to source code inspection, enabling developers to efficiently navigate through the source code by demonstrating program features. We propose program instrumentation (using AOP) and IDE interconnection as the means to implement the proposed mechanisms. The mechanisms will be demonstrated, and some results regarding empirical evaluations will be presented.

    Where: 
    6.3.5
    When: 
    Wednesday, June 6 2012
    Time: 
    13:30
  • Experiments in Parallel Methods for Combinatorial Optimization

    Salvador Abreu

    U. Evora and CENTRIA

    Abstract: 

    We give an overview of our work on Propagation-based Constraint solvers and methods for Constraint-based Local Search, formulated as an effective means of using parallel processors. We discuss the constraint programming paradigm, and how it maps to these two runtime approaches. We then describe several parallel designs and characterize them in terms of raw performance but also as to how they scale on multiprocessors. The range of parallel systems encompasses conventional homogeneous multicore processors, heterogeneous multicores such as Cell/BE and clusters of such systems. We provide experimental results on large scale parallel systems, and claim that these methods are both convenient for programming solutions to a significant class of problems and effective in using large-scale parallel hardware.

    This is joint work with D. Diaz, P. Codognet, V. Pedro and R. Machado.

    Where: 
    6.3.5
    When: 
    Wednesday, May 2 2012
    Time: 
    13:30
  • Runtime Programming

    Eduardo Marques

    FCUL

    Abstract: 

    We consider a methodology for flexible software design, runtime programming, defined by recurrent, incremental software modifications to a program at runtime, called runtime patches.

    The principles we consider for runtime programming are model preservation and scalability. Model preservation means that a runtime patch preserves the programming model in place for programs --- in terms of syntax, semantics, and correctness properties --- as opposed to an ``ad-hoc'', disruptive operation, or one that requires an extra level of abstraction. Scalability means that, for practicality and performance, the effort in program compilation required by a runtime patch should ideally scale in proportion to the change induced by it.

    We formulate runtime programming over an abstract model for component-based concurrent programs, defined by a modular relation between the syntax and semantics of programs, plus built-in notions of initialization and quiescence. The notion of a runtime patch is defined over these assumptions, as a model-preserving transition between two programs and respective states. Additionally, we propose an incremental compilation framework for scalability in patch compilation.

    The formulation is put in perspective through a case-study instantiation over a language for distributed hard real-time systems, the Hierarchical Timing Language (HTL).

    Where: 
    6.3.38
    When: 
    Wednesday, March 7 2012
    Time: 
    13:30
  • Proof Nets in Process Algebraic Form

    FCUL

    Abstract: 

    Process algebras suffer from the lack of logical foundations, in sharp contrast with λ-calculus which enjoys the Curry-Howard correspondence relating typed terms and Natural Deduction proofs. In this talk we present a Propositions-as-Types paradigm for concurrency: δ-calculus is a computational interpretation of Linear Logic, in the form of a typed process algebra whose structures correspond to Proof Nets -- the «Natural Deduction of Linear Logic» -- and where typing derivations correspond to linear sequent proofs. Term reduction shares the properties of cut elimination in the logic, and immediately we can obtain a number of inherited qualities, among which are termination, deadlock-freedom, and determinism.

    With respect to the notion of Programs-as-Proofs correspondence, we prove that for every Linear Sequent Proof there is a δ term typed with a (practically) identical sequent derivation, and the other direction, that for every well-typed term there exists a sequent proof. We will also show a sound and type-preserving translation to a linear λ-calculus, and finally a method that we conjecture to be sufficient in order to demonstrate that the language has the Church-Rosser (i.e., confluence) property.

    Where: 
    6.3.5
    When: 
    Wednesday, February 29 2012
    Time: 
    14:00
Subscribe to Seminars