Foundations and Applications of Software Technology



  • MOMPES 2008 - Model-based Methodologies for Pervasive and Embedded Software
  • Interacção 2008 - 3ª Conferência Interacção Pessoa-Máquina
  • XATA 2008 - 6th national conference of XML: Applications and Technologies. Évora, 14,15 February 2008



  • New Project: FAST members participate in EFACEC's InPACT project
  • Co-chair: J. C. Campos was designated co-chair of the programme committee of INTERACÇÃO'08.
  • New Paper: Simulation and Formal Verification of Industrial Systems Controllers
  • New Paper: Formal analysis of interactive systems: opportunities and weaknesses
  • New Paper: Connecting rigorous system analysis to experience centred design


DI » FAST » WebHome » FastSeminar

FAST Seminar Series

Wednesdays at 14:00 in the DI meeting room

The FAST Seminar Series is a bi-weekly scientific colloquium organized by the Foundations and Applications of Software Technology group.

Moderator: José Creissac Campos.

Attendance is open to all.

If you would like to contribute a talk, please contact the moderator.

Upcoming talks

None for the time being.

Past talks

Modelling human aspects of a simple ubiquitous system using UPPAAL and PROMELA
Michael Harrison (Newcastle University)
Thur, 2 Jul, 2009 at 11:00
The talk is very much work in progress. During the last few months I have been exploring models of a simple ubiquitous system to explore plausible operator behaviours. The first model, developed in UPPAAL, includes simple timing constraints driven by the process that a mobile device is intended to control. The second PROMELA model describes the same system but also makes explicit the information resources that would be used by the operator to control the plant. The talk will mainly focus on the PROMELA model. However I aim to discuss why the UPPAAL model was easier to construct and (at a simple level) to analyse, and to raise preliminary questions about time aspects of the model.

A Hoare-logic for programs that may or may not terminate
Keiko Nakata (Institute of Cybernetics, Tallinn University of Technology)
Wed, 17 Jun, 2009 at 11:30
In our previous work we have studied several coinductive operational semantics, all of which are proved equivalent, for the While language to describe terminating as well as non-terminating program executions. The operational semantics keep track of all the intermediate states that an execution goes through as a trace (a sequence of states). The trace is finite for a terminating execution and infinite for a non-terminating execution.
In this talk I present a Hoare-logic for While, which is proved sound and complete with respect to those operational semantics. As usual, our Hoare-triple consists of a precondition, a statement and a postcondition. The precondition is a predicate on initial states, whereas the postcondition is a predicate on traces. Since a trace contains the full information about an execution, the logic can talk about for instance if an execution is terminating or if an variable is updated infinitely often. My talk will start by introducing a coinductive big-step relational semantics, then present the Hoare-logic. I will explain some interesting design issues on the logic and our strategy for proving its completeness, that we have discovered through many failed attempts. All the results have been formalized in Coq.

Integração de Sistemas de Informação
Nuno F. Rodrigues (FAST)
Mon, 23 Mar, 2009 at 10:30
O objectivo da integração de sistemas de informação consiste na união de serviços e informações de diversos sub-sistemas independentes, por forma a obter uma solução única, coerente e integrada. Por outro lado, os modelos e linguagens de coordenação têm como principal objectivo especificar e raciocinar sobre configurações de cooperação entre entidades computacionais distintas e independentes. Apesar das diferenças fundamentais na forma com atacam os seus problemas específicos, a aplicação dos modelos e linguagens de coordenação à integração de sistemas de informação parece um exercício imediato e com enormes vantagens para o sucesso de projectos de integração de software. No entanto, esta relação encontra-se extremamente mal explorada, com a excepção de casos pontuais do uso de modelos de orquestração e coreografia. Nesta apresentação apresentar-se-á um conjunto de estilos de integração de sistemas de informação, tendo como preocupação explorar novas aplicações dos modelos de coordenação a cada estilo de integração introduzido. Para além de apresentar os estilos de integração de forma clara e independente de tecnologias específicas, é ainda apresentada uma organização comparativa dos estilos de integração.

Matrices As Arrows
Hugo Macedo (FAST)
Wed, 18 Feb, 2009 at 16:00
The advent of On-Chip parallelism poses a dreadful obstacle to current mature programming languages. Traditional approaches based on compiler or hand-coded optimizations are giving place to trendy generative techniques, based on DSL and ad-hoc program transformation frameworks. In this talk we will report on our first steps in the attempt to lay the common (categorical) semantics of a particular class of DSL addressing numerical programming under the motto "matrices as arrows!" We will shift the traditional view of matrices as indexed structures to an index-free representation, analogous to point-free program transformation.

Software Espacial nos Projetos de Veículos Lançadores Brasileiros
Miriam Alves (Instituto de Aeronáutica - IAE, Brasil)
Wed, 04 Feb, 2009 at 14:00
Esta apresentação abordará, de forma sucinta, as principais atividades do Instituto de Aeronáutica e Espaço (IAE - Brasil)- relacionadas aos Projetos de Veículos Lançadores de Satélites, com ênfase no desenvolvimento, validação e verificação tanto do software embarcado nestes veículos como nos sistemas de software de apoio de solo para a realização das missões de lançamento. Considerando a importância e o aspecto crítico destes sistemas de software, serão apresentadas as iniciativas mais recentes do grupo de software do IAE para a melhoria do processo de desenvolvimento e da abordagem de verificação e validação.

Automatic Generation of Visual Programming Environments
Nuno Oliveira (FAST)
Wed, 07 Jan, 2009 at 13:30
In this talk we will discuss the generation of visual programming environments in an automatic way, from the formal specification of the underlying language. An automatic visual environment generator, named DEViL? , is the base of the discussion. DEViL? generates visual programming environments with integration of graphical editors, compilers, translators and several others tools, from attribute grammars for visual-languages. A running example, VisualLISA? , is used to present the workflow to generate a visual programming environment. VisualLISA? is a visual editor for Attribute Grammar (AG) specifications. This editor is generated from a specification of a visual-language that enables us to draw, syntactically and semantically correct, attribute grammars. The visual specification of an AG is production-oriented and incremental. The editor translates the drawn attribute grammar directly into LISA notation or alternatively into a universal XML representation designed to support different AG-based compiler generators.

The IVY workbench
José Creissac Campos (FAST)
Wed, 03 Dec, 2008 at 14:00
In this talk I describe the IVY workbench, a tool for the modelling and model-checking based analysis of interactive systems.

GUISurfer - A Generic Framework for GUI Reasoning and Testing
João Carlos Silva (FAST)
Wed, 29 Oct, 2008 at 14:00
This talk discusses the development of the GUISurfer tool. GUISurfer is focused on extracting and testing behavioural models from Graphical User Interface (GUI) source code. We present a generic model for language independent reverse engineering of GUI-based applications, and we explore the integration of model-based testing techniques in our approach, thus allowing us to perform fault detection. First we describe our library for GUI models extraction and manipulation. And finally we show how these models can be use to reason about the user interface and generate test cases for automatic GUI testing.

Methods and techniques to analyze multi-level code to explore software components
Daniela da Cruz (FAST)
Wed, 22 Oct, 2008 at 14:00 (Anfiteatro A2 / DI)
This Ph.D. work, in the general context of Software Engineering, is concerned with software systems' maintenance (systems that may contain millions of lines of code). Namely, the work will be oriented to applications (may be web applications) developed under multi-language Integrated Development Environments (IDEs), where many languages and technologies can be smoothly combined due to the existence of a common language runtime.
Maintenance requires the comprehension of the overall system, as well as, the full understanding of each component (a program). Many times, the first task performed to do maintenance is the backward analysis of the system (from code to model), known as the reverse engineering process.
Program Comprehension, Program Understanding, and Reverse Engineering activities depend on the so-called program analysis, among other technologies; many times it is important to constrict the program analysis to a program slice to focus only on those statements that are responsible for some state.
Maintenance, code re-use, and systems' re-engineering require, as told above, quantifiable methods. That approach implies the definition and use of software metrics. But the complexity of data resulting from program analysis, or even from the metrics evaluation process, demands the resort to high-quality graphical interfaces to help the user to understand and navigate over the imbricated data. So, software visualization is another discipline involved in a systematic, disciplined, quantifiable approach to software maintenance. This contextualization let us understand that the background for the present work requires the study of: code analysis, slicing, metrics, and visualization. Because program verification is nowadays a relevant issue in this area of software engineering, it was decided to include another topic: proof carrying code (PCC).
A lot of work has been done in the past in code analysis to help in the various tasks of software re-engineering and maintenance, including program comprehension activities. Many good results have been reached. However in the multi-language multi-technology platform that will be considered, there is still need for a system that can handle programs at different levels of encoding. The aim of this Ph.D. work is to investigate efficient methods, techniques and tools to analyze source (high-level), intermediate (abstract middle-level) or target (low-level/machine) code, under the same environment, in order to extract static and dynamic information that can be visualized in a uniform way (independent of the analysis level) to help in program maintenance---the analysis, comprehension, and verification of a program.
The focus of this talk will be the general overview of the Ph.D. project, and a synthesis of the state-of-the-art concerning Program Analysis and Program Slicing.

From Spreadsheets to Relational Databases and Back
Jácome Cunha (FAST)
Wed, 08 Oct, 2008 at 14:00
This paper presents techniques and tools to transform spreadsheets into relational databases and back. A set of data refinement rules is introduced to map a tabular datatype into a relational database schema. Having expressed the transformation of the two data models as data refinements, we obtain for free the functions that migrate the data. We use well-known relational database techniques to optimize and query the data. Because data refinements define bidirectional transformations we can map such database back to an optimized spreadsheet. We have implemented the data refinement rules and we constructed Haskell-based tools to manipulate, optimize and refactor Excel-like spreadsheets.

Modelling and simulating virtual environments
José Luís Silva (FAST)
Wed, 03 Sep, 2008 at 14:00
Context-aware applications pose new usability challenges that cut across the phases of design and development. They provide richer interaction taking context into account. They are difficult to build due to their distributed nature. This talk presents a technical literature review about modelling and simulating virtual environments, with a focus in context-aware applications. Relevant work in this area is discussed and compared through a case study. A first attempt to introducing context into some of the existing modelling approaches is described. Areas that require more work, and that we will possibly follow, are referenced.

Resources for Situated Actions
Gavin Doherty (Trinity College Dublin)
Tue, 13 May, 2008 at 14:00
In recent years, advances in software tools have made it easier to analyze interactive system specifications, and allow the analyst to consider a wide range of possible behaviors. However, the effort involved in producing the specifications of the system is still substantial, and a difficulty exists regarding the specification of plausible behaviors on the part of the user. Recent trends in technology towards more mobile and distributed systems further exacerbates the issue, as contextual factors come in to play, and less structured, more opportunistic behavior on the part of the user makes purely task-based analysis difficult. In this paper we consider a resourced action approach to specification and analysis. In pursuing this approach we have two aims - firstly, to facilitate a resource-based analysis of user activity, allowing resources to be distributed across a number of artifacts, and secondly to consider within the analysis a wider range of plausible and opportunistic user behaviors without a heavy specification overhead, or requiring commitment to detailed user models.

Synthesis of Reo Circuits from Scenario-based Specifications
Sun Meng (CWI, Amsterdam)
Wed, 30 Apr, 2008 at 14:00
It is difficult to construct correct models for distributed large-scale service-oriented applications. Typically, the behavior of such applications emerge from interaction and collaboration of multiple components/services. On the other hand, each component, in general, takes part in multiple scenarios. Consequently, not only components, but also their interaction protocols are important in the development process for distributed systems. Coordination models and languages, like Reo, offer powerful ``glue-code'' that encode the interaction protocols. In this work we propose a novel synthesis technique, which can be used to generate Reo circuits directly from scenario specifications. Inspired by the way UML2.0 sequence diagrams can be algebraically composed, we define an algebraic framework for merging connectors generated from partial specifications by exploiting the algebraic structure of UML sequence diagrams.

An Introduction to Hoare Logic and Program Verification Conditions
Jorge Sousa Pinto
Wed, 20 Feb, 2008 at 14:00
Floyd-Hoare Logic stands at the heart of the science of Computer Programming, and has been used extensively in both formal software development and program verification. In this talk we review different methods for generating verification conditions for a given specification, and show how they are derived from Hoare's standard inference system. We discuss methods based on program annotations, weakest preconditions, and updates, and present examples of program verification systems based on each of these.

Contraint-aware schema transformation
Tiago Alves
Wed, 23 Jan, 2008 at 16:00 (new time)
Schema transformations occur in several contexts. Examples are software evolution, refactoring and cross-paradigm mapping (e.g. VDM to SQL transformation). When initial schemas are annotated with contraints, these contraints must be preserved in the target schema. Moreover, during the transformation process, when high-level data structures are refined, new constraints can be added for semantic preservation (e.g. referential integrity). We intend to present a possible solution, using an algebraic approach that is constraint-aware, in the sense that existent contraints are preserved and new contraints are added when necessary. This solution is based on refinement theory and point-free program transformation.

Template Metaprogramming - From University to Industry
Zoltán Porkolab (Eötvös Loránd University, Budapest)
Wed, 09 Jan, 2008 at 14:00
The C++ and Java programming languages are considered as object-oriented languages. However, both have strong features for generative programming: the C++ templates and the Java generics. Those generative programming facilities make it possible to write abstract data structures and generic algorithms. Moreover C++ templates form a Turing-complete sublanguage of C++, so one can write programs "running" in the compilation time. Template metaprogramming is an emerging new direction in C++ programming for executing algorithms in compilation time. This one time theoretical possibility today became a strong industrial tool widely used in various libraries and applications. In this talk we review the possible fields of application of C++ template metaprogramming, and emphasize its unique advantages.

Apresentação do Projecto FP7 CACE: Computer Aided Cryptography Engineering
Manuel Bernardo Barbosa
Wed, 05 Dec, 2007 at 14:00

Model-based user interface testing
José Creissac Campos
Wed, 21 Nov, 2007 at 14:00
Analytic usability analysis methods have been proposed as an alternative to user testing in early phases of development due to the cost of the latter approach. By working with models of the systems, analytic models are not capable of identifying implementation related problems that might have an impact on usability. Model-based testing enables the testing of an implemented software artefact against a model of what it should be (the oracle). In the case of model-based user interface testing, a main issue is the use of oracles at an adequate level of abstraction. This talk discusses the findings of an effort to use task models as oracles for model-based testing of user interfaces.
Slides (PDF)

Previous seminar series

See the past talks of TFM Seminar.

See the past talks of PURé Café.

-- JoseCampos - 16 Feb 2009

r38 - 13 May 2010 - 23:54:40 - JoseNunoOliveira
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
Syndicate this site RSSATOM