High-Assurance Software Laboratory



  • New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709–728, WSP Company. DOI: 10.1142/S0129054113400145
  • New Paper: H.D. Macedo and J.N. Oliveira. Typing Linear Algebra: a Biproduct-oriented Approach. SCP 78:11, pp.2160-2191 (DOI 10.1016/j.scico.2012.07.012)
  • New Paper: J.C. Campos and J. Machado, A Specification Patterns System for Discrete Event Systems Analysis, Int. J. Adv. Robotic Systems, vol. 10, 2013, doi:110.5772/56412
  • Job Opportunities: We are opening five post-doctoral positions. tinynew.gif Details here
  • New Paper: José N. Oliveira, Miguel A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15


DI » FMHAS » WebHome » Seminar

This page has been moved to the new HASLab web site at http://haslab.uminho.pt/calendar

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 software-intensive 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 cross-domain 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 network-centric 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 Just-In-Time Transaction Scheduling
Ana Nunes (HASLab)
Distributed transaction processing has benefited greatly from optimistic concurrency control protocols thus avoiding costly fine-grained 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 out-of-order execution.
Our evaluation using traces from the industry standard TPC-E 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

17th of April, 2013
Statically enforcing complex invariants in structured documents
Dario Teixeira
Lambdoc is an open-source library offering support for semantically rich structured documents in web applications [1]. It is particularly aimed at web sites that accept user-contributed 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

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 Cloud-enabled 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 TPC-C 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
"Point-free" Put-based 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 putback-based bidirectional language in which programmers write putback synchronization strategies from the start. In sharp contrast with traditional get-based languages, our putback-based 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 putback-based approach is central to specifying their non-trivial 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)
Large-scale distributed systems appear as the major infrastructures for supporting planet-scale services. These systems call for appropriate management mechanisms and protocols.
Slicing is an example of an autonomous, fully decentralized protocol suitable for large-scale environments. It aims at organizing the system into groups of nodes, called slices, according to an application-specific 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 non-uniform slices and to perform online and dynamic slices schema reconfiguration. Moreover, we describe how to provision a slice-local 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 large-scale 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 token-extraction 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 Least-change Lenses
Alcino Cunha (HASLab)
Non-trivial 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 (well-behaved) 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 state-based 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 least-change 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 QVT-R Bidirectional Model Transformations using Alloy
Nuno Macedo (HASLab)
QVT Relations (QVT-R) 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 QVT-R 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 meta-models (thus being prone to return ill-formed models), and none clearly formalizes how enforce semantics picks a target model from the myriad consistent candidates. In this paper we propose a QVT-R tool that overcomes all these issues: it supports a large subset of QVT-R 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 QVT-R 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 well-known object-relational mapping that illustrates OMG's QVT-R specification.
Keywords: QVT-R, 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 label-value pairs with a lookup operation that is linear-time in the number of fields. In this paper, we use type-level programming techniques to develop a more efficient 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 field 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 non-locality and quantum informatics
Rui Soares Barbosa (Department of Computer Science - University of Oxford)
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 higher-level data processing primitives in large scale data stores. The devised mechanisms should not hinder the scalability and dependability of large scale data stores. Regarding higher-level data processing primitives, this thesis explores two complementary approaches: extending data stores with additional operations such as general multi-item 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 so-called Linear Algebra of Programming (LAoP), an extension of the AoP towards quantitative reasoning. Simple examples (such as those given in eg. DOI: 10.1007/s00165-012-0240-9) show that faulty-program 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 component-oriented software systems modeled as co-algebras 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 safety-critical systems. One consequence of this is that interaction issues are almost entirely missing from international development standards in safety-critical 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 model-based 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 real-time systems properties
André Pedro
Real-time 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 real-time systems rather than for hard real-time 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 real-time 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 model-driven 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 web-based 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 domain-specific 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 Model-Driven 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. Model-Driven 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, Mode-driven 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.chi-med.ac.uk), where we integrate empirical approaches with mathematical methods to deliver a richer analysis of safety-critical 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 on-going work on the UNI-Pump 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 model-driven 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 UNI-Pump 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/masci-QMpreprints
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 language-based 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 domain-specific 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 sub-routine. 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 parameter-free 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 object-relational 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 re-evaluate 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, model-based 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 system-wide 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 fault-tolerance and support to churn. This study details a novel distributed aggregation approach, named Flow Updating, which is fault-tolerant 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 self-adapts 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, Fault-tolerance
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.

8th of February, 2012
Every transformation is a lens: Taming partiality using invariants and non-determinism
Nuno Macedo (HASLab)
Total well-behaved 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 round-tripping laws, opening the door to unpredictable synchronization behaviors. We propose a framework where any transformation written in a point-free functional language can be lifted to a total well-behaved 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 non-deterministic execution of backward transformations. Both these and the data invariants are naturally specified using a point-free relational calculus that enables concise and agile algebraic reasoning.
Keywords: Bidirectional transformations, Point-free relational calculus, Data invariants, Non-determinism
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 public-key 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 one-time 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, Public-key cryptography, Provable security
Slides: tba

11th of January, 2012
Implementing sound in a CAVE-like 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 CAVE-like 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
Fault-Tolerant Aggregation: Flow-Updating Meets Mass-Distribution
Carlos Baquero (HASLab)
Flow-Updating (FU) is a fault-tolerant 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 Mass-Distribution (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 Mass-Distribution with Flow-Updating (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 FU-based 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 message-loss rate, we adjust the accuracy of MDFU heuristically in a new protocol called MDFU with Linear Prediction (MDFU-LP). The evaluation shows that both MDFU and MDFU-LP 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)
Model-Driven 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 UML-based 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 whole-cell 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 tool-supported 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 Key-Value 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 aplicando-o 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 Two-Squares Theorem
João Ferreira (University of Teesside, UK, and HASLab)
I show a new and constructive proof of the two-squares theorem, based on a somewhat unusual but very effective, way of rewriting the so-called extended Euclid's algorithm. Rather than simply verifying the result---as it is usually done in the mathematical community---I 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 model-based spreadsheet evolution system
Jácome Cunha/Jorge Mendes (HASLab)
This paper describes the embedding of ClassSheet models in spreadsheet systems. ClassSheet models are well-known 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 model-driven 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 model-driven spreadsheet engineering environment.
Slides (pdf)

19th of October, 2011
WHISPER: Middleware for Confidential Communication in Large-Scale 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 large-scale 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 multi-hops 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 real-world 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 case-study. The approach is based on a methodology which enables semi-automatic 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 graph-based models of system structure. The approaches encompass specification, reverse engineering of running systems, and analysis of the models for HCI-relevant 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 topic-based publish/subscribe
Miguel Matos (HASLab)
Topic-based 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 topic-based 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
Benchmark-based 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 two-stage process to aggregate metrics, first to risk profiles and afterwards to ratings. A rating summarizes a metric at system-level, allowing it to compare and evaluate a software. Thresholds also allow to drill down from ratings to measurements, enabling root-cause analysis. We explain the methodologies to derive thresholds from benchmark data and their role in the SIG quality model. Finally, using two space-domain 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) statistics-based approaches, and (2) reasoning approaches. Statistics-based 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, model-based 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, low-cost, Bayesian reasoning approach to spectrum-based 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 well-known benchmark programs, but also experiments on the Philips TV software) show that Barinel outperforms other state-of-the-art 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, trade-offs 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 trade-offs (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 safety-critical 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 pre-defined 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 run-time 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 model-based 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 on-line analytical processing (OLAP) and data mining can be expressed in terms of matrix multiplication, transposition and the Khatri-Rao matrix product, a variant of the Kronecker product. This offers much potential for parallel OLAP, as such matrix operations have a well-defined parallelization theory. We propose a simple roadmap for parallel OLAP based on a separation of concerns: rather than depending on SQL-querying 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 well-established, 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 data-centric 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 p-value. We estimate the expected frequency of a motif by using Markov Chain models. The p-value 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 off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive low-level optimisations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. We apply state-of-the art deductive verification tools to check security-relevant 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 semi-automation of requirement analysis in requirements engineering. Prospect of enriching such methodologies with formal methods support.
Slides: tba

Wed, November 10th, 2010 at 09:15
A Engenharia de Software e o Projeto do Veículo Lançador de Satélites VLS-1
Carlos Lahoz (Instituto de Aeronáutica e Espaço, Brasil)
No abstract provided
Slides: tba

Wed, 3rd of November 2010, at 9:00 (DI-A2)
Calculating (Haskell) programs from Galois connections
J.N. Oliveira (HASLab); joint work with Shin-Cheng 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 non-deterministic, inductive specifications (vulg. "relational (un)folds"). This includes the elegant re-factoring of two results by Bird-de 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 (DI-A2)
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 model-based 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. APEX-based prototypes enable users to navigate a virtual world simulation of the envisaged ubiquitous environment. The APEX architecture and the proposed CPN-based modelling approach are described. An example illustrates their use.
Slides: HCSE2010_final.pdf

Wed, September 8, 2010 at 09:00
Fastest: a Model-Based Testing Tool for the Z Notation
Maximiliano Cristiá (Universidad Nacional de Rosario, Argentina)
Fastest is a model-based 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 industrial-strength 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 index-free, 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 type-level 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 divide-and-conquer version to the conventional, iterative one. From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise 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 Point-free Lenses
Hugo Pacheco (MAPi PhD student)
Lenses are one the most popular approaches to define bidirectional transformations between data models. A bidirectional transformation with "view-update", 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 point-free combinators can be lifted to lenses with suitable backward semantics, allowing us to use the point-free 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 "by-hand" 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 drill-down/roll-up operations typical of OLAP. In this context, the prospect of using SPIRAL to generate fast code for OLAP is envisaged.
Slides: there is a tinynew.gif technical note (version of July-10th) 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, semantics-based approach to mechanical program repair where the intended meaning of broken programs (i.e., programs that may abort under a given, error-admitting language semantics) can be defined by a special, error-compensating semantics. Program repair can then become a compile-time, mechanical program transformation based on a program analysis. It turns a given program into one whose evaluations under the error-admitting semantics agree with those of the given program under the error-compensating semantics. We present the analysis and transformation as a type system with a transformation component, following the type-systematic approach to program optimization from our earlier work. The type-systematic 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 error-compensating and error-admitting semantics. We first demonstrate our approach on the repair of file-handling 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: uustalu-minho-251109.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

r199 - 15 Jan 2014 - 17:25:50 - JacomeCunha
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