HASLab Seminar Series
The HASLab Seminar Series is a scientific colloquium organized by HASLab. 
Attendance is open to all. 
Unless otherwise specified, talks take place at 13h45 in the Department's DI A.1 room (ground floor). 
If you are willing to contribute with a talk, please contact a group member (if you are a group member, fill in the schedule below). 
Please use the following addresses to access a google calendar with the talks schedule. 
Feed reader (XML) + Calendar supporting the ical format (ICAL) + Web browser (HTML) 
Upcoming talks
(In chronological order)
17th of July, 2013 
Models in software engineering 
Perdita Stevens 
A model is (for purposes of this talk) an abstract, usually graphical, representation of some aspect of a softwareintensive system. Software engineering has, since its invention, involved the use of models. In recent decades, a perceived need for greater automation of processes in software engineering, the wish to develop software faster and more cheaply, and the drive for higher quality have motivated ever more reliance on models. Languages for modelling and techniques for working with models have struggled to keep pace, hindered in some cases by conflicting requirements arising from the different motivations. We are currently in a dangerous state in which models sometimes endanger rather than support the developers' aims. I will explain some of the problems, and discuss the progress that I think we will/may/should/must/cannot expect to see in the coming years. 
Keywords: tba 
Slides: tba 
Lightning Talk 1 (5 min.): tba 
Lightning Talk 2 (5 min.): tba 
Past Talks
(In reverse chronological order)
19th of June, 2013 
Towards fully trustworthy and cross domain safety engineering 
Eric Verhulst (CEO/CTO Altreonic) 
Safety engineering standards are amongst the best practice examples on how systems engineering should be done. Nevertheless, these standards are very heuristic, complex to apply and different from domain to domain. The top level requirement for safety critical systems is the SIL, or Safety Integrity Level, but the way it is defined and quantified differs also from domain to domain and is hence the reason why crossdomain reuse of safety process artefacts and components is very difficult, often even impossible. We argue that a better criterion is to use QoS (Quality of Service) as this expresses the point of view of the user in terms of trustworthiness, independently of the domain. The cross domain reuse as goal is also hampered by the way the SIL level is obtained with SIL as such is a system specific property. This is in contrast with the engineering practice to reuse components whenever possible. Altreonic defined a new criterion called ARRL (Assured Reliability and Resilience Level) that can be used to guide the architectural design and validation. The ARRL criterion takes into account the functional properties when faults occur. It complements the SIL criterion similarly like a HARA and FMEA complement each other. It also allows to define rules whereby components are assembled in a system to meet a corresponding SIL level, hence allowing composable safety. The ARRL criterion is also the driving criterion behind the R&D roadmap of Altreonic. This will briefly be illustrated by the formal development of the networkcentric OpenComRTOS and by the development of the traceability and requirements driven metamodel behind the GoedelWorks project portal. The latter will use a generic process pattern. The combination of OpenComRTOS Designer and GoedelWorks portal provides for cross domain and cost efficient support for safety and systems engineering. 
Keywords: tba 
Slides: tba 
5th of June, 2013 
Uma curta introdução ao BitCoin 
Manuel Barbosa (HASLab) 
Keywords: BitCoin 
Slides: tba 
29th of May, 2013 
AJITTS: Adaptive JustInTime Transaction Scheduling 
Ana Nunes (HASLab) 
Distributed transaction processing has benefited greatly from optimistic concurrency control protocols thus avoiding costly finegrained synchronization. However, the performance of these protocols degrades significantly when the workload increases, namely, by leading to a substantial amount of aborted transactions due to concurrency conflicts. Our approach stems from the observation that the abort rate increases with the load as already executed transactions queue for longer periods of time waiting for their turn to be certified and committed. We thus propose an adaptive algorithm for judiciously scheduling transactions to minimize the time during which these are vulnerable to being aborted by concurrent transactions, thereby reducing the overall abort rate. We do so by throttling transaction execution using an adaptive mechanism based on the locally known state of globally executing transactions, that includes outoforder execution. Our evaluation using traces from the industry standard TPCE workload shows that the amount of aborted transactions can be kept bounded as system load increases, while at the same time fully utilizing system resources and thus scaling transaction processing throughput. 
Keywords: Distributed Systems, AJITTS, Evaluation 
Slides: tba 
22th of May, 2013 
Interactive Interaction Constraints 
José Proença (KU Leuven) 
Interaction constraints are an expressive formalism for describing coordination patterns, such as those underlying the coordination language Reo, that can be efficiently implemented using constraint satisfaction technologies such as SAT and SMT solvers. Existing implementations of interaction constraints interact with external components only in a very simple way: interaction occurs only between rounds of constraint satisfaction. What is missing is any means for the constraint solver to interact with the external world during constraint satisfaction. This work introduces interactive interaction constraints which enable interaction during constraint satisfaction, and in turn increase the expressiveness of coordination languages based on interaction constraints by allowing a larger class of operations to be considered to occur atomically. We describe how interactive interaction constraints are implemented and detail a number of strategies for guiding constraint solvers. The benefit of interactive interaction constraints is illustrated using small examples. From a general perspective, our work describes how to open up and exploit constraint solvers as the basis of a coordination engine. 
Keywords: Interactive Interaction, Constraint Solving, Coordination, Reo 
Slides 
17th of April, 2013 
Statically enforcing complex invariants in structured documents 
Dario Teixeira 
Lambdoc is an opensource library offering support for semantically rich structured documents in web applications [1]. It is particularly aimed at web sites that accept usercontributed content and wish to ensure that such content follows strict guidelines regarding soundness and typographic conventions. This talk consists of two parts. The first part provides the context and motivation for the Lambdoc library, together with a brief overview of its features. The second part comprises the bulk of the talk, and discusses the application of the type system of statically typed functional languages such as OCaml and Haskell to enforce complex invariants on document structure. This latter discussion takes the form of a journey, which begins with Phantom Types and ends with Generalized Abstract Data Types (GADTs). Each of these concepts is briefly introduced and its strengths and weaknesses in a practical setting evaluated. Note that the presentation focuses mainly on the OCaml language. However, given the prevalence of Haskell in academia, a brief "OCaml for Haskellers" overview is also provided. Moreover, the OCaml code samples are simple enough to be understandable by anyone with some familiarity with Haskell or any other functional language with parametric polymorphism and algebraic data types.
[1] http://lambdoc.forge.ocamlcore.org/ 
Keywords: tba 
Slides 
10th of April, 2013 
MeT: Workload aware elasticity for NoSQL 
Francisco Cruz (HASLab) 
NoSQL databases manage the bulk of data produced by modern Web applications such as social networks. This stems from their ability to partition and spread data to all available nodes, allowing NoSQL systems to scale. Unfortunately, current solutions’ scale out is oblivious to the underlying data access patterns, resulting in both highly skewed load across nodes and suboptimal node configurations. In this paper, we first show that judicious placement of HBase partitions taking into account data access patterns can improve overall throughput by 35%. Next, we go beyond current state of the art elastic systems limited to uninformed replica addition and removal by: i) reconfiguring existing replicas according to access patterns and ii) adding replicas specifically configured to the expected access pattern. MET is a prototype for a Cloudenabled framework that can be used alone or in conjunction with OpenStack for the automatic and heterogeneous reconfiguration of a HBase deployment. Our evaluation, conducted using the YCSB workload generator and a TPCC workload, shows that MET is able to i) autonomously achieve the performance of a manual configured cluster and ii) quickly reconfigure the cluster according to unpredicted workload changes. 
Keywords: tba 
Slides: tba 
3rd of April, 2013 
"Pointfree" Putbased Bidirectional Programming Abstract 
Hugo Pacheco (National Institute of Informatics (NII), Tóquio, Japão) 
Bidirectional transformations and in particular lenses, programs with a forward get transformation and a backward putback transformation, are routinely written in ways that do not let programmers specify their behavior completely. Several bidirectional programming languages exist to aid programmers in writing a (usually simpler) forward transformation, and deriving a backward transformation for free. However, the maintainability offered by such languages comes at the cost of expressiveness because the ambiguity of synchronization – handled by the putback transformation – is solved by default strategies which are hidden from programmers. In this paper, we argue that such ambiguity is essential for bidirectional transformations and propose a novel putbackbased bidirectional language in which programmers write putback synchronization strategies from the start. In sharp contrast with traditional getbased languages, our putbackbased language allows programmers to describe the behavior of a bidirectional transformation completely, while retaining the maintainability of writing a single program. We demonstrate that this additional power is manageable in practice through a series of examples, ranging from simple ones that illustrate traditional lenses to complex ones for which our putbackbased approach is central to specifying their nontrivial update strategies. Our examples are inspired by existing problems from the functional and database programming fields. 
Keywords: tba 
Slides: tba 
27th of March, 2013 
Slicing as a Distributed Systems Primitive 
Francisco Maia (HASLab) 
Largescale distributed systems appear as the major infrastructures for supporting planetscale services. These systems call for appropriate management mechanisms and protocols. Slicing is an example of an autonomous, fully decentralized protocol suitable for largescale environments. It aims at organizing the system into groups of nodes, called slices, according to an applicationspecific criteria where the size of each slice is relative to the size of the full system. This allows assigning a certain fraction of nodes to different task, according to their capabilities. Although useful, current slicing techniques lack some features of considerable practical importance. This paper proposes a slicing protocol, that builds on existing solutions, and addresses some of their frailties. We present novel solutions to deal with nonuniform slices and to perform online and dynamic slices schema reconfiguration. Moreover, we describe how to provision a slicelocal Peer Sampling Service for upper protocol layers and how to enhance slicing protocols with the capability of slicing over more than one attribute. Slicing is presented as a complete, dependable and integrated distributed systems primitive for largescale systems. 
Keywords: tba 
Slides: tba 
20th of March, 2013 
On the semantic security of functional encryption schemes 
Manuel Barbosa (HASLab) 
Functional encryption (FE) is a powerful cryptographic primitive that generalizes many asymmetric encryption systems proposed in recent years. Syntax and security definitions for FE were proposed by Boneh, Sahai, and Waters (BSW) (TCC 2011) and independently by O’Neill (ePrint 2010/556). In this paper we revisit these definitions, identify several shortcomings in them, and propose a new definitional approach that overcomes these limitations. Our definitions display good compositionality properties and allow us to obtain new feasibility and impossibility results for adaptive tokenextraction attack scenarios that shed further light on the potential reach of general FE for practical applications. 
Keywords: tba 
Slides: tba 
13th of March, 2013 
Composing Leastchange Lenses 
Alcino Cunha (HASLab) 
Nontrivial bidirectional transformations (BXs) are inherently ambiguous, as there are in general many different ways to consistently translate an update from one side to the other. Existing BX languages and frameworks typically satisfy only fundamental first principles which ensure acceptable and stable (wellbehaved) translation. Unfortunately, these requirements give little insight about how a particular update translation is chosen among the myriad possible. From the user perspective, such unpredictability may hinder the adoption of BX frameworks. This problem can be remedied by imposing a "principle of least change": in a statebased framework this amounts to translating updates so that the result is as close as possible to the original state according to some distance measure. In this paper we start by formalizing such BXs, focusing on the particular framework of lenses. We then discuss whether such leastchange lenses can be defined by composition, an essential construct of BX frameworks. For sequential composition, we present two (dual) update translation alternatives: a classical deterministic one and a nondeterministic one where composition may require backtracking. A key ingredient of our paper is the reasoning style which, carried out in relational algebra, achieves elegant formalizations and exposes several similarities and dualities. 
Keywords: Bidirectional Transformations, Lenses 
Slides: tba 
27th of February, 2013 
Implementing QVTR Bidirectional Model Transformations using Alloy 
Nuno Macedo (HASLab) 
QVT Relations (QVTR) is the standard language proposed by the OMG to specify bidirectional model transformations. Unfortunately, due to ambiguities in its original semantics, acceptance and development of effective tool support has been slow. Although the bidirectional check semantics have been clarified recently, none of the existing QVTR tools have been shown to correctly implement it. Even worst, many tools do not even comply to the standard language, none supports OCL constraints over the metamodels (thus being prone to return illformed models), and none clearly formalizes how enforce semantics picks a target model from the myriad consistent candidates. In this paper we propose a QVTR tool that overcomes all these issues: it supports a large subset of QVTR and UML class diagrams annotated with OCL, complies to the bidirectional check semantics of [1], and enforces update propagation according to the predictable ``principle of least change''. We achieve this by embedding both QVTR transformations and UML class diagrams (annotated with OCL) in Alloy, a lightweight formal specification language with support for automatic model finding via SAT solving. The proposed tool already proved effective in debugging existing transformations, namely unveiling several errors in the wellknown objectrelational mapping that illustrates OMG's QVTR specification. 
Keywords: QVTR, Bidirectional Transformations, Alloy 
Slides: tba 
5th of March, 2013 
Just Do It While Compiling! Fast Extensible Records In Haskell 
Alberto Pardo (Instituto de Computacion, Universidad de la Republica, Montevideo, Uruguay) 
The library for strongly typed heterogeneous collections HList provides an implementation of extensible records in Haskell that needs only a few common extensions of the language. In HList, records are represented as linked lists of labelvalue pairs with a lookup operation that is lineartime in the number of ﬁelds. In this paper, we use typelevel programming techniques to develop a more efﬁcient representation of extensible records for HList. We propose two internal encodings for extensible records that improve lookup at runtime without needing a total order on the labels. One of the encodings performs lookup in constant time but at a cost of linear time insertion. The other one performs lookup in logarithmic time while preserving the fast insertion of simple linked lists. Through staged compilation, the required slow search for a ﬁeld is moved to compile time in both cases. This is a joint work with Bruno Martinez and Marcos Viera recently presented at PEPM 2013. 
Slides: tba 
6th of March, 2013 
Exceptionally, this seminar will take place in the Physics Department at 14:30h. 
The logic of nonlocality and quantum informatics 
Rui Soares Barbosa (Department of Computer Science  University of Oxford) 
tba 
Keywords: tba 
Slides: tba 
12th of December, 2012 
Clouder: A Flexible Large Scale Decentralized Object Store 
Ricardo Vilaça (HASLab) 
Large scale data stores have been initially introduced to support a few concrete extreme scale applications, such as social networks. Their scalability and availability requirements often sacrifice richer data and processing models, and even elementary data consistency. In strong contrast with traditional relational databases (RDBMS), large scale data stores present very simple data models and APIs, lacking most of the established relational data management operations, and presenting relaxed consistency guarantees, providing eventual consistency. This thesis aims at reducing the gap between traditional RDBMS and large scale data stores by seeking mechanisms to provide additional consistency guarantees, and higherlevel data processing primitives in large scale data stores. The devised mechanisms should not hinder the scalability and dependability of large scale data stores. Regarding higherlevel data processing primitives, this thesis explores two complementary approaches: extending data stores with additional operations such as general multiitem operations; and coupling data stores with other existing processing facilities without hindering scalability. We demonstrate our approaches with running prototypes and extensive experimental evaluation using proper workloads. 
Keywords: tba 
Slides: tba 
Lightning Talk 1 (5 min.): tba 
Lightning Talk 2 (5 min.): tba 
5th of December, 2012 
Calculating Fault Propagation in Functional Programs using the Linear Algebra of Programming (LAoP) 
J.N. Oliveira (HASLab) 
How do software faults propagate in computer programs/systems? Can faulty behavior be predicted in some way, eg. by calculation? Are there versions of the same program / software system which are "better" than others concerning fault propagation? This talk will not provide definite answers to these questions but it will point towards a strategy to handle them. First, faulty behavior can be mimicked probabilistically, and faults can be injected and simulated using monadic programming (see eg. the Probabilistic Functional Programming  PFP library developed in Haskell by M. Erwig). Second, rather than observing propagation patterns by repeated simulation, such programs can be converted into isomorphic matricial versions and reasoned about in the socalled Linear Algebra of Programming (LAoP), an extension of the AoP towards quantitative reasoning. Simple examples (such as those given in eg. DOI: 10.1007/s0016501202409) show that faultyprogram fusion can be calculated and the way faults combine with each other can be expressed using probabilistic (choice) combinators. Future work includes extending the approach to componentoriented software systems modeled as coalgebras of functors involving the distribution monad, thus scaling up from functional programs to software architectures. 
Keywords: Fault propagation, LAoP 
Slides: PDF (updated: Jan 2013) 
7th of November, 2012 
HCI for Safety Critical Interactive Applications: Commonalities and Differences between Air Traffic Control, Satelite Ground Segments and Large Civil Aircrafts Cockpits 
Philippe Palanque (IRIT, Toulouse) 
Recent years have seen an increasing use of sophisticated interaction techniques in the field of command and control systems. The use of such techniques has been required in order to increase the bandwidth between the users and the systems and thus to help them deal efficiently to increasingly complex systems. These techniques come from research and innovation done in the field of HCI but very little has been done to improve their reliability and their tolerance to human error. It can be difficult to know how to assess the risks that such systems can create for the successful operation of safetycritical systems. One consequence of this is that interaction issues are almost entirely missing from international development standards in safetycritical systems, such as IEC615098 or DO 178B. This presentation will present lessons learnt over the last 20 years on developing research in HCI for safety critical interactive systems as well as applying the results in different application domains such as cockpits of large civil aircrafts, air traffic management and satellite ground segments. 
Keywords: Safety Critical, Interactive Applications 
Slides: tba 
24th of October, 2012 
Can GUI implementation markup languages be used for modelling? 
Carlos E. Silva (HASLab) 
The current diversity of available devices and form factors increases the need for modelbased techniques to support adapting applications from one device to another. Most work on user interface modelling is built around declarative markup languages. Markup languages play a relevant role, not only in the modelling of user interfaces, but also in their implementation. However, the languages used by each community (modellers/developers) have, to a great extent evolved separately. This means that the step from concrete model to final interface becomes needlessly complicated, requiring either compilers or interpreters to bridge this gap. In this paper we compare a modelling language (UsiXML? ) with several markup implementation languages. We analyse if it is feasible to use the implementation languages as modelling languages. 
Keywords: User Interfaces, Modelling, Markup languages 
Slides: tba 
10th of October, 2012 
Dynamic contracts for verification and enforcement of realtime systems properties 
André Pedro 
Realtime systems are systems where clearly the runtime verification is indispensable, not only due to the high complexity which make static approaches practically unfeasible, but also due to their high dependence of temporal constraints (e.g., model checking  where models becomes undecidable to check due to the time clock operations: addiction, subtraction by a constant, etc.). The research of techniques for such systems has been growing progressively along the past years due to high need of reliable and safe development complements and alternatives to static approaches. However, the trend towards the research of new dynamic approaches has been higher for soft realtime systems rather than for hard realtime systems (i.e., focusing essentially on the functional aspects). The talk presents briefly the underlying concepts of runtime verification, its motivation, and introduces a specification language prototype proposed by us for monitor generation as well as a practical case study, focusing on hard realtime embedded systems. 
Keywords: tba 
Slides: tba 
26th of September, 2012 
Extension and Implementation of ClassSheet Models 
Jácome Cunha (HASLab) 
In this talk we explore the use of models in the context of spreadsheet engineering. We review a successful spreadsheet modeling language, whose semantics we further extend. With this extension we bring spreadsheet models closer to the business models of spreadsheets themselves. An addon for a widely used spreadsheet system, providing bidirectional modeldriven spreadsheet development, was also improved to include the proposed model extension. 
Keywords: tba 
Slides: tba 
A Web Portal for the Certification of Open Source Software 
Pedro Martins (HASLab) 
In this talk we will present a web portal for the certification of open source software. The portal aims at helping programmers in the internet age, when there are (too) many open source reusable libraries and tools available. Our portal offers programmers a webbased and easy setting to analyze and certify open source software, which is a crucial step to help programmers choosing among many available alternatives, and to get some guarantees before using one piece of software. We will also present our first prototype of such web portal. We will describe in detail a domain specific language that allows programmers to describe with a high degree of abstraction specific open source software certifications. The design and implementation of this language is the core of the web portal. 
Keywords: tba 
Slides: tba 
12th of September, 2012 
Bidirectional Data Transformation by Calculation 
Hugo Pacheco (HASLab) 
The advent of bidirectional programming, in recent years, has led to the development of a vast number of approaches from various computer science disciplines. These are often based on domainspecific languages in which a program can be read both as a forward and a backward transformation that satisfy some desirable consistency properties. Despite the high demand and recognized potential of intrinsically bidirectional languages, they have still not matured to the point of mainstream adoption. This dissertation contemplates some usually disregarded features of bidirectional transformation languages that are vital for deployment at a larger scale. The first concerns efficiency. Most of these languages provide a rich set of primitive combinators that can be composed to build more sophisticated transformations. Although convenient, such compositional languages are plagued by inefficiency and their optimization is mandatory for a serious application. The second relates to configurability. As update translation is inherently ambiguous, users shall be allowed to control the choice of a suitable strategy. The third regards genericity. Writing a bidirectional transformation typically implies describing the concrete steps that convert values in a source schema to values a target schema, making it impractical to express very complex transformations, and practical tools shall support concise and generic coding patterns. 
Keywords: Bidirectional Transformations, Data Calculation 
Slides: tba 
Evolution of ModelDriven Spreadsheets Spreadsheets 
Jorge Mendes (HASLab) 
Spreadsheets are the most used programming environment, mostly because they are very flexible. This is due to the lack of restrictions imposed on them which can lead to lots of errors. ModelDriven Engineering was already suggested to improve spreadsheets, providing them with specications and checking tools. However, users have to learn to use these tools on top of their existing spreadsheet host system. To remove that difficulty, the work for this thesis describes an embedding of spreadsheet models within spreadsheet themselves. Moreover, a set of operations that can be performed on these models and respective instances is defined. This way, users interact with models and spreadsheets in the same environment with the objective to improve work performance and reduce errors. Resulting from this work, a prototype was created and is also discussed in this dissertation. This prototype can be used to validate the approach taken in this thesis and to provide a base framework for future developments. 
Keywords: tba 
Slides: Spreadsheets, Modedriven Spreadsheet Engineering, Evolution, Bidirectional Transformations 
5th of September, 2012 
Designing interactive software for medical device user interfaces: case studies on drug infusion pumps 
Paolo Masci (Queen Mary University of London) 
This seminar will be of interest to anybody involved in the design or development of interactive systems. We will discuss some of our recent work carried out within the CHI+MED project (http://www.chimed.ac.uk), where we integrate empirical approaches with mathematical methods to deliver a richer analysis of safetycritical interactive systems. We will focus on automated analysis of interactive software incorporated in infusion pumps  interactive medical devices used in healthcare to deliver drugs and nutrients to patients. Case studies based on commercial infusion pumps will be presented. First, we present our recent work [1,2] on the verification of 'predictability', an interaction design principle that concerns the ability of a user to determine the outcome of future interactions. We will illustrate how: (i) precise insights can be gained about situations where interaction design seems awkward and may lead to use errors; (ii) verified solutions can be developed that fix the interaction design; (iii) simple user strategies can be identified that can be safely used to overcome identified issues in devices already on the market. Second, we present our ongoing work on the UNIPump framework, a formal framework to support a uniform and rigorous approach for specifying and verifying safety requirements for interactive software incorporated in infusion pump user interfaces. This work aims to complement the Generic Infusion Pump (GIP) framework supported by the University of Pennsylvania and the FDA for modeldriven development of software incorporated in infusion pumps. The existing GIP is restricted to software for the control logic of infusion pumps. It does not directly tackle interactive software for the user interface, which is also necessary to demonstrate device safety. The UNIPump framework addresses this gap. [1] P. Masci, R. Ruksenas, P. Curzon, et.al., "On formalising interactive number entry on infusion pumps.", ECEASST 45 (2011), available at http://www.eecs.qmul.ac.uk/~masci/ [2] P. Masci, R. Ruksenas, P. Curzon, et.al., "The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps.", submitted for publication to Innovations in Systems and Software Engineering (2012). Preprint available at http://tinyurl.com/masciQMpreprints 
Keywords: tba 
Slides: tba 
20th of June, 2012 
Formal Verification of Cryptographic Software Implementations 
Bárbara Vieira (HASLab) 
We explore how formal techniques, namely deductive verification techniques, can be used to increase the guarantees that cryptographic software implementations indeed work as prescribed. First we identify relevant security policies that may be at play in cryptographic systems, as well as the languagebased mechanisms that can be used to enforce such policies in those systems. We propose methodologies based on deductive verification to formalise and verify relevant security policies in cryptographic software. We also propose a deductive verification tool for a domainspecific language for cryptographic implementations, that can be used to verify the previously identified security policies. At the very end, we conclude our work by reasoning about the soundness of our verification tool. 
Keywords: tba 
Slides: tba 
6th of June, 2012 
Automatic parameter estimation of the iSAX time series representation 
Nuno Castro (HASLab) 
The key to scalable mining algorithms is to select a suitable representation of the data. From the existing techniques, the Symbolic Aggregate Approximation (SAX) has been widely used in the time series data mining community. Its popularity arises from the fact that it is symbolic, reduces the dimensionality of the series, allows lower bounding and is space efficient. However, the need to set the symbolic length and alphabet size parameters limits the applicability of the representation since the best parameter setting is highly application dependent. Typically, these are either set to a fixed value (e.g. 8) or experimentally probed for the best configuration. In this work, we aim to tackle this limitation by introducing a novel technique to automatically derive these parameters. The technique, referred as AutoiSAX, not only discovers the best parameter setting for each time series in the database but also finds the alphabet size for each iSAX symbol within the same word. It is based on the simple and intuitive ideas of time series complexity and segment standard deviation. The technique can be smoothly embedded in existing data mining tasks as an efficient subroutine. We analyse the impact of using AutoiSAX in visualisation interpretability, and motif mining results. Our contribution aims to make iSAX a more general approach as it evolves towards a parameterfree method. 
Keywords: tba 
Slides: tba 
23rd of May, 2012 
Modelling and systematic analysis of interactive systems (tentative title) 
José Creissac Campos (HASLab) 
In this talk I will address some of the more recent work on the modelling and systematic analysis of interactive system being done at HASLab. The main focus will be on ubiquitous computing system. The is the rehearsal of an invited talk to be given at QMUL the following week. 
Keywords: tba 
Slides: tba 
9th of May, 2012 
Strong Eventual Consistency for scalable distribution 
Carlos Baquero (HASLab) 
In this presentation we establish the conditions for strong eventual consistent datatypes (with no rollback allowed) and present two equivalent implementation flavors: State Based, with a defined merge operation and constraints that ensure that mutating operations are compatible with merge; Operation Based, building on top of a causal delivery middleware and ensuring that concurrent operations commute. In particular, we will show Set implementations that match this design. 
Slides: tba 
28th of March, 2012 
Middleware for the NOSQL generation: Challenges and opportunities 
José Orlando Pereira (HASLab) 
The middleware stack based on a relational database management system (RDBMS) has been the workhorse of the IT industry, incrementally extending the decades old RDBMS with concepts such as objectrelational mapping, caching, sharding, and replication. More recently, there has been a growing shift towards the so called NoSQL databases, stemming mostly from the requirements of extremely large applications offered as services (SaaS), but also from novel platforms as a service (PaaS). By departing from the traditional architecture and interfaces of the venerable RDBMS, this movement shatters the foundation of database middleware stack. In this talk we start by examining the assumptions and goals of each layer in the the traditional stack, including the RDBMS. Then we reevaluate those assumptions and goals in the context of a NoSQL database such as Cassandra or HBase. This leads us to discuss to what extent the role of the database has changed and what should now be expected from middleware. Although there is room for some of the traditional middleware concepts, there are others that have become obsolete, and also some new challenges and opportunities. 
Keywords: tba 
Slides: tba 
21st of March, 2012 
From Relational ClassSheets to UML+OCL 
Jácome Cunha (HASLab) 
Spreadsheets are among the most popular programming languages in the world. Unfortunately, spreadsheet systems were not tailored from scratch with modern programming language features that guarantee, as much as possible, program correctness. As a consequence, spreadsheets are populated with unacceptable amounts of errors. In other programming language settings, modelbased approaches have been proposed to increase productivity and program effectiveness. Within spreadsheets, this approach has also been followed, namely by ClassSheets. In this paper, we propose an extension to ClassSheets to allow the specification of spreadsheets that can be viewed as relational databases. Moreover, we present a transformation from ClassSheet models to UML class diagrams enriched with OCL constraints. This brings to the spreadsheet realm the entire paraphernalia of model validation techniques that are available for UML. 
Keywords: Spreadsheets, UML, OCL, ClassSheets 
Slides: tba 
14th of February, 2012 
Robust Distributed Data Aggregation 
Paulo Jesus (HASLab) 
Distributed aggregation algorithms are an important building block of modern large scale systems, as it allows the determination of meaningful systemwide properties (e.g., network size, total storage capacity, average load, or majorities) which are required to direct the execution of distributed applications. In the last decade, several algorithms have been proposed to address the distributed computation of aggregation functions (e.g., COUNT, SUM, AVERAGE, and MAX/MIN), exhibiting different properties in terms of accuracy, speed and communication tradeoffs. However, existing approaches exhibit many issues when challenged in faulty and dynamic environments, lacking in terms of faulttolerance and support to churn. This study details a novel distributed aggregation approach, named Flow Updating, which is faulttolerant and able to operate on dynamics networks. The algorithm is based on manipulating flows (inspired by the concept from graph theory), that are updated using idempotent messages, providing it with unique robustness capabilities. Experimental results showed that Flow Updating outperforms previous averaging algorithms in terms of time and message complexity, and unlike them it selfadapts to churn and changes of the initial input values without requiring any periodic restart, supporting node crashes and high levels of message loss. 
Keywords: Data aggregation, Distributed algorithms, Dynamic networks, Faulttolerance 
Slides: tba 
22th of February, 2012 
Subgroup Discovery driven by a user defined property of interest 
Paulo Azevedo (HASLab) 
In this talk I will describe a framework based on association rules for the discovery of pertinent subgroups of a population according to a defined property of interest. The main idea of subgroup mining is to identify the characteristics of subpopulations that deviate from the global population, according to a user defined property. This property can be represented by categorical values, numerical, a contrast (frequency comparison) or even a distribution. A classical application on census data identifies discrimination on wage for subgroups formed by females with low education when compared to the global population. Other example on medical data identifies characteristics of subgroups with abnormal distribution of the Cholesterol values when compared to the global population. Several instances of this framework will be described, like contrast sets mining, distribution rules and Distribution Learning. 
Slides 
8th of February, 2012 
Every transformation is a lens: Taming partiality using invariants and nondeterminism 
Nuno Macedo (HASLab) 
Total wellbehaved lenses are restricted to surjective functions. However, many useful transformations are not surjective. To support these, most lens frameworks relax the totality requirement and weaken the roundtripping laws, opening the door to unpredictable synchronization behaviors. We propose a framework where any transformation written in a pointfree functional language can be lifted to a total wellbehaved lens, by capturing the exact range and domain of the transformation as invariants on the target and source datatypes. To enforce such invariants, the proposed framework relies on nondeterministic execution of backward transformations. Both these and the data invariants are naturally specified using a pointfree relational calculus that enables concise and agile algebraic reasoning. 
Keywords: Bidirectional transformations, Pointfree relational calculus, Data invariants, Nondeterminism 
Slides: tba 
1st of February, 2012 
Delegatable Homomorphic Encryption with Applications to Secure Outsourcing of Computation 
Manuel Barbosa (HASLab) 
In this work we propose a new cryptographic primitive called Delegatable Homomorphic Encryption (DHE). This allows a Trusted Authority to control/delegate the capability to evaluate circuits over encrypted data to untrusted workers/evaluators by issuing tokens. This primitive can be both seen as a publickey counterpart to Verifiable Computation, where input generation and output verification are performed by different entities, or as a generalisation of Fully Homomorphic Encryption enabling control over computations on encrypted data. Our primitive comes with a series of extra features as follows: 1) there is a onetime setup procedure for all circuits; 2) senders do not need to be aware of the functions which will be evaluated on the encrypted data, nor do they need to register keys; 3) tokens are independent of senders and receiver; and 4) receivers are able to verify the correctness of computation given short auxiliary information on the input data and the function, independently of the complexity of the computed circuit. We give a modular construction of such a DHE scheme from three components: Fully Homomorphic Encryption (FHE), Functional Encryption (FE), and a (customised) MAC. As a stepping stone, we first define Verifiable Functional Encryption (VFE), and then show how one can build a secure DHE scheme from a VFE and an FHE scheme. We also show how to build the required VFE from a standard FE together with a MAC scheme. All our results hold in the standard model. Finally, we show how one can build a verifiable computation (VC) scheme generically from a DHE. As a corollary, we get the first VC scheme which remains verifiable even if the attacker can observe verification results. 
Keywords: Homomorphism delegation, Homomorphic encryption, Functional encryption, Verifiable computation, Publickey cryptography, Provable security 
Slides: tba 
11th of January, 2012 
Implementing sound in a CAVElike system while ensuring the “synchrony” of the virtual world 
Carlos CL Silva (HASLab/LVP) 
Although great developments have been made in the generation of ever more visually immersive virtual reality (VR) environments, audiovisual interactive VR environments are still conceived as an enormous challenge, mostly due to ignorance about some audiovisual processes, such as the audiovisual perception of synchrony. Psychophysically, audiovisual perception is still an intriguing phenomenon, especially when we think about time differences – both at the physical and neural level – underlying the perception of sound and light. Thus, in order to develop a truly immersive audiovisual VR environment we need to know how human beings deal with these differences and perceive synchrony between sound and image. This presentation intends to expose these problems and discuss possible solutions for the implementation process of an auditory VR environment in a CAVElike system at the Laboratory of Visualization and Perception in the University of Minho. Moreover, we will explore this case as an example of the historical contribution of Psychology and Psychophysical research as a start and an ending point in the processes of developing technology for interactive VR environments. 
4th of January, 2012 
FaultTolerant Aggregation: FlowUpdating Meets MassDistribution 
Carlos Baquero (HASLab) 
FlowUpdating (FU) is a faulttolerant technique that has proved to be efficient in practice for the distributed computation of aggregate functions in communication networks where individual processors do not have access to global information. Previous distributed aggregation protocols, based on repeated sharing of input values (or mass) among processors, sometimes called MassDistribution (MD) protocols, are not resilient to communication failures (or message loss) because such failures yield a loss of mass. In this paper, we present a protocol which we call MassDistribution with FlowUpdating (MDFU). We obtain MDFU by applying FU techniques to classic MD. We analyze the convergence time of MDFU showing that stochastic message loss produces low overhead. This is the first convergence proof of an FUbased algorithm. We evaluate MDFU experimentally, comparing it with previous MD and FU protocols, and verifying the behavior predicted by the analysis. Finally, given that MDFU incurs a fixed deviation proportional to the messageloss rate, we adjust the accuracy of MDFU heuristically in a new protocol called MDFU with Linear Prediction (MDFULP). The evaluation shows that both MDFU and MDFULP behave very well in practice, even under high rates of message loss and even changing the input values dynamically. 
Slides: tba 
21st of December, 2011 
Translating Alloy Specifications to UML Class Diagrams Annotated with OCL 
Ana Garis (HASLab/Universidad Nacional de San Luis, Argentina) 
ModelDriven Engineering (MDE) is a Software Engineering approach based on model transformations at different abstraction levels. It prescribes the development of software by successively transforming models from abstract (specifications) to more concrete ones (code). Alloy is an increasingly popular lightweight formal specification language that supports automatic verification. Unfortunately, its widespread industrial adoption is hampered by the lack of an ecosystem of MDE tools. We present a model transformation between Alloy and UML Class Diagrams annotated with OCL. The proposed transformation enables current UMLbased tools to also be applied to Alloy specifications, thus unleashing its potential for MDE. 
Slides: tba 
21st of December, 2011 
Archery  Modelling of Architectural Patterns 
Alejandro Sanchez (HASLab/Universidad Nacional de San Luis, Argentina) 
In a number of contexts the term “architectural pattern” is used as an architectural abstraction. The expression is taken in the usual sense of pattern in object oriented programming  a known design solution to recurring problems. Available pattern catalogs allow to design and evolve architectures by applying them. However, its characterizations remain largely informal, enough to generate a vocabulary for design discussions at a high abstraction level, but insufficient to underpin, for instance, executable models. We describe Archery, a language for modelling of architectural patterns, supporting hierarchical composition and a type discipline. We provide formal semantics for the behavioural and structural dimensions by respective translations to mCRL2 and to bigraphical reactive systems. 
Slides: tba 
14th of December, 2011 
Systems Biology, a holistic approach to the "algebra" of Life 
Daniel Machado (IBB/CEB  UMinho) 
The cell is the fundamental building block of life. From this basic unit, a myriad of life forms have emerged. Systems Biology is a recent field that studies the complex interactions that happen inside a cell. It represents a new holistic paradigm when compared to the traditional reductionist perspective to biology. The multidisciplinary nature of this field requires the integration of several areas such as computer science, mathematics, physics, chemistry, biology and systems engineering. Building a wholecell model is its ultimate goal, hampered by the difficulty of "reverse engineering" the specification of a system that evolved in nature. Although still far from this goal, several models of different organisms have been built. These provide a platform for performing "in silico" experiments that allow us to understand the cellular behavior and also to predict the optimal manipulations towards a specific objective. Therefore, they have several applications in biomedical research for the study of diseases and novel drug discovery, as well as in industrial biotechnology for the creation of microbial cell factories that produce a wide range of commodity chemicals. 
Slides: tba 
7th of November, 2011 
Experimental Evaluation of Distributed Middleware with a Virtualized Java Environment 
Nuno Carvalho (HASLab) 
The correctness and performance of large scale service oriented systems depend on distributed middleware components performing various communication and coordination functions. It is, however, very difficult to experimentally assess such middleware components, as interesting behavior often arises exclusively in large scale settings, but such deployments are costly and time consuming. We address this challenge with MINHA, a system that virtualizes multiple JVM instances within a single JVM while simulating key environment components, thus reproducing the concurrency, distribution, and performance characteristics of the actual system. The usefulness of MINHA is demonstrated by applying it to the WS4D Java stack, a popular implementation of the Devices Profile for Web Services (DPWS) specification. 
Slides: tba 
7th of November, 2011 
Formal Verification of Ada Programs: An Approach based on Model Checking 
João Martins (HASLab) 
The rapid growth of the complexity of software systems demands, now more than ever, a rigorous validation of these systems in order to maintain or even increase their reliability. The talk will describe a toolsupported method for the formal verification of Ada programs. It presents ATOS, a tool that automatically extracts from an Ada program a SPIN model, together with a set of desirable properties. ATOS is also capable of extracting properties from a specification annotated by the user in the program, inspired by the Spark Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada programs, based on model checking. 
Slides: tba 
30th of November, 2011 
Dotted Version Vectors: Efficient Causality Tracking for Distributed KeyValue Stores 
Carlos Baquero (HASLab) 
In cloud computing environments, data storage systems often rely on optimistic replication to provide good performance to geographically disperse users and to allow operation even in the presence of failures or network partitions. In this scenario, it is important to be able to accurately and efficiently identify updates executed concurrently. In this paper, first we review, and expose problems with current approaches to causality tracking in optimistic replication: these either lose information about causality or do not scale, as they require replicas to maintain information that grows linearly with the number of clients or updates. Then, we propose a novel, scalable solution that fully captures causality: it maintains very concise information that grows linearly only with the number of servers that register updates for a given data element, bounded by the degree of replication. Moreover, causality can be checked in $O(1)$ time instead of O(n) time for version vectors. We have integrated our solution in Riak, and results with realistic benchmarks show that it can use as little as 10% of the space consumed by current version vector implementation, which includes an unsafe pruning mechanism. 
Slides: tba 
23rd of November, 2011 
Estimativa de funções de probabilidade cumulativa em redes de larga escala 
Miguel Borges (HASLab) 
A capacidade de agregar dados é uma característica fundamental na concepção de sistemas de informação escaláveis, que permite a determinação de propriedades globais importantes de forma descentralizada, para a coordenação de aplicações distribuídas, ou para fins de monitorização. No entanto, são ainda relativamente escassos os trabalhos que se focam sobre a agregação de métricas expressivas dessas propriedades. Tomando como ponto de partida o actual estado da arte, será apresentado neste trabalho um algoritmo distribuído para a determinação de funções cumulativas de probabilidade em redes de larga escala. O mecanismo mostra resiliência quando submetido a perda de mensagens, é adaptável a alterações no valor amostrado e resiliente a dinamismo no número de nodos na rede. 
Slides: tba 
Avaliação realista de aplicações distribuídas num ambiente centralizado 
João Bordalo (HASLab) 
Avaliação realista e controlada de aplicações distribuídas é ainda hoje muito difícil de alcançar, especialmente em cenários de grande escala. Modelos de simulação pura podem ser uma solução para este problema, mas criar modelos abstractos a partir de implementações reais nem sempre é possível ou mesmo desejável, sobretudo na fase de desenvolvimento na qual ainda podem não existir todos os componentes ou a sua funcionalidade estar incompleta. Esta falha pode ser colmatada com a plataforma Minha, que permite uma avaliação realista das aplicações através da combinação de modelos abstractos de simulação e implementações reais num ambiente centralizado. O ponto principal desta dissertação consiste na criação de um modelo de rede a ser usado pela plataforma de modo a incluir na avaliação variáveis como os tempos necessários para a troca de mensagens, elevando assim a precisão dos resultados gerados. Para isto é apresentado o método de calibração do modelo através do qual é possível aproximar o modelo do ambiente real. Este sistema permite reproduzir as condições de um sistema em grande escala e através da manipulação de bytecode Java, suporta componentes de middleware inalterados. A utilidade deste sistema é demonstrada aplicandoo ao WS4D, uma pilha que cumpre a especificação Device Profile for Web Services. 
Slides: tba 
2nd of November, 2011 
Designing an Algorithmic Proof of the TwoSquares Theorem 
João Ferreira (University of Teesside, UK, and HASLab) 
I show a new and constructive proof of the twosquares theorem, based on a somewhat unusual but very effective, way of rewriting the socalled extended Euclid's algorithm. Rather than simply verifying the resultas it is usually done in the mathematical communityI use Euclid's algorithm as an interface to investigate which numbers can be written as sums of two squares. The precise formulation of the problem as an algorithmic problem is the key, since it allows the use of algorithmic techniques. The notion of invariance, in particular, plays a central role in the development: it is used initially to observe that Euclid's algorithm can actually be used to represent a given number as a sum of two squares, and then it is used throughout the argument to prove other relevant properties. I also show how the use of program inversion techniques can make mathematical arguments more precise. 
More info here. 
Slides: tba 
26th of October, 2011 
HaExcel: a modelbased spreadsheet evolution system 
Jácome Cunha/Jorge Mendes (HASLab) 
This paper describes the embedding of ClassSheet models in spreadsheet systems. ClassSheet models are wellknown and describe the business logic of spreadsheet data. We embed this domain specific model representation on the (general purpose) spreadsheet system. By defining such an embedding, we provide end users a modeldriven engineering spreadsheet developing environment. End users can interact with both the model and the spreadsheet data in the same environment. Moreover, we use advanced techniques to evolve spreadsheets and models and to have them synchronized. In this paper we present our work on extending a widely used spreadsheet system with such a modeldriven spreadsheet engineering environment. 
Slides (pdf) 
Demo 
19th of October, 2011 
WHISPER: Middleware for Confidential Communication in LargeScale Networks 
Etienne Riviere (University of Neuchâtel) 
A wide range of distributed applications requires some form of confidential communication between groups of users. In particular, the messages exchanged between the users and the identity of group members should not be visible to external observers. Classical approaches to confidential group communication rely upon centralized servers, which limit scalability and represent single points of failure. In this talk, I will introduce our work on WHISPER, a fully decentralized middleware that supports confidential communications within groups of nodes in largescale systems. It builds upon a peer sampling service that takes into account network limitations such as NAT and firewalls. WHISPER implements confidentiality in two ways: it protects the content of messages exchanged between the members of a group, and it keeps the group memberships secret to external observers. Using multihops paths allows these guarantees to hold even if attackers can observe the link between two nodes, or be used as content relays for NAT bypassing. Evaluation in realworld settings indicates that the price of confidentiality remains reasonable in terms of network load and processing costs. 
Slides: tba 
12th of October, 2011 
The Role of Coordination Analysis in Software Integration Projects 
Nuno Oliveira (HASLab) 
What sort of component coordination strategies emerge in a software integration process? How can such strategies be discovered and further analysed? How close are they to the coordination component of the envisaged architectural model which was supposed to guide the integration process? This talk introduces a framework in which such questions can be discussed and illustrates its use by describing part of a real casestudy. The approach is based on a methodology which enables semiautomatic discovery of coordination patterns from source code, combining generalized slicing techniques and graph manipulation. 
Slides: tba 
28th of September, 2011 
Some lightweight approaches to formal HCI 
Andy Gimblett (Swansea University) 
In this talk I will review some recent work at Swansea University in exploring application of "lightweight" formal methods to questions of HCI, whose common thread is the use of graphbased models of system structure. The approaches encompass specification, reverse engineering of running systems, and analysis of the models for HCIrelevant properties; the intent is to discover techniques which could feasibly be integrated into mainstream software development toolchains without requiring extensive expertise on the part of the tool user  hence "lightweight". The talk will be fairly informal and high level. 
Slides: tba 
27th of July, 2011 
Exploiting shared interests without disclosing them in topicbased publish/subscribe 
Miguel Matos (HASLab) 
Topicbased publish/subscribe abstracts news dissemination systems typified by RSS feeds. Existing systems either fail to take advantage of shared interests in topic subscriptions, thus incurring high maintenance/traffic costs, or require full disclosure of interests raising privacy concerns and leading to brittle structures due to clustering. We present StaN? a decentralized protocol that leverages shared interests to optimize physical resource usage of topicbased pub/sub without inducing clustering. StaN? does not require interest disclosure thus offering simple but naive privacy. With privacy being a recent concern in p2p networks we seek how to incorporate it in the existing scalable infrastructure. 
Slides: tba 
Lightning Talk 2 (5 min.): Where do algorithms "come from"? (JNO) 
20th of July, 2011 
Benchmarkbased Software Product Quality 
Tiago Alves (HASLab/SIG) 
Key to software product quality is the ability to measure, evaluate and rank software systems. In this presentation we will introduce a novel methodology to use source code metrics to evaluate and rank software systems against a benchmark. Thresholds are derived from a benchmark and used in a twostage process to aggregate metrics, first to risk profiles and afterwards to ratings. A rating summarizes a metric at systemlevel, allowing it to compare and evaluate a software. Thresholds also allow to drill down from ratings to measurements, enabling rootcause analysis. We explain the methodologies to derive thresholds from benchmark data and their role in the SIG quality model. Finally, using two spacedomain software systems, we show how the whole process enables meaningful analysis and evaluation of software systems. 
Slides: pdf 
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)  see the HASLab blog 
Lightning Talk 2 (5 min.): Where do algorithms "come from"? (JNO) 
6th of July, 2011 
(Semi) Automatic Fault Diagnosis 
Rui Maranhão (FEUP/HASLab) 
Automatic fault localization techniques aid developers/testers to pinpoint the root cause of software faults, thereby reducing the debugging effort. Depending on the amount of knowledge that is required about the system’s internal component structure and behavior, current, predominant approaches to automatic software fault localization can be classified as (1) statisticsbased approaches, and (2) reasoning approaches. Statisticsbased fault localization techniques such as SFL use program spectra to find a statistical relationship with observed failures. While modeling costs and computational complexity are minimal, SFL’s diagnostic accuracy is inherently limited as no reasoning is used. In contrast to SFL, modelbased reasoning approaches use prior knowledge of the system, such as component interconnection and statement semantics, to build a model of the correct behavior of the system. While delivering higher diagnostic accuracy, they suffer from high computation complexity. In this talk, we present a novel, lowcost, Bayesian reasoning approach to spectrumbased multiple fault localization, coined Barinel. A central feature of our contribution is the use of a generic, intermittent component failure model. Whereas previous approaches have used approximations instead, in Barinel component intermittency rate is computed as part of the posterior candidate probability computation, using a maximum likelihood estimation procedure. This procedure optimally exploits all information contained by the program spectra. Our synthetic and real software experiments (not only including wellknown benchmark programs, but also experiments on the Philips TV software) show that Barinel outperforms other stateoftheart approaches. 
Slides: tba 
29th of June, 2011 
Worldwide Consensus  Best paper award 
Francisco Maia (HASLab) 
Consensus is an abstraction of a variety of important challenges in dependable distributed systems. Thus a large body of theoretical knowledge is focused on modeling and solving consensus within different system assumptions. However, moving from theory to practice imposes compromises and design decisions that may impact the elegance, tradeoffs and correctness of theoretical appealing consensus protocols. In this paper we present the implementation and detailed analysis, in a real environment with a large number of nodes, of mutable consensus, a theoretical appealing protocol able to offer a wide range of tradeoffs (called mutations) between decision latency and message complexity. The analysis sheds light on the fundamental behavior of the mutations, and leads to the identification of problems related to the real environment. Such problems are addressed without ever affecting the correctness of the theoretical proposal. 
Slides: tba 
22nd of June, 2011 
Reasoning about Alloy Specifications using Pointfree Relational Calculus 
Nuno Macedo (HASLab) 
As a lightweight formal modeling language, Alloy focusses on quick and automatic verification of specifications, at the expense of the size of the scope of analysis. However, when modeling safetycritical systems, the need for unbounded proofs arises. Since in Alloy everything is a relation, the calculus of relations is a natural candidate to represent its specifications. As such, we propose a possible translation of Alloy models into a pointfree relational calculus, whose resulting expressions are still simple and easy to manipulate. 
Slides: (pdf) ; see also a paper in preparation on this subject 
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino) 
15th of June, 2011 
Formalizing and Implementing a Type System for a Cryptographic Language 
Paulo Silva (HASLab) 
Cryptographic software development is a challenging field not only by the inherent mathematical issues but also by the need of correctness and the lack of supporting tools. CAO is a DSL designed to aid the development of cryptographic software. The language incorporates a series of syntactic and semantic features that facilitate the development of correct and optimised cryptographic software. One of the central key features of CAO is its original type system, introducing native types such as predefined sized vectors and matrices as well as integer and polynomial moduli types. This paper presents the formalisation and the implementation of this rich CAO type system. We also show, resorting to practical examples, how this type system enforces strong typing rules and how these rules detect several common runtime errors in cryptographic algorithms. 
Slides: tba 
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino) 
8th of June, 2011 
Test case generation from mutated task models 
José Creissac Campos (HASLab) 
This talk describes an approach to the modelbased testing of graphical user interfaces from task models. Starting from a task model of the system under test, oracles are generated whose behaviour is compared with the execution of the running system. The use of task models means that the effort of producing the test oracles is reduced. It does also mean, however, that the oracles are confined to the set of expected user behaviours for the system. The talk focuses on solving this problem. It shows how task mutations can be generated automatically, enabling a broader range of user behaviours to be considered. The is the rehearsal of a talk to be given at EICS 2011 the following week. 
Slides: tba 
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino) 
1st of June, 2011 
Do the middle letters of "OLAP" stand for Linear Algebra (LA)? 
H. Macedo and J.N. Oliveira (HASLab) 
Inspired by work on pointfree relational data processing, we investigate how the generation of cross tabulations (pivot tables) and data cubes essential to online analytical processing (OLAP) and data mining can be expressed in terms of matrix multiplication, transposition and the KhatriRao matrix product, a variant of the Kronecker product. This offers much potential for parallel OLAP, as such matrix operations have a welldefined parallelization theory. We propose a simple roadmap for parallel OLAP based on a separation of concerns: rather than depending on SQLquerying and heavy machinery, one encodes the data in matrix format and relies solely on LA operations to perform OLAP operations; then such LA scripts run on a parallel machine, trusting on the efficiency of wellestablished, parallel LA kernels which have become available in areas such as eg. DSP and computer graphics. 
Slides: PDF 
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino) 
25th of May, 2011 
Distributed Systems Cloud Platform 
Francisco Maia (HASLab) 
Regardless all the theoretical results and research in the field, Distributed Systems remain considered to be a topic somehow difficult and mastered by a small group of people. However, designing and implementing Distributed Systems is essential to achieve highly resilient and robust systems. Moreover, there is still a gap between the design of distributed protocols and their implementation and deployment processes. There are a number of systems aimed at solving these problems. These systems try to provide a programming paradigm that eases the development of Distributed Systems from design to deployment. However, a unifying solution is still lacking. Recently Declarative Networking (Hellerstein et al) appeared solving some of these problems. Namely, focusing on a datacentric approach to application design. However, providing consistency guarantees in such programming model seems to require a posteriori verification of the code and, in some cases, requires the developer to rewrite the code. Building on all these observations it becomes clear that there is room for a new Distributed Systems Cloud Platform. 
Slides: tba 
Lightning Talk 1 (5 min.): MDE with Alloy @ UMinho (Alcino) 
18th of May, 2011 
Time Series Motifs Statistical Significance 
Nuno Castro (HASLab) 
Time series motif discovery is the task of extracting previously unknown recurrent patterns from time series data. It is an important problem within applications that range from finance to health. Many algorithms have been proposed for the task of efficiently finding motifs. Surprisingly, most of these proposals do not focus on how to evaluate the discovered motifs. They are typically evaluated by human experts. This is unfeasible even for moderately sized datasets, since the number of discovered motifs tends to be prohibitively large. Statistical significance tests are widely used in bioinformatics and association rules mining communities to evaluate the extracted patterns. In this work we present an approach to calculate time series motifs statistical significance. Our proposal leverages work from the bioinformatics community by using a symbolic definition of time series motifs to derive each motif's pvalue. We estimate the expected frequency of a motif by using Markov Chain models. The pvalue is then assessed by comparing the actual frequency to the estimated one using statistical hypothesis tests. Our contribution gives means to the application of a powerful technique  statistical tests  to a time series setting. This provides researchers and practitioners with an important tool to evaluate automatically the degree of relevance of each extracted motif. 
Slides (pdf) 
Slides (ppt) 
More about this topic: www.di.uminho.pt/~castro/stat 
11th of May, 2011 
Formal Verification of Security Policies 
Bárbara Vieira (HASLab) 
Formal verification of cryptographic software implementations poses significant challenges for offtheshelf tools. This is due to the domainspecific characteristics of the code, involving aggressive lowlevel optimisations and nonfunctional security requirements, namely the critical aspect of countermeasures against sidechannel attacks. We apply stateofthe art deductive verification tools to check securityrelevant properties of cryptographic software, including safety, absence of error propagation, and correctness with respect to reference implementations. 
Slides (pdf) 
Fri, 11 in February, 2011 at 11:00 
Requirements management in the CESAR project: Boilerplates and Ontologies together 
J.M. Faria (Critical Software) 
Presentation of tools and methodologies for semiautomation of requirement analysis in requirements engineering. Prospect of enriching such methodologies with formal methods support. 
Slides: tba 
Wed, 3rd of November 2010, at 9:00 (DIA2) 
Calculating (Haskell) programs from Galois connections 
J.N. Oliveira (HASLab); joint work with ShinCheng Mu (IIS, Academia Sinica, Taiwan) 
Problem statements (and software requirements) resorting to superlatives such as in eg. "... the smallest such number", "... the best approximation", "... the longest such list" lead to specifications made of two parts: one defining a broad class of solutions (the "easy" part) and the other requesting one particular such solution, which is optimal in some sense (the "hard" part). I will talk about a binary relational combinator which mirrors this linguistic structure and exploit (using pointfree relational algebra) its potential for calculating programs by optimization. This applies to handling Galois connections in which one of the adjoints delivers the optimal solution. The framework is also shown to encompass, as special cases, thinning strategies already known for refining nondeterministic, inductive specifications (vulg. "relational (un)folds"). This includes the elegant refactoring of two results by Birdde Moor (the two Greedy Theorems and the Dynamic Programming Theorem) dispensing with powersets and the power transpose. 
Slides: PDF (545k). See also Shin's research blog on this topic. 
Wed, October 06, 2010 at 09:30 (DIA2) 
The APEX framework: prototyping of ubiquitous environments based on Petri nets 
José Luís Silva (HASLab) 
The user experience of ubiquitous environments is a determining factor in their success. The characteristics of such systems must be explored as early as possible to anticipate potential user problems, and to reduce the cost of redesign. However, the development of early prototypes to be evaluated in the target environment can be disruptive to the ongoing system and therefore unacceptable. This talk reports on an ongoing effort to explore how modelbased rapid prototyping of ubiquitous environments might be used to avoid actual deployment while still enabling users to interact with a representation of the system. The paper describes APEX, a framework that brings together an existing 3D Application Server with CPN Tools. APEXbased prototypes enable users to navigate a virtual world simulation of the envisaged ubiquitous environment. The APEX architecture and the proposed CPNbased modelling approach are described. An example illustrates their use. 
Slides: HCSE2010_final.pdf 
Wed, September 8, 2010 at 09:00 
Fastest: a ModelBased Testing Tool for the Z Notation 
Maximiliano Cristiá (Universidad Nacional de Rosario, Argentina) 
Fastest is a modelbased testing tool for the Z formal notation providing an almost automatic implementation of the Test Template Framework. Z is one of the first and most studied industrialstrength formal methods to formally specify software systems. In this talk I will show how to use Fastest to automatically derive abstract test cases from a Z specification. 
Slides: tba 
Wed, June 16, 2010 at 10:00 
Matrices as Arrows! A Biproduct Approach to Typed Linear Algebra 
Hugo Macedo (MAPi PhD student) 
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an indexfree, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a typelevel perspective analogous to that of the pointfree algebra of programming. The derivation of fusion, cancellation and abide laws from the biproduct equations makes it easy to calculate algorithms implementing matrix multiplication, the kernel operation of matrix algebra, ranging from its divideandconquer version to the conventional, iterative one. From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered blockwise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given. 
Slides: read the homonym paper 
Wed, June 16, 2010 at 09:30 
Generic Pointfree Lenses 
Hugo Pacheco (MAPi PhD student) 
Lenses are one the most popular approaches to define bidirectional transformations between data models. A bidirectional transformation with "viewupdate", denoted a "lens", encompasses the definition of a forward transformation projecting "concrete models" into "abstract views", together with a backward transformation instructing how to translate an abstract view to an update over concrete models. In this presentation we show that most of the standard pointfree combinators can be lifted to lenses with suitable backward semantics, allowing us to use the pointfree style to define powerful bidirectional transformations by composition. We also demonstrate how to define generic lenses over arbitrary inductive data types by lifting standard recursion patterns, like folds or unfolds. To exemplify the power of this approach, we "lensify" some standard functions over naturals and lists, which are tricky to define directly "byhand" using explicit recursion. 
Slides: tba 
Wed, June 16, 2010 at 09:00 
The GUISurfer tool: towards a language independent approach to reverse engineering GUI code 
J. Carlos Silva (MAPi PhD student) 
Graphical user interfaces (GUIs) are critical components of today's software. Developers are dedicating a larger portion of code to implementing them. Given their increased importance, correctness of GUIs code is becoming essential. This talk describes the latest results in the development of GUISurfer, a tool to reverse engineer the GUI layer of interactive computing systems. The ultimate goal of the tool is to enable analysis of interactive system from source code. 
Slides: slides.pdf 
Wed, June 9, 2010 at 09:00 
Can we teach computers to generate fast OLAP code? 
Hugo Macedo (MAPi PhD student) and J.N. Oliveira 
Inspired by previous pointfree relational approaches to data processing, we investigate how the generation of pivot tables in data mining (such as those produced by Microsoft Excel) can be expressed using matrix multiplication and transposition. This generalizes relational projections and provides a linear algebra approach to FD detection and the drilldown/rollup operations typical of OLAP. In this context, the prospect of using SPIRAL to generate fast code for OLAP is envisaged. 
Slides: there is a technical note (version of July10th) about this talk 
Wed, May 19, 2010 at 09:00 
Formal analysis of user interfaces: state of the art and future prospects 
Michael Harrison (Newcastle University) 
This talk will give a (biased) survey of the use of mathematically based tools in the analysis of aspects of the user interface. It will discuss the role that these tools can play in improving interface design, how they complement more conventional HCI techniques and why their integration with existing techniques remains a future prospect. The talk will discuss future challenges and opportunities. Amongst these, scale and genericity, the prospects for tools that are accessible to HCI experts and the need for a common language will be a particular focus. 
Slides: braga2010.pdf 
Wed, April 07, 2010 at 09:00 
Taming Selective Strictness 
Daniel Seidel, Bonn University 
Free theorems establish interesting properties of parametrically polymorphic functions, solely from their types, and serve as a nice proof tool. For pure and lazy functional programming languages, they can be used with very few preconditions. Unfortunately, in the presence of selective strictness, as provided in languages like Haskell, their original strength is reduced. In this paper we present an approach for restrengthening them. By a refined type system which tracks the use of strict evaluation, we rule out unnecessary restrictions that otherwise emerge from the general suspicion that strict evaluation may be used at any point. Additionally, we provide an implemented algorithm determining all refined types for a given term. 
Slides: tamingSelectiveStrictness.pdf 
Wed, March 17, 2010 at 09:00 
A security types preserving compiler in Haskell 
Alberto Pardo, InCo, Universidad de La República, Uruguai 
We show the main aspects of a compiler, written in Haskell, which preserves the property of noninterference between a simple imperative language and structured machine code with loop and branch primitives. The compiler is based on the use of typed abstract syntax (represented in terms of GADTs and type families) both for the source and target language. In this case typed abstract syntax is used to model the type system for noninterference of each language where types correspond to security types. That way it is possible, on the one hand, to use Haskell's type checker to verify that programs enforce security restrictions, and on the other hand, verify that the compiler is correct (in the sense that preserves security restrictions) by construction. Joint work with Cecilia Manzino. 
Slides: UMinho0310.pdf 
Wed, November 25, 2010 at 10:00 
Program Repair as Sound Optimization of Broken Programs 
Tarmo Uustalu, Institute of Cybernetics, Tallinn University of Technology 
We present a new, semanticsbased approach to mechanical program repair where the intended meaning of broken programs (i.e., programs that may abort under a given, erroradmitting language semantics) can be defined by a special, errorcompensating semantics. Program repair can then become a compiletime, mechanical program transformation based on a program analysis. It turns a given program into one whose evaluations under the erroradmitting semantics agree with those of the given program under the errorcompensating semantics. We present the analysis and transformation as a type system with a transformation component, following the typesystematic approach to program optimization from our earlier work. The typesystematic method allows for simple soundness proofs of the repairs, based on a relational interpretation of the type system, as well as mechanical transformability of program correctness proofs between the Hoare logics for the errorcompensating and erroradmitting semantics. We first demonstrate our approach on the repair of filehandling programs with missing or superfluous open and close statements. Our framework shows that this repair is strikingly similar to partial redundancy elimination optimization commonly used by compilers. In a second example, we demonstrate the repair of programs operating a queue that can over and underflow, including mechanical transformation of program correctness proofs. (Joint work with Bernd Fischer, Ando Saabas.) 
Slides: uustaluminho251109.pdf 
Previous seminar series
See the past talks of FAST Seminar.
See the past talks of TFM Seminar.
See the past talks of PURé Café.
 JoseNunoOliveira  20 May 2010


Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors. Ideas, requests, problems regarding TWiki? Send feedback

