Master courses in Computer science at Minho University are built upon the concept of specialisation course.
Each of these corresponds to a half-time academic year, and are focused on a particular applicational area of computer science. Moreover, they incorporate an important project component, where the student must incorporate all the necessary skills.
FAST group members are involved in the following courses:
MOMPES 2008 - Model-based Methodologies for Pervasive and Embedded Software
MOMPES (Model-based Methodologies for Pervasive and Embedded Software) workshop series focuses on the scientific and practical aspects related with the adoption of MDA and other MBD methodologies (notation, process, methods, and tools) for supporting the construction of computer-based systems, and more specifically, pervasive and embedded software.
The 5th edition of this wrokshop will be organized within ETAPS 2008 (11th European Joint Conferences on Theory and Practice of Software), Budapest, Hungary, April 5, 2008.
A Interacção 2008 – 3ª Conferência Interacção Pessoa-Máquina – realiza-se na Universidade de Évora, de 15 a 17 de Outubro de 2008, e visa reunir investigadores, docentes e profissionais das diversas áreas envolvidas, promovendo a partilha de conhecimentos e pontos de vista sobre a Interacção Pessoa-Máquina em Portugal.
Past Events
XATA 2008 - 6th national conference of XML: Applications and Technologies. Évora, 14,15 February 2008.
CIC 2007 - Research Workshop on Coinduction, Interaction and Composition.
GTTSE'07 - Summer School on Generative and Transformational Techniques in Software Engineering, 2007.
ETAPS'07 - European Joint Conferences on Theory and Practice of Software, 2007
New Project: FAST members participate in EFACEC's InPACT project.
FAST members J.C. Campos and P.R. Henriques will be cooperating with EFACEC over the next two years in its, QREN funded, InPACT project (Integrated Engineering Tools for Protection, Automation and Control Systems).
Sep 08, 2008 11:59 PM
Co-chair: J. C. Campos was designated co-chair of the programme committee of INTERACÇÃO'08.
The conference will be held in Évora, 15-17 October 2008.
Oct 12, 2007 2:08 PM
New Paper: Simulation and Formal Verification of Industrial Systems Controllers
J. Machado and E. Seabra and J.C. Campos and F. Soares and C.P. Leao and J.F. Silva (forthcoming) In 19th International Congress of Mechanical Engineering (COBEM 2007).
Oct 12, 2007 1:40 AM
New Paper: Formal analysis of interactive systems: opportunities and weaknesses
M. D. Harrison and J. C. Campos and K. Loer (forthcoming) In P. Cairns and A. Cox, editors, Research Methods in Human Computer Interaction. Cambridge University Press.
Oct 12, 2007 1:39 AM
New Paper: Connecting rigorous system analysis to experience centred design
(download from RepositoriUM? )
M. D. Harrison and J. C. Campos and G. Doherty and K. Loer (forthcoming) In E. Law and E. Hvannberg and G. Cockton and J. Vanderdonckt, editors, Maturing Usability: Quality in Software, Interaction and Value, Human-Computer Interaction Series. Springer. (ISSN: 1571-5035; ISBN: 978-1-84628-940-8)
Oct 12, 2007 1:39 AM
New Paper: A New Plant Modelling Approach For Formal Verification Purposes
J. Machado and E. Seabra and F. Soares and J. Campos (forthcoming) In 11th IFAC Symposium on Large Scale Systems 2007. Elsevier.
New Paper: Considering context and users in interactive systems analysis
J.C. Campos and M.D. Harrison (forthcoming) In Engineering Interactive Systems 2007, Lecture Notes in Computer Science. Springer-Verlag.
New Paper: An Interaction Model and Infrastructure for Localized Activities in Pervasive Computing Environments
H. Pinto and R. José and J. C. Campos (2007) In IEEE International Conference on Pervasive Services 2007 (ICPS'07), pages 232-241. IEEE Computer Society Press. (ar: 18/64 ~.28)
NewPaper: Model-based user interface testing with Spec Explorer and ConcurTaskTrees?
J. L. Silva and J. C. Campos and A. Paiva (2007) In Paul Curzon and Antonio Cerone, editors, The Pre-proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems (FMIS 2007), pages 116-133. (to appear in ENTCS, Springer - ar: 7/18 ~.39)
New Paper: Exploring an option space to engineer a ubiquitous computing system
M. Harrison and C. Kray and J. C. Campos (2007) In Paul Curzon and Antonio Cerone, editors, The Pre-proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems (FMIS 2007), pages 67-82. (to appear in ENTCS, Springer - ar: 7/18 ~.39)
New Paper: Exploring an option space to engineer a ubiquitous computing system
M. Harrison and C. Kray and J. C. Campos (2007) In Paul Curzon and Antonio Cerone, editors, The Pre-proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems (FMIS 2007), pages 67-82. (to appear in ENTCS, Springer - ar: 7/18 ~.39)
New Paper: Integrating HCI into a Software Engineering course
A.N. Ribeiro and J.C. Campos and F.M. Martins (2007) In Pre-proceedings HCI Educators 2007.
New Paper: Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications
J. C. Silva and J. C. Campos and J. Saraiva (2007) In G. Doherty and A. Blandford, editors, Interactive Systems: Design, Specification and Verification, volume 4323 of Lecture Notes in Computer Science, pages 137-150. Springer-Verlag.
New Paper: Paper Coupled Schema Transformation and Data Conversion For XML and SQL (by Pablo Berdaguer, Alcino Cunha, Hugo Pacheco, and Joost Visser) accepted by PADL 2007 (Nice, France).
Oct 5, 2006 4:21 PM
New Paper: Paper Strongly Typed Rewriting For Coupled Software Transformation (by AlcinoCunha? and Joost Visser) accepted by RULE 2006 (Seattle, USA).
Sep 25, 2006 11:42 AM
New Paper: Paper Strong Types for Relational Databases by Alexandra Silva and Joost Visser has been accepted for the Haskell Workshop 2006 (Portland, USA).
Sep 25, 2006 11:42 AM
New Paper: Paper Configurations of Web Services by MarcoAntonioBarbosa? and LuisSoaresBarbosa? has been accepted for FOCLASA'06 (Bonn, Germany).
Sep 25, 2006 11:41 AM
New Paper: Paper Towards a Coordination Model for Interactive Systems by MarcoAntonioBarbosa? , JoseCampos? and LuisSoaresBarbosa? has been accepted for FMIS'06 (Macau).
Sep 25, 2006 11:40 AM
The Computer Science and Technology Center (Centro de Ciências e Tecnologias de Computação, CCTC) invites applications for a 3 year research position in the area of Software Foundations. Specific expertise is sought in applied semantics, software analysis and transformation, formal verification, provable security and theory of programming languages as well as eager interest in formal foundations and a strong aptitude for projects with real-world potential. (Application deadline: 30-09-2008; more information).
InPACT: Integrated Engineering Tools for Protection, Automation and Control Systems
O projecto InPACT é um projecto de II&DT com vista ao desenvolvimento de ferramentas de engenharia
avançadas para aplicação a sistemas de protecção, automação e controlo (PAC) de sistemas eléctricos de
energia. Nestes sistemas incluem-se os domínios (i) da automação de subestações (SAS), (ii) comando e
controlo de centrais electroprodutoras, (iii) automação de redes de distribuição e (iv) sistemas afins.
O projecto tem enfoque particular no SAS e em tecnologia de automação distribuída com base em normas
internacionais aplicáveis, nomeadamente a IEC 61850 e normalização internacional associada e a IEC 61131-3,
não deixando de abranger conceitos mais recentes como aqueles incluídos na série de normas IEC 61499 ou
abordar outras tecnologias comunicativas de segunda geração como aquelas baseadas na série de normas IEC
60870-5.
A Universidade do Minho traz ao projecto competências nas áreas de investigação científica,
análise e desenho de soluções nos domínios genéricos de aplicações informáticas e, em particular, nos domínios específicos da interface ao utilizador, edição diagramática, compiladores de linguagens, linguagens
visuais e validação de comportamento.
Jul/2008-Jun/2010
Funded by EFACEC and QREN
Partners: EFACEC, U.Minho, EDP.
Budget: 81K¤ (UMinho budget)
The goal of this project is to design, develop and deploy a toolbox that will support the specific domain of cryptographic software engineering. Ordinarily, development of cryptographic software is a huge challenge:security and trust is mission critical and modern applications processing sensitive data typically require the deployment of sophisticated cryptographic techniques. The proposed toolbox will allow non-experts to develop high-level cryptographic applications and business models by means of cryptography-aware high-level programming languages and compilers. The description of such applications in this way will allow automatic analysis and transformation of cryptographic software to detect security critical implementation failures, e.g., software and hardware based side-channel attacks, when realizing low level cryptographic primitives and protocols.
CACE is an FP7 project funded by the European Union.
CACE will start beginning of 2008 and run for 3 years.
This project aims at providing innovative, efficient and expressive mechanisms for the secure implementation and execution of code, with an emphasis on problems posed by embedded systems.
Rescue is a 3 year project, funded by FCT under contract PTDC/EIA/65862/2006.
Starting date: January 2008.
AMADEUS: Aspects and Compiler Optimizations for Matlab System Development
This project addresses the enrichment of MATLAB with aspect-oriented extensions to include additional information (e.g., type and shape of variables) and to experiment different implementation features (e.g., different implementations for the same function, certain type binding for variables, etc.). The proposed aspects aim to configure the low-level data representation of real variables and expressions, to specifically-tailored data representations that benefit from a more efficient support by target computing engines (e.g., fixed- instead of floating-point representations). The approach also aims to help developers to introduce handlers (code triggered when certain conditions may occur and with a richer functionality than assertions) and monitoring features, and to configure function implementations. We believe aspect-oriented extensions will help system modelling, simulation, and exploration of features conceiving system implementation. One of the advantages is related to the fact that a single version of the specification can be used throughout the entire development cycle rather than maintaining multiple versions, as is currently the case.
Nov/2007-Oct/2009
Funded by FCT (PTDC/EIA/70271/2006)
Partners: Inesc-ID, U.Minho, Uninova, Deimos.
Budget: 106K¤
IVY's goal is to develop a model based tool for the analysis of interactive systems designs. The tool will act as a front end to the SMV model checker, creating an abstraction layer where models of interactive systems can be developed and analysed.
Language Engineering and Rigorous Software Development is an ALFA project (Latin America Academic Training ) funded by the European Comission.
Project partners are the Universities of Minho (coordinator), Utrecht, Chalmers, INRIA, Politécnica de Valência, Castilla-La Mancha, La República, EAFIT, Nacional de San Luís, Federal de Minas Gerais, Católica de Santiago del Estero.
The project will fund a total of 27 PhD students co-tutored by a Latin-American and an European institution. Total funding: approx. 530.000¤. Current state: 8 PhD students have started their work.
Additionally the project will set up a research network in the areas of Programming Languages and Rigorous Software Construction.
The Types project is a coordination action in EU′s 6th. framework programme. It started in September 2004 and is a continuation of a number of successful European projects.
Maria João Frade is associated to this project.
GRICES-00342
Technological and Scientific Cooperation Project between Portugal and the P. R. of China on Formal Foundations for Component-based Programming
A Iberoamerican network of experts in Software Verification and Validation. Funded by CYTED. Started 01/2007, runs for 3 years. J. F. Campos and J. B. Almeida are members.
SOFTAS: Software Development with Aspects
This project aims at inventing a seamless AOSD process by focusing on the definition of a complete software methodology covering all the development stages, so that crosscutting and non-crosscutting concerns can be traced during the lifecycle to produce efficient and high-quality software applications. The research results will be instantiated in practice with real world examples from industry.
In summary, the two main objectives of the project are:
to propose a modelling and architecture design framework, which includes a methodology and tools to help the development of software applications that can take advantage of the principles of aspect-orientation;
to derive quantitative evidence on the improvement on the modularity of produced software and other quality attributes.
Sep/2005-Dec/2007
Funded by FCT (POSC/EIA/60189/2004)
Partners: FCT-UNL, U.Minho, IP Beja, LINCIS, NAV.
Budget: FCT: 89K¤
The following research challenges have been targetted in recent work:
How to model, design and reason rigorously about highly complex software systems (including forms of composition, coordination, interaction and deployment)?
How to derive correct software from abstract models (oriented to critical aspects of system's design such as eg, functionality, security, data quality and usability)?
How to reconstruct abstract models from the real world (including legacy software and incomplete or inconsistent data sources)?
The talk is very much work in progress. During the last few months I have been exploring models of a simple ubiquitous system to explore plausible operator behaviours. The first model, developed in UPPAAL, includes simple timing constraints driven by the process that a mobile device is intended to control. The second PROMELA model describes the same system but also makes explicit the information resources that would be used by the operator to control the plant. The talk will mainly focus on the PROMELA model. However I aim to discuss why the UPPAAL model was easier to construct and (at a simple level) to analyse, and to raise preliminary questions about time aspects of the model.
Keiko Nakata (Institute of Cybernetics, Tallinn University of Technology)
Wed, 17 Jun, 2009 at 11:30
In our previous work we have studied several coinductive operational semantics, all of which are proved equivalent, for the While language to describe terminating as well as non-terminating program executions. The operational semantics keep track of all the intermediate states that an execution goes through as a trace (a sequence of states). The trace is finite for a terminating execution and infinite for a non-terminating execution. In this talk I present a Hoare-logic for While, which is proved sound and complete with respect to those operational semantics. As usual, our Hoare-triple consists of a precondition, a statement and a postcondition. The precondition is a predicate on initial states, whereas the postcondition is a predicate on traces. Since a trace contains the full information about an execution, the logic can talk about for instance if an execution is terminating or if an variable is updated infinitely often. My talk will start by introducing a coinductive big-step relational semantics, then present the Hoare-logic. I will explain some interesting design issues on the logic and our strategy for proving its completeness, that we have discovered through many failed attempts. All the results have been formalized in Coq.
O objectivo da integração de sistemas de informação consiste na união de serviços e informações de diversos sub-sistemas independentes, por forma a obter uma solução única, coerente e integrada. Por outro lado, os modelos e linguagens de coordenação têm como principal objectivo especificar e raciocinar sobre configurações de cooperação entre entidades computacionais distintas e independentes. Apesar das diferenças fundamentais na forma com atacam os seus problemas específicos, a aplicação dos modelos e linguagens de coordenação à integração de sistemas de informação parece um exercício imediato e com enormes vantagens para o sucesso de projectos de integração de software. No entanto, esta relação encontra-se extremamente mal explorada, com a excepção de casos pontuais do uso de modelos de orquestração e coreografia. Nesta apresentação apresentar-se-á um conjunto de estilos de integração de sistemas de informação, tendo como preocupação explorar novas aplicações dos modelos de coordenação a cada estilo de integração introduzido. Para além de apresentar os estilos de integração de forma clara e independente de tecnologias específicas, é ainda apresentada uma organização comparativa dos estilos de integração.
The advent of On-Chip parallelism poses a dreadful obstacle to current mature programming languages. Traditional approaches based on compiler or hand-coded optimizations are giving place to trendy generative techniques, based on DSL and ad-hoc program transformation frameworks. In this talk we will report on our first steps in the attempt to lay the common (categorical) semantics of a particular class of DSL addressing numerical programming under the motto "matrices as arrows!" We will shift the traditional view of matrices as indexed structures to an index-free representation, analogous to point-free program transformation.
Miriam Alves (Instituto de Aeronáutica - IAE, Brasil)
Wed, 04 Feb, 2009 at 14:00
Esta apresentação abordará, de forma sucinta, as principais atividades do Instituto de Aeronáutica e Espaço (IAE - Brasil)- relacionadas aos Projetos de Veículos Lançadores de Satélites, com ênfase no desenvolvimento, validação e verificação tanto do software embarcado nestes veículos como nos sistemas de software de apoio de solo para a realização das missões de lançamento. Considerando a importância e o aspecto crítico destes sistemas de software, serão apresentadas as iniciativas mais recentes do grupo de software do IAE para a melhoria do processo de desenvolvimento e da abordagem de verificação e validação.
In this talk we will discuss the generation of visual programming environments in an automatic way, from the formal specification of the underlying language. An automatic visual environment generator, named DEViL? , is the base of the discussion. DEViL? generates visual programming environments with integration of graphical editors, compilers, translators and several others tools, from attribute grammars for visual-languages. A running example, VisualLISA? , is used to present the workflow to generate a visual programming environment. VisualLISA? is a visual editor for Attribute Grammar (AG) specifications. This editor is generated from a specification of a visual-language that enables us to draw, syntactically and semantically correct, attribute grammars. The visual specification of an AG is production-oriented and incremental. The editor translates the drawn attribute grammar directly into LISA notation or alternatively into a universal XML representation designed to support different AG-based compiler generators.
This talk discusses the development of the GUISurfer tool. GUISurfer is focused on extracting and testing behavioural models from Graphical User Interface (GUI) source code. We present a generic model for language independent reverse engineering of GUI-based applications, and we explore the integration of model-based testing techniques in our approach, thus allowing us to perform fault detection. First we describe our library for GUI models extraction and manipulation. And finally we show how these models can be use to reason about the user interface and generate test cases for automatic GUI testing.
This Ph.D. work, in the general context of Software Engineering, is concerned with software systems' maintenance (systems that may contain millions of lines of code). Namely, the work will be oriented to applications (may be web applications) developed under multi-language Integrated Development Environments (IDEs), where many languages and technologies can be smoothly combined due to the existence of a common language runtime. Maintenance requires the comprehension of the overall system, as well as, the full understanding of each component (a program). Many times, the first task performed to do maintenance is the backward analysis of the system (from code to model), known as the reverse engineering process. Program Comprehension, Program Understanding, and Reverse Engineering activities depend on the so-called program analysis, among other technologies; many times it is important to constrict the program analysis to a program slice to focus only on those statements that are responsible for some state. Maintenance, code re-use, and systems' re-engineering require, as told above, quantifiable methods. That approach implies the definition and use of software metrics. But the complexity of data resulting from program analysis, or even from the metrics evaluation process, demands the resort to high-quality graphical interfaces to help the user to understand and navigate over the imbricated data. So, software visualization is another discipline involved in a systematic, disciplined, quantifiable approach to software maintenance. This contextualization let us understand that the background for the present work requires the study of: code analysis, slicing, metrics, and visualization. Because program verification is nowadays a relevant issue in this area of software engineering, it was decided to include another topic: proof carrying code (PCC). A lot of work has been done in the past in code analysis to help in the various tasks of software re-engineering and maintenance, including program comprehension activities. Many good results have been reached. However in the multi-language multi-technology platform that will be considered, there is still need for a system that can handle programs at different levels of encoding. The aim of this Ph.D. work is to investigate efficient methods, techniques and tools to analyze source (high-level), intermediate (abstract middle-level) or target (low-level/machine) code, under the same environment, in order to extract static and dynamic information that can be visualized in a uniform way (independent of the analysis level) to help in program maintenance---the analysis, comprehension, and verification of a program. The focus of this talk will be the general overview of the Ph.D. project, and a synthesis of the state-of-the-art concerning Program Analysis and Program Slicing.
This paper presents techniques and tools to transform spreadsheets into relational databases and back. A set of data refinement rules is introduced to map a tabular datatype into a relational database schema. Having expressed the transformation of the two data models as data refinements, we obtain for free the functions that migrate the data. We use well-known relational database techniques to optimize and query the data. Because data refinements define bidirectional transformations we can map such database back to an optimized spreadsheet. We have implemented the data refinement rules and we constructed Haskell-based tools to manipulate, optimize and refactor Excel-like spreadsheets.
Context-aware applications pose new usability challenges that cut across the phases of design and development. They provide richer interaction taking context into account. They are difficult to build due to their distributed nature. This talk presents a technical literature review about modelling and simulating virtual environments, with a focus in context-aware applications. Relevant work in this area is discussed and compared through a case study. A first attempt to introducing context into some of the existing modelling approaches is described. Areas that require more work, and that we will possibly follow, are referenced.
In recent years, advances in software tools have made it easier to analyze interactive system specifications, and allow the analyst to consider a wide range of possible behaviors. However, the effort involved in producing the specifications of the system is still substantial, and a difficulty exists regarding the specification of plausible behaviors on the part of the user. Recent trends in technology towards more mobile and distributed systems further exacerbates the issue, as contextual factors come in to play, and less structured, more opportunistic behavior on the part of the user makes purely task-based analysis difficult. In this paper we consider a resourced action approach to specification and analysis. In pursuing this approach we have two aims - firstly, to facilitate a resource-based analysis of user activity, allowing resources to be distributed across a number of artifacts, and secondly to consider within the analysis a wider range of plausible and opportunistic user behaviors without a heavy specification overhead, or requiring commitment to detailed user models.
It is difficult to construct correct models for distributed large-scale service-oriented applications. Typically, the behavior of such applications emerge from interaction and collaboration of multiple components/services. On the other hand, each component, in general, takes part in multiple scenarios. Consequently, not only components, but also their interaction protocols are important in the development process for distributed systems. Coordination models and languages, like Reo, offer powerful ``glue-code'' that encode the interaction protocols. In this work we propose a novel synthesis technique, which can be used to generate Reo circuits directly from scenario specifications. Inspired by the way UML2.0 sequence diagrams can be algebraically composed, we define an algebraic framework for merging connectors generated from partial specifications by exploiting the algebraic structure of UML sequence diagrams.
Floyd-Hoare Logic stands at the heart of the science of Computer Programming, and has been used extensively in both formal software development and program verification. In this talk we review different methods for generating verification conditions for a given specification, and show how they are derived from Hoare's standard inference system. We discuss methods based on program annotations, weakest preconditions, and updates, and present examples of program verification systems based on each of these.
Schema transformations occur in several contexts. Examples are software evolution, refactoring and cross-paradigm mapping (e.g. VDM to SQL transformation). When initial schemas are annotated with contraints, these contraints must be preserved in the target schema. Moreover, during the transformation process, when high-level data structures are refined, new constraints can be added for semantic preservation (e.g. referential integrity). We intend to present a possible solution, using an algebraic approach that is constraint-aware, in the sense that existent contraints are preserved and new contraints are added when necessary. This solution is based on refinement theory and point-free program transformation.
Zoltán Porkolab (Eötvös Loránd University, Budapest)
Wed, 09 Jan, 2008 at 14:00
The C++ and Java programming languages are considered as object-oriented languages. However, both have strong features for generative programming: the C++ templates and the Java generics. Those generative programming facilities make it possible to write abstract data structures and generic algorithms. Moreover C++ templates form a Turing-complete sublanguage of C++, so one can write programs "running" in the compilation time. Template metaprogramming is an emerging new direction in C++ programming for executing algorithms in compilation time. This one time theoretical possibility today became a strong industrial tool widely used in various libraries and applications. In this talk we review the possible fields of application of C++ template metaprogramming, and emphasize its unique advantages.
Analytic usability analysis methods have been proposed as an alternative to user testing in early phases of development due to the cost of the latter approach. By working with models of the systems, analytic models are not capable of identifying implementation related problems that might have an impact on usability. Model-based testing enables the testing of an implemented software artefact against a model of what it should be (the oracle). In the case of model-based user interface testing, a main issue is the use of oracles at an adequate level of abstraction. This talk discusses the findings of an effort to use task models as oracles for model-based testing of user interfaces.
A two-level data transformation system. 2LT is a deliverable of the
PURe project. Examples of application include XML schema evolution coupled
with document migration, and data mappings between VDM abstract models and
SQL.
A Portuguese talking browser is the final product of this project. The application aims at minimizing the scanning time of a web page thus enabling a talking browser to read a web site at a speed comparable to that of a sighted user.
A model based tool for the analysis of interactive systems' designs. The tool acts as a front end to the NuSMV model checker, creating an abstraction layer where models of interactive systems can be developed and analysed. IVY uses a plugin approach enabling for easy integration of new components. Current components include: a text and graphical editor of MAL interactors (the IVY workbench modelling language), a property patterns tool (under development), a compiler from MAL interactors to NuSMV, and a trace visualiser . All components are integrated via IPF (the interactor plugin framework).
An open-source morphological analyzer. Mainly developed for Portuguese,
it includes dictionaries for English and Latin. It is being used to create
spelling dictionaries of several open-source projects, e.g. aspell, Firefox
and Thunderbird dictionaries.
A Topic Maps Builder (Oveia), Validator (Tche), and Navigator (Ulisses): A XML generic platform for TM specification (syntax+semantics), construction (enabling data extraction from heterogenous information resources), validation (according to a constraint spec), storage (XTM-format or Database), and navigation (conceptual browsing).
An open-source workbench for parallel corpora processing. Among
other tools, this includes a sentence aligner and a Probabilistic Translation
Dictionary extractor, plus a word aligner.
A web-based Information System to support the Prosopographic study of portuguese medieval priests, in the context of the "Fasti Ecclesiae Portugaliae".
The UMinho Haskell Libraries are located in the libraries subdirectory. The modules included in the libraries cover a wide range of functionality, for instance: representation and operations on relations and graphs; analysis and manipulation of spreadsheets and Java programs; support for pointfree programming; support for VDM like concepts (such as data type invariants, pre and post-conditions).
Several tools are included in the UMS distributions, among which: DrHylo (Derives hylomorphisms from restricted Haskell syntax), ChopaChops (Graph slicing and chopping), HaGLR (Generalized LR parsing), SdfMetz (An SDF monitoring tool), Camila (Prototype Camila interpreter), VooDooM (Transforms VDM datatypes to a relational representation).
InPACT
O projecto InPACT (Integrated Engineering Tools for Protection, Automation and Control Systems) é liderado pela EFACEC e acaba de obter financiamento do QREN. Outros parceiros são a Universidade do Minho (via DI e CCG) e a EDP Distribuição.
Com o InPACT a EFECEC visa o desenvolvimento e introdução de uma nova linha de ferramentas de engenharia avançadas na sua gama de produto para o sector de actividade de automação, protecção e controlo de sistemas de energia ou similares.
A Universidade do Minho, através do DI e CCG, traz ao projecto competências nas áreas de investigação científica, análise e desenho de soluções nos domínios genéricos de aplicações informáticas e, em particular, nos domínios específicos da interface com o utilizador, edição diagramática, compiladores de linguagens, linguagens visuais e validação de comportamento.
No contexto do InPACT estão disponíveis dois projectos de mestrado na área do desenvolvimento de editores avançados de diagramas. Existes financiamento para estes projectos:
a) Desenvolvimento de um editor de sinópticos (representações do processo controlado 2D vectoriais dinâmicas e interactivas) executável em múltiplas plataformas (web, dispositivo embebido e desktop).
b) Desenvolvimento de um editor diagramático configurável para diferentes linguagens gráficas.
-- JoseCampos - 08 Sep 2008
PROPONENTES:
Carlos Bacelar Almeida / Manuel Alcino Cunha
DESCRIÇÃO:
A linguagem CALF está a ser desenvolvida no âmbito do projecto europeu CACE. Trata-se de uma linguagem de domínio específico para o desenvolvimento de aplicações criptográficas que concilia, por um lado, abstracções poderosas ao nível do sistema de tipos (e.g. tipos parametrizados por valores) e, por outro, matém presente preocupações relativas à eficiência do código resultante.
O tema proposto é o desenvolvimento de um interpretador e de um mini-compilador para essa linguagem.
análise sintáctica do código fonte;
verificação/inferência de tipos;
codificação de uma "shell" que permita o teste rápido de programas;
tradutor da representação interna para código C++ (fazendo uso da biblioteca NTL)
Recomenda-se a utilização de uma linguagem funcional na realização do projecto (e.g. Haskell ou OCaml).
Esta proposta enquadra-se no projecto FP7 CACE.
INFORMAÇÃO ADICIONAL:
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Gerador de Condições de Verificação
ÁREA CIENTÍFICA:
Program Verification
LOGICS AND MEANINGS OF PROGRAMS
PROPONENTES:
Jorge Sousa Pinto / Carlos Bacelar Almeida
DESCRIÇÃO:
As abordagens recentes à verificação de programas envolvem duas componentes:
a utilização de um demonstrador de teoremas (automático ou interactivo);
uma aplicação designada por "Gerador de Condições de Verificação" (VCGen).
A ideia é que o VCGen transforma um programa (anotado com a respectiva especificação) num conjunto de "obrigações de prova" de primeira ordem que possam ser verificadas pelo demonstrador de teoremas considerado. O VCGen é "correcto" na medida em que, se todas as obrigações de prova se verificarem, existe garantia que o programa se encontra "conforme" a especificação apresentada.
O objectivo deste projecto é o de implementar um VCGen para uma linguagem imperativa "C-like". Pretende-se que esse VCGen seja modular, na medida em que diferentes características da linguagem (e.g. utilização de "arrays"; memória dinâmica; etc.) sejam consideradas incrementalmente.
Esta proposta enquadra-se no projecto FCT Rescue e no projecto FP7 CACE.
INFORMAÇÃO ADICIONAL:
Está aberto um concurso para uma bolsa de investigação do projecto Rescue em que este tema se enquadra. Recomenda-se assim que potenciais interessados submetam a respectiva candidatura (mais informações em http://www.eracareers.pt/opportunities/index.aspx?task=global&jobId=11685).
Descrição detalhada: VCGen.pdf
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Computação Multipartida Segura do Logaritmo
ÁREA CIENTÍFICA:
SECURITY AND PROTECTION
Distributed Systems
PROPONENTES:
Carlos Bacelar Almeida
DESCRIÇÃO:
Em "Computação Multipartida Segura" (SMC) existem várias partes que pretendem contribuir com dados para uma dada computação (e.g. alguma estatística sobre a agregação desses dados), mas com garantias que a confidencialidade desses dados não é comprometida. Um domínio onde essas técnicas encontram aplicação é o da "Mineração de Dados com Preservação de Privacidade" (PPDM) - nesse caso cada uma das partes contribui com a sua Base de Dados para uma dada técnica de Mineração de Dados, tendo garantias que as outras partes não obtém qualquer conhecimento desses dados (para além do resultado da técnica executada).
O objectivo deste projecto é a codificação de um algoritmo SMC específico: o cálculo do logaritmo. Esse algoritmo é uma peça fundamental numa grande quantidade de técnicas PPDM, e constitui por si só um excelente exemplo combinação de técnicas específicas de SMC (avaliação segura de circuitos; partilha de segredos; etc.). Pretende-se assim utilizar a codificação do algoritmo proposto como pretexto para apresentar o domínio da SMC.
Linguagens de programação a utilizar: C/C++, Java.
INFORMAÇÃO ADICIONAL:
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Correcção perante implementação de referência
ÁREA CIENTÍFICA:
Program Verification
LOGICS AND MEANINGS OF PROGRAMS
PROPONENTES:
Jorge Sousa Pinto / Carlos Bacelar Almeida
DESCRIÇÃO:
Para se aferir a correcção de um programa é necessário saber qual a funcionalidade que supostamente ele codifica, i.e. a sua "especificação". Tipicamente, essa especificação é expressa por propriedades lógicas embebidas no próprio código do programa (sob a forma de "anotações"). No entanto, e em domínios específicos como na codificação de técnicas criptográficas, é conveniente apresentar uma "implementação de referência" cujo comportamento é adoptado como modelo.
O objectivo deste projecto consiste em implementar uma metodologia, que tem vindo a ser desenvolvida no grupo de investigação FAST, que permite um certo grau de automatização na verificação da correcção perante implementações de referência.
Recomenda-se a utilização de uma linguagem funcional na realização do projecto (e.g. Haskell ou OCaml).
Esta proposta enquadra-se no projecto FP7 CACE.
INFORMAÇÃO ADICIONAL:
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Verificação estática de programas CALF/CAO
ÁREA CIENTÍFICA:
SECURITY AND PROTECTION
Program Verification
PROPONENTES:
Carlos Bacelar Almeida / Jorge Sousa Pinto
DESCRIÇÃO:
Os ataques a bibliotecas que implementam funcionalidade criptográfica são tipicamente orientados a pequenas falhas na codificação. Assim se explicam os numerosos "vulnerability reports" que nos dão conta de ataques que exploram "stack/heap buffer overflow", etc. Esse facto justifica que no desenho de uma linguagem orientada à codificação de técnicas criptográficas se invista em mecanismos que minimizem os problemas referidos.
Com a "análise estática" de programas pretende-se antecipar potenciais problemas na sua execução por análise do seu código. Um exemplo clássico é a verificação dos limites nos acessos a vectores - nesse caso, pretende-se garantir que esses acessos serão realizados sempre dentro da gama declarada.
Este projecto consiste em desenvolver um módulo de análise estática para a linguagem CALF/CAO --- uma linguagem de domínio específico orientada para a codificação de técnicas criptográficas, desenvolvido no projecto europeu CACE. Esse módulo deverá ser responsável por realizar a análise simbólica do programa e, com o auxílio de um demonstrador automático, fornecer garantias relativas à segurança do programa considerado.
Recomenda-se a utilização de uma linguagem funcional na realização do
projecto (e.g. Haskell ou OCaml).
Esta proposta enquadra-se no projecto FP7 CACE.
INFORMAÇÃO ADICIONAL:
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Extensões de Alto-Nivel Para uma Linguagem de Programação Criptográfica
ÁREA CIENTÍFICA:
SECURITY AND PROTECTION
ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
No âmbito do Projecto FP7 CACE (Computer Aided Cryptography Engineering) está a ser desenvolvida a linguagem de programação CAO. Esta linguagem foi desenhada com o objectivo de facilitar a implementação de algoritmos criptográficos numa notação que se aproxime daquela utilizada nas publicações científicas e normas criptográficas, e será suportada por um compilador que automatizará algumas optimizações e contra-medidas de segurança.
Pretende-se com este projecto explorar algumas extensões de alto-nível à linguagem CAO, que permitirão melhorar a usabilidade da linguagem, nomeadamente na implementação de bibliotecas criptográficas genéricas, que poderão ser instanciadas com parametrizações diferentes. Incluem-se nos objectivos deste trabalho a exploração de sistemas de tipos dependentes, funções de ordem superior, etc. A implementação das ferramentas de suporte a esta linguagem deverão ser realizadas na linguagem OCaml.
LOCAL
Dep. Informática
Suporte para raciocínio sobre estruturas algébricas
ÁREA CIENTÍFICA:
SECURITY AND PROTECTION
ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
PROPONENTES:
Carlos Bacelar Almeida
DESCRIÇÃO:
As estruturas algébricas são um ingrediente fundamental na codificação e na demonstração de segurança das técnicas criptográficas. Raciocinar formalmente sobre elas é assim um aspecto crítico quando está em causa a demonstração de correcção e segurança de software criptográfico.
Neste projecto pretende-se definir uma biblioteca para o Sistema de Prova COQ que incorpore factos e propriedades sobre as estruturas algébricas utilizadas em software criptográfico (grupos, grupos cíclicos, corpos finitos, etc.). Essa bibliotecas terá um papel importante na infra-estrutura de verificação na "toolbox CACE" na medida em que realizará a ponte entre as abstracções disponibilizadas pelas linguagens CAO/CALF, e as demonstrações de correcção/segurança que decorrem das propriedades matemáticas dessas estruturas.
Como base de trabalho, pretende-se adoptar o projecto "Math Components" (http://www.msr-inria.inria.fr/Projects/math-components), biblioteca construída sobre uma extensão da linguagem de tácticas do Coq (SSreflect) que incorpora facilidades avançadas para a gestão de scripts de prova e construção de provas por reflexão. Assim, e numa primeira fase, o projecto consistirá em dominar essa extensão e os conceitos associados. Numa segunda fase, o trabalho incidirá sobre a integração da biblioteca com o gerador de obrigações de prova para a linguagem CALF (desenvolvido no âmbito de outras tarefas do projecto CACE), e com a "toolbox" desenvolvida por David Nowak orientada para a demonstração de segurança de técnicas criptográficas.
Esta proposta enquadra-se no projecto FP7 CACE.
LOCAL:
Dep. Informática
Avaliação de Protocolos de Acordo de Chaves com Autenticação Baseada em Segredos Fracos
ÁREA CIENTÍFICA:
DATA ENCRYPTION
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
A execução de um protocolo de acordo de chaves tipicamente exige a existência de uma infra-estrutura de chave-pública para garantir a autenticação dos agentes. Quando isto não é possível, a autenticação é garantida pela pré-distribuição de um segredo partilhado que, muitas vezes é relativamente fraco no que respeita à informação que permanece desconhecida para os atacantes. As palavras-chave são um exemplo destes segredos, bem como as variáveis aleatórias partilhadas geradas a partir da exploração das características dos canais físicos em redes wireless.
No contexto do projecto de investigação Wireless Information Theoretic Security (WITS) pretende-se avaliar a aplicabilidade prática dos protocolos de acordo de chaves com autenticação baseada em segredos fracos já propostos na literatura. Para além da implementação dos protocolos, e dado que as soluções existentes são justificadas de formas distintas e com base em aproximações variadas que incluem a Teoria da Informação e a Segurança Computacional, será necessário estabelecer uma metodologia que permita medir a performance das diferentes soluções para níveis de segurança comparáveis.
LOCAL:
Dep. Informática
Exploração de Algorítmos de Anonimização de Bases de Dados
ÁREA CIENTÍFICA:
DATA ENCRYPTION
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
As técnicas de anonimização de bases de dados são uma tecnologia emergente. O seu objectivo é permitir a divulgação de listagens com informação útil para data mining, mas sujeitas a restrições devido a questões de privacidade. Um exemplo clássico é a divulgação de uma listagem com um conjunto de pacientes que deram entrada num hospital num dado período de tempo, conjuntamente com as condições médicas de que padeciam. A omissão da identidade do paciente, sendo necessária à preservação da sua privacidade, não elimina a possibilidade da sua identificação. De facto, campos como o código-postal, a idade e o sexo podem permitir, só por si, identificar um indivíduo univocamente. São, por este motivo, chamados de quasi-identificadores. No entanto, a eliminação de todos estes quasi-identificadores torna os dados inúteis de um ponto de vista estatístico.
A anonimização consiste em processar os dados, agrupando os registos que tenham valores suficientemente próximos dos quasi-identificadores, de maneira a que um número suficiente de indivíduos em questão se tornem indistinguíveis a um observador, mesmo que este tenha algum conhecimento externo. Pretende-se com este projecto a validação, implementação e benchmarking de um algoritmo desenvolvido no âmbito de um projecto de transferência de tecnologia terminado recentemente.
LOCAL:
Dep. Informática
Reutilização de alietoridade entre diversas primitivas criptográficas
ÁREA CIENTÍFICA:
DATA ENCRYPTION
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
A disponibilidade de bits perfeitamente aleatórios na implementação de algoritmos criptográficos é um dos pressupostos fundamentais à sua segurança. No entanto, a geração de bits aleatórios com qualidade adequada é uma operação custosa, que pode mesmo colocar em causa a viabilidade de implementação de determinados algoritmos criptográficos em plataformas com recursos limitados.
Uma das soluções para este problema, que permite obter ganhos significativos em termos do peso computacional e largura de banda, é amortizar esse custo reutilizando a mesma aleatoriedade em diversas execuções de um mesmo algoritmo. No entanto, este tipo de optimização tem de ser cuidadosamente analisado a nível teórico, para garantir que não implica perdas de segurança.
Pretende-se com este projecto estender os resultados teóricos existentes para o caso em que se reutiliza aleatoriedade entre algoritmos de natureza diferentes, nomeadamente entre algoritmos de cifra e assinatura digital.
LOCAL:
Dep. Informática
Extensões de Alto-Nível Para uma Linguagem de Programação Criptográfica
ÁREA CIENTÍFICA:
DATA ENCRYPTION
LANGUAGE CONSTRUCTS AND FEATURES
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
No âmbito do Projecto FP7 CACE (Computer Aided Cryptography Engineering) está a ser desenvolvida a linguagem de programação CAO. Esta linguagem foi desenhada com o objectivo de facilitar a implementação de algoritmos criptográficos numa notação que se aproxime daquela utilizada nas publicações científicas e normas criptográficas, e será suportada por um compilador que automatizará algumas optimizações e contra-medidas de segurança.
Pretende-se com este projecto explorar algumas extensões de alto-nível à linguagem CAO, que permitirão melhorar a usabilidade da linguagem, nomeadamente na implementação de bibliotecas criptográficas genéricas, que poderão ser instanciadas com parametrizações diferentes. Incluem-se nos objectivos deste trabalho a exploração de sistemas de tipos dependentes, funções de ordem superior, etc. A implementação das ferramentas de suporte a esta linguagem deverão ser realizadas na linguagem OCaml.
Functional programming support for language processing
Most of this software is programmed in the functional programming language Haskell. Some tools and libraries are also available as part of the UMinho Haskell Libraries & Tools.
The Theory and Formal Methods Seminar series (TfmSeminar) is a bi-weekly scientific colloquium organized by the Theory and Formal Methods group. The seminar continues the tradition of PURé Café in a wider scope.
Moderator: Jorge Sousa Pinto.
Attendance is open to all.
If you would like to contribute a talk, please contact the moderator.
Extended Static Checking by Strategic Rewriting of Pointfree Relational Expressions
Claudia Necco
We describe how a pointfree treatment of relations, their properties, their operators, and the laws that govern them can be captured in a type-directed strategic rewriting system for transformation of relational expressions. This rewriting tool can be used to simplify relational proof obligations and ultimately reduce them to tautologies. We demonstrate how such reductions provide extended static checking (ESC) for design contraints commonly found in software modeling and development.
XCentric: processamento de XML em programação em lógica
Jorge Coelho, LIACC
Nesta palestra vamos apresentar a linguagem de programação especializada no processamento de XML, XCentric. O XCentric é uma linguagem de programação em lógica baseada numa extensão ao algoritmo de unificação de Robinson para lidar com termos com functores de aridade arbitrária e num sistema de tipos que extende a noção de tipo regular para para permitir tipificar sequências de argumentos: os "regular sequence types". Vai ser apresentada a linguagem, vários exemplos de utilização, o uso de termos com functores de aridade flexivel para representar XML e de regular sequence types para representar linguages de tipos para XML (DTDs e XMLSchema). Em seguida vamos mostrar o uso da nova forma de unificação no processamento (muito compacto e declarativo) de XML e o uso dos tipos para validação desse processamento.
Compreensão de Algoritmos de Routing / Understanding Routing Algorithms
Mario Berón
Nesta palestra conceptualizamos Compreensão de Programas e Ferramentas de Compreensão de Programas. Depois descrevemos um esquema de anotação de código que permite a extracção de informação dinâmica de programas escritos em linguagem C. Como passo seguinte apresentamos um sistema de avaliação de algoritmos de routing denominado EAR (un Evaluador de Algoritmos de Ruteo) que utilizamos para analisar a aplicabilidade do nosso esquema de anotação de código. Também, apresentamos as diferentes visões de EAR que foram extraídas a partir do nosso esquema de anotação. Finalmente apresentamos BORS (Behavioral-Operational Relation Strategy), uma estratégia para relacionar as visões comportamental e operacional de sistemas.
We present an algebraic approach to transformation of structure-shy programs, in particular strategic functions (eg. Strafunski or SyB) and XML queries (eg. XPath). We formulate a rich set of algebraic laws and show how subsets of these laws can be used to construct rewrite systems for specialization, generalization, and optimization of structure-shy programs. Our approach demonstrates that the analogy between the Laplace/Fourier transforms and the point-wise/point-free transform can be extended with a structure-shy/point-free transform.
Secure Cryptographic Workflow in the Standard Model
Manuel Bernardo Barbosa
Following the work of Al-Riyami et al. we define the notion of key encapsulation mechanism supporting cryptographic workflow (WF-KEM) and prove a KEM-DEM composition theorem which extends the notion of hybrid encryption to cryptographic workflow. We then generically construct a WF-KEM from an identity-based encryption (IBE) scheme and a secret sharing scheme. Chosen ciphertext security is achieved using one-time signatures. Adding a public-key encryption scheme we are able to modify the construction to obtain escrow-freeness. We prove all our constructions secure in the standard model.
A two-level data transformation (2LT) consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. A typical example of a 2LT consists in transforming XML schemas into relational database schemas, coupled with the migration of the XML documents to relational tables. Recently, we have developed a type-safe Haskell library for 2LT, based on the theory of data refinement.
9:15
Generation and preservation of referential constraints during two-level tranformation
Pablo Berdaguer
Abstract not available yet
9:45
Luís Pedro Machado
On the correspondance between generic lenses and data refinement
Theory and Formal Methods Seminar Series Wednesdays at 9:00 in the DI meeting room The Theory and Formal Methods Seminar series (TfmSeminar) is a bi weekly scientific ...
FAST Seminar Series Wednesdays at 14:00 in the DI meeting room The FAST Seminar Series is a bi weekly scientific colloquium organized by the and Applications of ...
Propostas de Temas para Dissertações de Mestrado Extensões de Alto Nivel Para uma Linguagem de Programação Criptográfica ÁREA CIENTÍFICA: SECURITY AND PROTECTION ...
Post doctoral positions The Computer Science and Technology Center (Centro de Ciências e Tecnologias de Computação, CCTC) invites applications for a 3 year research ...
The research group on Foundations and Applications of Software Technology is part of the Center for Computing Sciences and Technologies (Centro de Ciências e Tecnologias ...
InPACT: Integrated Engineering Tools for Protection, Automation and Control Systems O projecto InPACT é um projecto de II DT com vista ao desenvolvimento de ferramentas ...
Propostas de Temas para Dissertações de Mestrado Um animador para a linguagem CALF. ÁREA CIENTÍFICA: SECURITY AND PROTECTION ANALYSIS OF ALGORITHMS AND ...
InPACT O projecto InPACT (Integrated Engineering Tools for Protection, Automation and Control Systems) é liderado pela EFACEC e acaba de obter financiamento do QREN ...
New Project: FAST members participate in EFACEC's InPACT project Co chair: J. C. Campos was designated co chair of the programme committee of INTERACÇÃO'08. ...
FAST News New Project: FAST members participate in EFACEC's InPACT project. FAST members J.C. Campos and P.R. Henriques will be cooperating with EFACEC over the ...
2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled with document migration ...
The following research challenges have been targetted in recent work: How to model, design and reason rigorously about highly complex software systems (including ...
2008 Model based Methodologies for Pervasive and Embedded Software 2008 3ª Conferência Interacção Pessoa Máquina 2008 6th national conference of XML: Applications ...
Forthcoming Events 2008 Model based Methodologies for Pervasive and Embedded Software MOMPES (Model based Methodologies for Pervasive and Embedded Software ...
Ph.D. MAP/I Doctoral Programme in Computer Science M.Sc. Courses Master courses in Computer science at Minho University are built upon the concept of specialisation ...
TWiki.DI/FAST Web Preferences The following settings are web preferences of the TWiki.DI/FAST web. These preferences overwrite the site level preferences in ...
The FAST group develops and maintains software tools and libraries that support its research and education activities. name description Camila VDM meets ...
Livros a comprar Por favor indiquem o número de cópias e um link para a página respectiva na editora. E verifiquem se já existe na biblioteca! Kees Doets and ...
body { background color : lightgray; font family: Verdana, Arial, Helvetica, sans serif; font size: 12px ; } a:link { text decoration : none ; color : darkblue ...
This is a subscription service to be automatically notified by e mail when topics change in this DI/FAST web. This is a convenient service, so you do not have to ...
The research group on Foundations and Applications of Software Technology is part of the Center for Computing Sciences and Technologies (Centro de Ciências e Tecnologias da Computação, CCTC) of the University of Minho (Braga, Portugal).
FAST's research is concerned with foundations (F), applications (A) and software (S) technology (T) and spreads over HCI, software components, reactive systems, language technology and security. Abstract modeling binds these concerns together.
Research in this area at the Department of Informatics has a long tradition at the scientific level, with significant links to national industry, and a deep involvement in the department's teaching activities, at both the undergraduate and the postgraduate level.
Regular group's activities include a research seminar that provides a stimulating meeting opportunity for the whole team, including post-grad and final year undergraduate students.
Ph.D. MAP/I Doctoral Programme in Computer Science M.Sc. Courses Master courses in Computer science at Minho University are built upon the concept of specialisation ...
Forthcoming Events 2008 Model based Methodologies for Pervasive and Embedded Software MOMPES (Model based Methodologies for Pervasive and Embedded Software ...
2008 Model based Methodologies for Pervasive and Embedded Software 2008 3ª Conferência Interacção Pessoa Máquina 2008 6th national conference of XML: Applications ...
FAST News New Project: FAST members participate in EFACEC's InPACT project. FAST members J.C. Campos and P.R. Henriques will be cooperating with EFACEC over the ...
New Project: FAST members participate in EFACEC's InPACT project Co chair: J. C. Campos was designated co chair of the programme committee of INTERACÇÃO'08. ...
Post doctoral positions The Computer Science and Technology Center (Centro de Ciências e Tecnologias de Computação, CCTC) invites applications for a 3 year research ...
InPACT: Integrated Engineering Tools for Protection, Automation and Control Systems O projecto InPACT é um projecto de II DT com vista ao desenvolvimento de ferramentas ...
The following research challenges have been targetted in recent work: How to model, design and reason rigorously about highly complex software systems (including ...
FAST Seminar Series Wednesdays at 14:00 in the DI meeting room The FAST Seminar Series is a bi weekly scientific colloquium organized by the and Applications of ...
2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled with document migration ...
body { background color : lightgray; font family: Verdana, Arial, Helvetica, sans serif; font size: 12px ; } a:link { text decoration : none ; color : darkblue ...
InPACT O projecto InPACT (Integrated Engineering Tools for Protection, Automation and Control Systems) é liderado pela EFACEC e acaba de obter financiamento do QREN ...
Livros a comprar Por favor indiquem o número de cópias e um link para a página respectiva na editora. E verifiquem se já existe na biblioteca! Kees Doets and ...
Propostas de Temas para Dissertações de Mestrado Um animador para a linguagem CALF. ÁREA CIENTÍFICA: SECURITY AND PROTECTION ANALYSIS OF ALGORITHMS AND ...
Propostas de Temas para Dissertações de Mestrado Extensões de Alto Nivel Para uma Linguagem de Programação Criptográfica ÁREA CIENTÍFICA: SECURITY AND PROTECTION ...
The FAST group develops and maintains software tools and libraries that support its research and education activities. name description Camila VDM meets ...
Theory and Formal Methods Seminar Series Wednesdays at 9:00 in the DI meeting room The Theory and Formal Methods Seminar series (TfmSeminar) is a bi weekly scientific ...
The research group on Foundations and Applications of Software Technology is part of the Center for Computing Sciences and Technologies (Centro de Ciências e Tecnologias ...
This is a subscription service to be automatically notified by e mail when topics change in this DI/FAST web. This is a convenient service, so you do not have to ...
TWiki.DI/FAST Web Preferences The following settings are web preferences of the TWiki.DI/FAST web. These preferences overwrite the site level preferences in ...
This is a subscription service to be automatically notified by e-mail when topics change in this DI/FAST web. This is a convenient service, so you do not have to come back and check all the time if something has changed. To subscribe, please add a bullet with your WikiName in alphabetical order to this list:
Format: <space><space><space>, followed by: * Main.yourWikiName (if you want that the e-mail address in your home page is used) * Main.yourWikiName - yourEmailAddress (if you want to specify a different e-mail address) * Main.anyTWikiGroup (if you want to notify all members of a particular TWikiGroup)
Related topics:TWikiUsers, TWikiRegistration
The following settings are web preferences of the TWiki.DI/FAST web. These preferences overwrite the site-level preferences in TWikiPreferences, and can be overwritten by user preferences (your personal topic, i.e. TWikiGuest in the TWiki.Main web)
Preferences:
Set SKIN=nat
Set SKINSTYLE = Kubrick
Set STYLEBORDER = thin
Set STYLEBUTTONS = off
Set STYLESIDEBAR = left
Set STYLEVARIATION = none
Set STYLESEARCHBOX = off
Set PAGETITLE = FAST
Set NATWEBLOGO = FAST
Set WEBLOGOALT = Foundations and Applications of Software Technology
If yes, set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Make sure to list only links that include the name of the web, e.g. DI/FAST.Topic links.
Set SITEMAPLIST = on
Set SITEMAPWHAT = Foundations and Applications of Software Technology
Set SITEMAPUSETO = Foundations and Applications of Software Technology
Exclude web from a web="all" search: (Set to on for hidden webs)
Set NOSEARCHALL =
Default template for new topics and form(s) for this web:
WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
Set FINALPREFERENCES = WEBTOPICLIST, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME
Notes:
A preference is defined as: 6 spaces * Set NAME = value Example:
Set WEBBGCOLOR = #FFFFC0
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #FFCC66 .
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce new preferences variables and use them in your topics and templates. There is no need to change the TWiki engine (Perl scripts).
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #FFCC66
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce your own preferences variables and use them in your topics and templates.
TWiki's DI/FAST web
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST
The DI/FAST web of TWiki. TWiki is a Web-Based Collaboration Platform for the Corporate World.en-usCopyright 2020 by contributing authorsTWiki Administrator [webmaster@di.uminho.pt]The contributing authors of TWikiTWikiDIUM.DI/FAST
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST
/twiki/pub/Main/LocalLogos/um_eengP.jpgTfmSeminar
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/TfmSeminar
Theory and Formal Methods Seminar Series Wednesdays at 9:00 in the DI meeting room The Theory and Formal Methods Seminar series (TfmSeminar) is a bi weekly scientific ... (last changed by JoseNunoOliveira)2010-05-14T00:01:27ZJoseNunoOliveiraFastSeminar
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastSeminar
FAST Seminar Series Wednesdays at 14:00 in the DI meeting room The FAST Seminar Series is a bi weekly scientific colloquium organized by the and Applications of ... (last changed by JoseNunoOliveira)2010-05-13T23:54:40ZJoseNunoOliveiraMscThemes0910
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/MscThemes0910
Propostas de Temas para Dissertações de Mestrado Extensões de Alto Nivel Para uma Linguagem de Programação Criptográfica ÁREA CIENTÍFICA: SECURITY AND PROTECTION ... (last changed by ManuelBernardoBarbosa)2009-09-29T16:49:44ZManuelBernardoBarbosaFastOpportunities
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastOpportunities
Post doctoral positions The Computer Science and Technology Center (Centro de Ciências e Tecnologias de Computação, CCTC) invites applications for a 3 year research ... (last changed by JoseBacelarAlmeida)2009-09-29T15:04:07ZJoseBacelarAlmeidaWebHome
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/WebHome
The research group on Foundations and Applications of Software Technology is part of the Center for Computing Sciences and Technologies (Centro de Ciências e Tecnologias ... (last changed by PedroRangelHenriques)2009-06-28T00:49:26ZPedroRangelHenriquesFastProjects
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastProjects
InPACT: Integrated Engineering Tools for Protection, Automation and Control Systems O projecto InPACT é um projecto de II DT com vista ao desenvolvimento de ferramentas ... (last changed by AntonioNestorRibeiro)2009-06-23T13:18:07ZAntonioNestorRibeiroMscThemes0809
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/MscThemes0809
Propostas de Temas para Dissertações de Mestrado Um animador para a linguagem CALF. ÁREA CIENTÍFICA: SECURITY AND PROTECTION ANALYSIS OF ALGORITHMS AND ... (last changed by JoseBacelarAlmeida)2008-09-26T17:00:42ZJoseBacelarAlmeidaInPACT
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/InPACT
InPACT O projecto InPACT (Integrated Engineering Tools for Protection, Automation and Control Systems) é liderado pela EFACEC e acaba de obter financiamento do QREN ... (last changed by JoseCampos)2008-09-08T23:41:19ZJoseCamposFastNewsHeadlines
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastNewsHeadlines
New Project: FAST members participate in EFACEC's InPACT project Co chair: J. C. Campos was designated co chair of the programme committee of INTERACÇÃO'08. ... (last changed by TWikiGuest)2008-09-08T23:30:49ZguestFastNews
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastNews
FAST News New Project: FAST members participate in EFACEC's InPACT project. FAST members J.C. Campos and P.R. Henriques will be cooperating with EFACEC over the ... (last changed by JoseCampos)2008-09-08T23:30:49ZJoseCamposFastPeople
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastPeople
Staff (All email addresses are AT di.uminho.pt except where indicated) Nuno Oliveira (PI, Associate Professor) http://repositorium.sdum.uminho.pt/items ... (last changed by JoseBacelarAlmeida)2008-08-29T14:00:45ZJoseBacelarAlmeidaFastTools
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastTools
2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled with document migration ... (last changed by JoseBacelarAlmeida)2008-04-09T17:16:21ZJoseBacelarAlmeidaFastResearch
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastResearch
The following research challenges have been targetted in recent work: How to model, design and reason rigorously about highly complex software systems (including ... (last changed by JoseBacelarAlmeida)2008-04-09T16:53:41ZJoseBacelarAlmeidaFastPastProjects
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastPastProjects
Past Projects Program Understanding and Re engineering: Calculi and Applications (FCT contract POSI/CHS/44304/2002) http://www.di.uminho.pt/~jmf/ ... (last changed by JoseBacelarAlmeida)2008-03-30T16:02:34ZJoseBacelarAlmeidaFastEventsHeadlines
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastEventsHeadlines
2008 Model based Methodologies for Pervasive and Embedded Software 2008 3ª Conferência Interacção Pessoa Máquina 2008 6th national conference of XML: Applications ... (last changed by TWikiGuest)2008-03-29T04:51:56ZguestFastEvents
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastEvents
Forthcoming Events 2008 Model based Methodologies for Pervasive and Embedded Software MOMPES (Model based Methodologies for Pervasive and Embedded Software ... (last changed by JoseBacelarAlmeida)2008-03-29T04:51:56ZJoseBacelarAlmeida
Master courses in Computer science at Minho University are built upon the concept of specialisation course.
Each of these corresponds to a half-time academic year, and are focused on a particular applicational area of computer science. Moreover, they incorporate an important project component, where the student must incorporate all the necessary skills.
FAST group members are involved in the following courses:
MOMPES 2008 - Model-based Methodologies for Pervasive and Embedded Software
MOMPES (Model-based Methodologies for Pervasive and Embedded Software) workshop series focuses on the scientific and practical aspects related with the adoption of MDA and other MBD methodologies (notation, process, methods, and tools) for supporting the construction of computer-based systems, and more specifically, pervasive and embedded software.
The 5th edition of this wrokshop will be organized within ETAPS 2008 (11th European Joint Conferences on Theory and Practice of Software), Budapest, Hungary, April 5, 2008.
A Interacção 2008 – 3ª Conferência Interacção Pessoa-Máquina – realiza-se na Universidade de Évora, de 15 a 17 de Outubro de 2008, e visa reunir investigadores, docentes e profissionais das diversas áreas envolvidas, promovendo a partilha de conhecimentos e pontos de vista sobre a Interacção Pessoa-Máquina em Portugal.
Past Events
XATA 2008 - 6th national conference of XML: Applications and Technologies. Évora, 14,15 February 2008.
CIC 2007 - Research Workshop on Coinduction, Interaction and Composition.
GTTSE'07 - Summer School on Generative and Transformational Techniques in Software Engineering, 2007.
ETAPS'07 - European Joint Conferences on Theory and Practice of Software, 2007
New Project: FAST members participate in EFACEC's InPACT project.
FAST members J.C. Campos and P.R. Henriques will be cooperating with EFACEC over the next two years in its, QREN funded, InPACT project (Integrated Engineering Tools for Protection, Automation and Control Systems).
Sep 08, 2008 11:59 PM
Co-chair: J. C. Campos was designated co-chair of the programme committee of INTERACÇÃO'08.
The conference will be held in Évora, 15-17 October 2008.
Oct 12, 2007 2:08 PM
New Paper: Simulation and Formal Verification of Industrial Systems Controllers
J. Machado and E. Seabra and J.C. Campos and F. Soares and C.P. Leao and J.F. Silva (forthcoming) In 19th International Congress of Mechanical Engineering (COBEM 2007).
Oct 12, 2007 1:40 AM
New Paper: Formal analysis of interactive systems: opportunities and weaknesses
M. D. Harrison and J. C. Campos and K. Loer (forthcoming) In P. Cairns and A. Cox, editors, Research Methods in Human Computer Interaction. Cambridge University Press.
Oct 12, 2007 1:39 AM
New Paper: Connecting rigorous system analysis to experience centred design
(download from RepositoriUM? )
M. D. Harrison and J. C. Campos and G. Doherty and K. Loer (forthcoming) In E. Law and E. Hvannberg and G. Cockton and J. Vanderdonckt, editors, Maturing Usability: Quality in Software, Interaction and Value, Human-Computer Interaction Series. Springer. (ISSN: 1571-5035; ISBN: 978-1-84628-940-8)
Oct 12, 2007 1:39 AM
New Paper: A New Plant Modelling Approach For Formal Verification Purposes
J. Machado and E. Seabra and F. Soares and J. Campos (forthcoming) In 11th IFAC Symposium on Large Scale Systems 2007. Elsevier.
New Paper: Considering context and users in interactive systems analysis
J.C. Campos and M.D. Harrison (forthcoming) In Engineering Interactive Systems 2007, Lecture Notes in Computer Science. Springer-Verlag.
New Paper: An Interaction Model and Infrastructure for Localized Activities in Pervasive Computing Environments
H. Pinto and R. José and J. C. Campos (2007) In IEEE International Conference on Pervasive Services 2007 (ICPS'07), pages 232-241. IEEE Computer Society Press. (ar: 18/64 ~.28)
NewPaper: Model-based user interface testing with Spec Explorer and ConcurTaskTrees?
J. L. Silva and J. C. Campos and A. Paiva (2007) In Paul Curzon and Antonio Cerone, editors, The Pre-proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems (FMIS 2007), pages 116-133. (to appear in ENTCS, Springer - ar: 7/18 ~.39)
New Paper: Exploring an option space to engineer a ubiquitous computing system
M. Harrison and C. Kray and J. C. Campos (2007) In Paul Curzon and Antonio Cerone, editors, The Pre-proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems (FMIS 2007), pages 67-82. (to appear in ENTCS, Springer - ar: 7/18 ~.39)
New Paper: Exploring an option space to engineer a ubiquitous computing system
M. Harrison and C. Kray and J. C. Campos (2007) In Paul Curzon and Antonio Cerone, editors, The Pre-proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems (FMIS 2007), pages 67-82. (to appear in ENTCS, Springer - ar: 7/18 ~.39)
New Paper: Integrating HCI into a Software Engineering course
A.N. Ribeiro and J.C. Campos and F.M. Martins (2007) In Pre-proceedings HCI Educators 2007.
New Paper: Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications
J. C. Silva and J. C. Campos and J. Saraiva (2007) In G. Doherty and A. Blandford, editors, Interactive Systems: Design, Specification and Verification, volume 4323 of Lecture Notes in Computer Science, pages 137-150. Springer-Verlag.
New Paper: Paper Coupled Schema Transformation and Data Conversion For XML and SQL (by Pablo Berdaguer, Alcino Cunha, Hugo Pacheco, and Joost Visser) accepted by PADL 2007 (Nice, France).
Oct 5, 2006 4:21 PM
New Paper: Paper Strongly Typed Rewriting For Coupled Software Transformation (by AlcinoCunha? and Joost Visser) accepted by RULE 2006 (Seattle, USA).
Sep 25, 2006 11:42 AM
New Paper: Paper Strong Types for Relational Databases by Alexandra Silva and Joost Visser has been accepted for the Haskell Workshop 2006 (Portland, USA).
Sep 25, 2006 11:42 AM
New Paper: Paper Configurations of Web Services by MarcoAntonioBarbosa? and LuisSoaresBarbosa? has been accepted for FOCLASA'06 (Bonn, Germany).
Sep 25, 2006 11:41 AM
New Paper: Paper Towards a Coordination Model for Interactive Systems by MarcoAntonioBarbosa? , JoseCampos? and LuisSoaresBarbosa? has been accepted for FMIS'06 (Macau).
Sep 25, 2006 11:40 AM
The Computer Science and Technology Center (Centro de Ciências e Tecnologias de Computação, CCTC) invites applications for a 3 year research position in the area of Software Foundations. Specific expertise is sought in applied semantics, software analysis and transformation, formal verification, provable security and theory of programming languages as well as eager interest in formal foundations and a strong aptitude for projects with real-world potential. (Application deadline: 30-09-2008; more information).
InPACT: Integrated Engineering Tools for Protection, Automation and Control Systems
O projecto InPACT é um projecto de II&DT com vista ao desenvolvimento de ferramentas de engenharia
avançadas para aplicação a sistemas de protecção, automação e controlo (PAC) de sistemas eléctricos de
energia. Nestes sistemas incluem-se os domínios (i) da automação de subestações (SAS), (ii) comando e
controlo de centrais electroprodutoras, (iii) automação de redes de distribuição e (iv) sistemas afins.
O projecto tem enfoque particular no SAS e em tecnologia de automação distribuída com base em normas
internacionais aplicáveis, nomeadamente a IEC 61850 e normalização internacional associada e a IEC 61131-3,
não deixando de abranger conceitos mais recentes como aqueles incluídos na série de normas IEC 61499 ou
abordar outras tecnologias comunicativas de segunda geração como aquelas baseadas na série de normas IEC
60870-5.
A Universidade do Minho traz ao projecto competências nas áreas de investigação científica,
análise e desenho de soluções nos domínios genéricos de aplicações informáticas e, em particular, nos domínios específicos da interface ao utilizador, edição diagramática, compiladores de linguagens, linguagens
visuais e validação de comportamento.
Jul/2008-Jun/2010
Funded by EFACEC and QREN
Partners: EFACEC, U.Minho, EDP.
Budget: 81K¤ (UMinho budget)
The goal of this project is to design, develop and deploy a toolbox that will support the specific domain of cryptographic software engineering. Ordinarily, development of cryptographic software is a huge challenge:security and trust is mission critical and modern applications processing sensitive data typically require the deployment of sophisticated cryptographic techniques. The proposed toolbox will allow non-experts to develop high-level cryptographic applications and business models by means of cryptography-aware high-level programming languages and compilers. The description of such applications in this way will allow automatic analysis and transformation of cryptographic software to detect security critical implementation failures, e.g., software and hardware based side-channel attacks, when realizing low level cryptographic primitives and protocols.
CACE is an FP7 project funded by the European Union.
CACE will start beginning of 2008 and run for 3 years.
This project aims at providing innovative, efficient and expressive mechanisms for the secure implementation and execution of code, with an emphasis on problems posed by embedded systems.
Rescue is a 3 year project, funded by FCT under contract PTDC/EIA/65862/2006.
Starting date: January 2008.
AMADEUS: Aspects and Compiler Optimizations for Matlab System Development
This project addresses the enrichment of MATLAB with aspect-oriented extensions to include additional information (e.g., type and shape of variables) and to experiment different implementation features (e.g., different implementations for the same function, certain type binding for variables, etc.). The proposed aspects aim to configure the low-level data representation of real variables and expressions, to specifically-tailored data representations that benefit from a more efficient support by target computing engines (e.g., fixed- instead of floating-point representations). The approach also aims to help developers to introduce handlers (code triggered when certain conditions may occur and with a richer functionality than assertions) and monitoring features, and to configure function implementations. We believe aspect-oriented extensions will help system modelling, simulation, and exploration of features conceiving system implementation. One of the advantages is related to the fact that a single version of the specification can be used throughout the entire development cycle rather than maintaining multiple versions, as is currently the case.
Nov/2007-Oct/2009
Funded by FCT (PTDC/EIA/70271/2006)
Partners: Inesc-ID, U.Minho, Uninova, Deimos.
Budget: 106K¤
IVY's goal is to develop a model based tool for the analysis of interactive systems designs. The tool will act as a front end to the SMV model checker, creating an abstraction layer where models of interactive systems can be developed and analysed.
Language Engineering and Rigorous Software Development is an ALFA project (Latin America Academic Training ) funded by the European Comission.
Project partners are the Universities of Minho (coordinator), Utrecht, Chalmers, INRIA, Politécnica de Valência, Castilla-La Mancha, La República, EAFIT, Nacional de San Luís, Federal de Minas Gerais, Católica de Santiago del Estero.
The project will fund a total of 27 PhD students co-tutored by a Latin-American and an European institution. Total funding: approx. 530.000¤. Current state: 8 PhD students have started their work.
Additionally the project will set up a research network in the areas of Programming Languages and Rigorous Software Construction.
The Types project is a coordination action in EU′s 6th. framework programme. It started in September 2004 and is a continuation of a number of successful European projects.
Maria João Frade is associated to this project.
GRICES-00342
Technological and Scientific Cooperation Project between Portugal and the P. R. of China on Formal Foundations for Component-based Programming
A Iberoamerican network of experts in Software Verification and Validation. Funded by CYTED. Started 01/2007, runs for 3 years. J. F. Campos and J. B. Almeida are members.
SOFTAS: Software Development with Aspects
This project aims at inventing a seamless AOSD process by focusing on the definition of a complete software methodology covering all the development stages, so that crosscutting and non-crosscutting concerns can be traced during the lifecycle to produce efficient and high-quality software applications. The research results will be instantiated in practice with real world examples from industry.
In summary, the two main objectives of the project are:
to propose a modelling and architecture design framework, which includes a methodology and tools to help the development of software applications that can take advantage of the principles of aspect-orientation;
to derive quantitative evidence on the improvement on the modularity of produced software and other quality attributes.
Sep/2005-Dec/2007
Funded by FCT (POSC/EIA/60189/2004)
Partners: FCT-UNL, U.Minho, IP Beja, LINCIS, NAV.
Budget: FCT: 89K¤
The following research challenges have been targetted in recent work:
How to model, design and reason rigorously about highly complex software systems (including forms of composition, coordination, interaction and deployment)?
How to derive correct software from abstract models (oriented to critical aspects of system's design such as eg, functionality, security, data quality and usability)?
How to reconstruct abstract models from the real world (including legacy software and incomplete or inconsistent data sources)?
The talk is very much work in progress. During the last few months I have been exploring models of a simple ubiquitous system to explore plausible operator behaviours. The first model, developed in UPPAAL, includes simple timing constraints driven by the process that a mobile device is intended to control. The second PROMELA model describes the same system but also makes explicit the information resources that would be used by the operator to control the plant. The talk will mainly focus on the PROMELA model. However I aim to discuss why the UPPAAL model was easier to construct and (at a simple level) to analyse, and to raise preliminary questions about time aspects of the model.
Keiko Nakata (Institute of Cybernetics, Tallinn University of Technology)
Wed, 17 Jun, 2009 at 11:30
In our previous work we have studied several coinductive operational semantics, all of which are proved equivalent, for the While language to describe terminating as well as non-terminating program executions. The operational semantics keep track of all the intermediate states that an execution goes through as a trace (a sequence of states). The trace is finite for a terminating execution and infinite for a non-terminating execution. In this talk I present a Hoare-logic for While, which is proved sound and complete with respect to those operational semantics. As usual, our Hoare-triple consists of a precondition, a statement and a postcondition. The precondition is a predicate on initial states, whereas the postcondition is a predicate on traces. Since a trace contains the full information about an execution, the logic can talk about for instance if an execution is terminating or if an variable is updated infinitely often. My talk will start by introducing a coinductive big-step relational semantics, then present the Hoare-logic. I will explain some interesting design issues on the logic and our strategy for proving its completeness, that we have discovered through many failed attempts. All the results have been formalized in Coq.
O objectivo da integração de sistemas de informação consiste na união de serviços e informações de diversos sub-sistemas independentes, por forma a obter uma solução única, coerente e integrada. Por outro lado, os modelos e linguagens de coordenação têm como principal objectivo especificar e raciocinar sobre configurações de cooperação entre entidades computacionais distintas e independentes. Apesar das diferenças fundamentais na forma com atacam os seus problemas específicos, a aplicação dos modelos e linguagens de coordenação à integração de sistemas de informação parece um exercício imediato e com enormes vantagens para o sucesso de projectos de integração de software. No entanto, esta relação encontra-se extremamente mal explorada, com a excepção de casos pontuais do uso de modelos de orquestração e coreografia. Nesta apresentação apresentar-se-á um conjunto de estilos de integração de sistemas de informação, tendo como preocupação explorar novas aplicações dos modelos de coordenação a cada estilo de integração introduzido. Para além de apresentar os estilos de integração de forma clara e independente de tecnologias específicas, é ainda apresentada uma organização comparativa dos estilos de integração.
The advent of On-Chip parallelism poses a dreadful obstacle to current mature programming languages. Traditional approaches based on compiler or hand-coded optimizations are giving place to trendy generative techniques, based on DSL and ad-hoc program transformation frameworks. In this talk we will report on our first steps in the attempt to lay the common (categorical) semantics of a particular class of DSL addressing numerical programming under the motto "matrices as arrows!" We will shift the traditional view of matrices as indexed structures to an index-free representation, analogous to point-free program transformation.
Miriam Alves (Instituto de Aeronáutica - IAE, Brasil)
Wed, 04 Feb, 2009 at 14:00
Esta apresentação abordará, de forma sucinta, as principais atividades do Instituto de Aeronáutica e Espaço (IAE - Brasil)- relacionadas aos Projetos de Veículos Lançadores de Satélites, com ênfase no desenvolvimento, validação e verificação tanto do software embarcado nestes veículos como nos sistemas de software de apoio de solo para a realização das missões de lançamento. Considerando a importância e o aspecto crítico destes sistemas de software, serão apresentadas as iniciativas mais recentes do grupo de software do IAE para a melhoria do processo de desenvolvimento e da abordagem de verificação e validação.
In this talk we will discuss the generation of visual programming environments in an automatic way, from the formal specification of the underlying language. An automatic visual environment generator, named DEViL? , is the base of the discussion. DEViL? generates visual programming environments with integration of graphical editors, compilers, translators and several others tools, from attribute grammars for visual-languages. A running example, VisualLISA? , is used to present the workflow to generate a visual programming environment. VisualLISA? is a visual editor for Attribute Grammar (AG) specifications. This editor is generated from a specification of a visual-language that enables us to draw, syntactically and semantically correct, attribute grammars. The visual specification of an AG is production-oriented and incremental. The editor translates the drawn attribute grammar directly into LISA notation or alternatively into a universal XML representation designed to support different AG-based compiler generators.
This talk discusses the development of the GUISurfer tool. GUISurfer is focused on extracting and testing behavioural models from Graphical User Interface (GUI) source code. We present a generic model for language independent reverse engineering of GUI-based applications, and we explore the integration of model-based testing techniques in our approach, thus allowing us to perform fault detection. First we describe our library for GUI models extraction and manipulation. And finally we show how these models can be use to reason about the user interface and generate test cases for automatic GUI testing.
This Ph.D. work, in the general context of Software Engineering, is concerned with software systems' maintenance (systems that may contain millions of lines of code). Namely, the work will be oriented to applications (may be web applications) developed under multi-language Integrated Development Environments (IDEs), where many languages and technologies can be smoothly combined due to the existence of a common language runtime. Maintenance requires the comprehension of the overall system, as well as, the full understanding of each component (a program). Many times, the first task performed to do maintenance is the backward analysis of the system (from code to model), known as the reverse engineering process. Program Comprehension, Program Understanding, and Reverse Engineering activities depend on the so-called program analysis, among other technologies; many times it is important to constrict the program analysis to a program slice to focus only on those statements that are responsible for some state. Maintenance, code re-use, and systems' re-engineering require, as told above, quantifiable methods. That approach implies the definition and use of software metrics. But the complexity of data resulting from program analysis, or even from the metrics evaluation process, demands the resort to high-quality graphical interfaces to help the user to understand and navigate over the imbricated data. So, software visualization is another discipline involved in a systematic, disciplined, quantifiable approach to software maintenance. This contextualization let us understand that the background for the present work requires the study of: code analysis, slicing, metrics, and visualization. Because program verification is nowadays a relevant issue in this area of software engineering, it was decided to include another topic: proof carrying code (PCC). A lot of work has been done in the past in code analysis to help in the various tasks of software re-engineering and maintenance, including program comprehension activities. Many good results have been reached. However in the multi-language multi-technology platform that will be considered, there is still need for a system that can handle programs at different levels of encoding. The aim of this Ph.D. work is to investigate efficient methods, techniques and tools to analyze source (high-level), intermediate (abstract middle-level) or target (low-level/machine) code, under the same environment, in order to extract static and dynamic information that can be visualized in a uniform way (independent of the analysis level) to help in program maintenance---the analysis, comprehension, and verification of a program. The focus of this talk will be the general overview of the Ph.D. project, and a synthesis of the state-of-the-art concerning Program Analysis and Program Slicing.
This paper presents techniques and tools to transform spreadsheets into relational databases and back. A set of data refinement rules is introduced to map a tabular datatype into a relational database schema. Having expressed the transformation of the two data models as data refinements, we obtain for free the functions that migrate the data. We use well-known relational database techniques to optimize and query the data. Because data refinements define bidirectional transformations we can map such database back to an optimized spreadsheet. We have implemented the data refinement rules and we constructed Haskell-based tools to manipulate, optimize and refactor Excel-like spreadsheets.
Context-aware applications pose new usability challenges that cut across the phases of design and development. They provide richer interaction taking context into account. They are difficult to build due to their distributed nature. This talk presents a technical literature review about modelling and simulating virtual environments, with a focus in context-aware applications. Relevant work in this area is discussed and compared through a case study. A first attempt to introducing context into some of the existing modelling approaches is described. Areas that require more work, and that we will possibly follow, are referenced.
In recent years, advances in software tools have made it easier to analyze interactive system specifications, and allow the analyst to consider a wide range of possible behaviors. However, the effort involved in producing the specifications of the system is still substantial, and a difficulty exists regarding the specification of plausible behaviors on the part of the user. Recent trends in technology towards more mobile and distributed systems further exacerbates the issue, as contextual factors come in to play, and less structured, more opportunistic behavior on the part of the user makes purely task-based analysis difficult. In this paper we consider a resourced action approach to specification and analysis. In pursuing this approach we have two aims - firstly, to facilitate a resource-based analysis of user activity, allowing resources to be distributed across a number of artifacts, and secondly to consider within the analysis a wider range of plausible and opportunistic user behaviors without a heavy specification overhead, or requiring commitment to detailed user models.
It is difficult to construct correct models for distributed large-scale service-oriented applications. Typically, the behavior of such applications emerge from interaction and collaboration of multiple components/services. On the other hand, each component, in general, takes part in multiple scenarios. Consequently, not only components, but also their interaction protocols are important in the development process for distributed systems. Coordination models and languages, like Reo, offer powerful ``glue-code'' that encode the interaction protocols. In this work we propose a novel synthesis technique, which can be used to generate Reo circuits directly from scenario specifications. Inspired by the way UML2.0 sequence diagrams can be algebraically composed, we define an algebraic framework for merging connectors generated from partial specifications by exploiting the algebraic structure of UML sequence diagrams.
Floyd-Hoare Logic stands at the heart of the science of Computer Programming, and has been used extensively in both formal software development and program verification. In this talk we review different methods for generating verification conditions for a given specification, and show how they are derived from Hoare's standard inference system. We discuss methods based on program annotations, weakest preconditions, and updates, and present examples of program verification systems based on each of these.
Schema transformations occur in several contexts. Examples are software evolution, refactoring and cross-paradigm mapping (e.g. VDM to SQL transformation). When initial schemas are annotated with contraints, these contraints must be preserved in the target schema. Moreover, during the transformation process, when high-level data structures are refined, new constraints can be added for semantic preservation (e.g. referential integrity). We intend to present a possible solution, using an algebraic approach that is constraint-aware, in the sense that existent contraints are preserved and new contraints are added when necessary. This solution is based on refinement theory and point-free program transformation.
Zoltán Porkolab (Eötvös Loránd University, Budapest)
Wed, 09 Jan, 2008 at 14:00
The C++ and Java programming languages are considered as object-oriented languages. However, both have strong features for generative programming: the C++ templates and the Java generics. Those generative programming facilities make it possible to write abstract data structures and generic algorithms. Moreover C++ templates form a Turing-complete sublanguage of C++, so one can write programs "running" in the compilation time. Template metaprogramming is an emerging new direction in C++ programming for executing algorithms in compilation time. This one time theoretical possibility today became a strong industrial tool widely used in various libraries and applications. In this talk we review the possible fields of application of C++ template metaprogramming, and emphasize its unique advantages.
Analytic usability analysis methods have been proposed as an alternative to user testing in early phases of development due to the cost of the latter approach. By working with models of the systems, analytic models are not capable of identifying implementation related problems that might have an impact on usability. Model-based testing enables the testing of an implemented software artefact against a model of what it should be (the oracle). In the case of model-based user interface testing, a main issue is the use of oracles at an adequate level of abstraction. This talk discusses the findings of an effort to use task models as oracles for model-based testing of user interfaces.
A two-level data transformation system. 2LT is a deliverable of the
PURe project. Examples of application include XML schema evolution coupled
with document migration, and data mappings between VDM abstract models and
SQL.
A Portuguese talking browser is the final product of this project. The application aims at minimizing the scanning time of a web page thus enabling a talking browser to read a web site at a speed comparable to that of a sighted user.
A model based tool for the analysis of interactive systems' designs. The tool acts as a front end to the NuSMV model checker, creating an abstraction layer where models of interactive systems can be developed and analysed. IVY uses a plugin approach enabling for easy integration of new components. Current components include: a text and graphical editor of MAL interactors (the IVY workbench modelling language), a property patterns tool (under development), a compiler from MAL interactors to NuSMV, and a trace visualiser . All components are integrated via IPF (the interactor plugin framework).
An open-source morphological analyzer. Mainly developed for Portuguese,
it includes dictionaries for English and Latin. It is being used to create
spelling dictionaries of several open-source projects, e.g. aspell, Firefox
and Thunderbird dictionaries.
A Topic Maps Builder (Oveia), Validator (Tche), and Navigator (Ulisses): A XML generic platform for TM specification (syntax+semantics), construction (enabling data extraction from heterogenous information resources), validation (according to a constraint spec), storage (XTM-format or Database), and navigation (conceptual browsing).
An open-source workbench for parallel corpora processing. Among
other tools, this includes a sentence aligner and a Probabilistic Translation
Dictionary extractor, plus a word aligner.
A web-based Information System to support the Prosopographic study of portuguese medieval priests, in the context of the "Fasti Ecclesiae Portugaliae".
The UMinho Haskell Libraries are located in the libraries subdirectory. The modules included in the libraries cover a wide range of functionality, for instance: representation and operations on relations and graphs; analysis and manipulation of spreadsheets and Java programs; support for pointfree programming; support for VDM like concepts (such as data type invariants, pre and post-conditions).
Several tools are included in the UMS distributions, among which: DrHylo (Derives hylomorphisms from restricted Haskell syntax), ChopaChops (Graph slicing and chopping), HaGLR (Generalized LR parsing), SdfMetz (An SDF monitoring tool), Camila (Prototype Camila interpreter), VooDooM (Transforms VDM datatypes to a relational representation).
InPACT
O projecto InPACT (Integrated Engineering Tools for Protection, Automation and Control Systems) é liderado pela EFACEC e acaba de obter financiamento do QREN. Outros parceiros são a Universidade do Minho (via DI e CCG) e a EDP Distribuição.
Com o InPACT a EFECEC visa o desenvolvimento e introdução de uma nova linha de ferramentas de engenharia avançadas na sua gama de produto para o sector de actividade de automação, protecção e controlo de sistemas de energia ou similares.
A Universidade do Minho, através do DI e CCG, traz ao projecto competências nas áreas de investigação científica, análise e desenho de soluções nos domínios genéricos de aplicações informáticas e, em particular, nos domínios específicos da interface com o utilizador, edição diagramática, compiladores de linguagens, linguagens visuais e validação de comportamento.
No contexto do InPACT estão disponíveis dois projectos de mestrado na área do desenvolvimento de editores avançados de diagramas. Existes financiamento para estes projectos:
a) Desenvolvimento de um editor de sinópticos (representações do processo controlado 2D vectoriais dinâmicas e interactivas) executável em múltiplas plataformas (web, dispositivo embebido e desktop).
b) Desenvolvimento de um editor diagramático configurável para diferentes linguagens gráficas.
-- JoseCampos - 08 Sep 2008
PROPONENTES:
Carlos Bacelar Almeida / Manuel Alcino Cunha
DESCRIÇÃO:
A linguagem CALF está a ser desenvolvida no âmbito do projecto europeu CACE. Trata-se de uma linguagem de domínio específico para o desenvolvimento de aplicações criptográficas que concilia, por um lado, abstracções poderosas ao nível do sistema de tipos (e.g. tipos parametrizados por valores) e, por outro, matém presente preocupações relativas à eficiência do código resultante.
O tema proposto é o desenvolvimento de um interpretador e de um mini-compilador para essa linguagem.
análise sintáctica do código fonte;
verificação/inferência de tipos;
codificação de uma "shell" que permita o teste rápido de programas;
tradutor da representação interna para código C++ (fazendo uso da biblioteca NTL)
Recomenda-se a utilização de uma linguagem funcional na realização do projecto (e.g. Haskell ou OCaml).
Esta proposta enquadra-se no projecto FP7 CACE.
INFORMAÇÃO ADICIONAL:
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Gerador de Condições de Verificação
ÁREA CIENTÍFICA:
Program Verification
LOGICS AND MEANINGS OF PROGRAMS
PROPONENTES:
Jorge Sousa Pinto / Carlos Bacelar Almeida
DESCRIÇÃO:
As abordagens recentes à verificação de programas envolvem duas componentes:
a utilização de um demonstrador de teoremas (automático ou interactivo);
uma aplicação designada por "Gerador de Condições de Verificação" (VCGen).
A ideia é que o VCGen transforma um programa (anotado com a respectiva especificação) num conjunto de "obrigações de prova" de primeira ordem que possam ser verificadas pelo demonstrador de teoremas considerado. O VCGen é "correcto" na medida em que, se todas as obrigações de prova se verificarem, existe garantia que o programa se encontra "conforme" a especificação apresentada.
O objectivo deste projecto é o de implementar um VCGen para uma linguagem imperativa "C-like". Pretende-se que esse VCGen seja modular, na medida em que diferentes características da linguagem (e.g. utilização de "arrays"; memória dinâmica; etc.) sejam consideradas incrementalmente.
Esta proposta enquadra-se no projecto FCT Rescue e no projecto FP7 CACE.
INFORMAÇÃO ADICIONAL:
Está aberto um concurso para uma bolsa de investigação do projecto Rescue em que este tema se enquadra. Recomenda-se assim que potenciais interessados submetam a respectiva candidatura (mais informações em http://www.eracareers.pt/opportunities/index.aspx?task=global&jobId=11685).
Descrição detalhada: VCGen.pdf
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Computação Multipartida Segura do Logaritmo
ÁREA CIENTÍFICA:
SECURITY AND PROTECTION
Distributed Systems
PROPONENTES:
Carlos Bacelar Almeida
DESCRIÇÃO:
Em "Computação Multipartida Segura" (SMC) existem várias partes que pretendem contribuir com dados para uma dada computação (e.g. alguma estatística sobre a agregação desses dados), mas com garantias que a confidencialidade desses dados não é comprometida. Um domínio onde essas técnicas encontram aplicação é o da "Mineração de Dados com Preservação de Privacidade" (PPDM) - nesse caso cada uma das partes contribui com a sua Base de Dados para uma dada técnica de Mineração de Dados, tendo garantias que as outras partes não obtém qualquer conhecimento desses dados (para além do resultado da técnica executada).
O objectivo deste projecto é a codificação de um algoritmo SMC específico: o cálculo do logaritmo. Esse algoritmo é uma peça fundamental numa grande quantidade de técnicas PPDM, e constitui por si só um excelente exemplo combinação de técnicas específicas de SMC (avaliação segura de circuitos; partilha de segredos; etc.). Pretende-se assim utilizar a codificação do algoritmo proposto como pretexto para apresentar o domínio da SMC.
Linguagens de programação a utilizar: C/C++, Java.
INFORMAÇÃO ADICIONAL:
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Correcção perante implementação de referência
ÁREA CIENTÍFICA:
Program Verification
LOGICS AND MEANINGS OF PROGRAMS
PROPONENTES:
Jorge Sousa Pinto / Carlos Bacelar Almeida
DESCRIÇÃO:
Para se aferir a correcção de um programa é necessário saber qual a funcionalidade que supostamente ele codifica, i.e. a sua "especificação". Tipicamente, essa especificação é expressa por propriedades lógicas embebidas no próprio código do programa (sob a forma de "anotações"). No entanto, e em domínios específicos como na codificação de técnicas criptográficas, é conveniente apresentar uma "implementação de referência" cujo comportamento é adoptado como modelo.
O objectivo deste projecto consiste em implementar uma metodologia, que tem vindo a ser desenvolvida no grupo de investigação FAST, que permite um certo grau de automatização na verificação da correcção perante implementações de referência.
Recomenda-se a utilização de uma linguagem funcional na realização do projecto (e.g. Haskell ou OCaml).
Esta proposta enquadra-se no projecto FP7 CACE.
INFORMAÇÃO ADICIONAL:
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Verificação estática de programas CALF/CAO
ÁREA CIENTÍFICA:
SECURITY AND PROTECTION
Program Verification
PROPONENTES:
Carlos Bacelar Almeida / Jorge Sousa Pinto
DESCRIÇÃO:
Os ataques a bibliotecas que implementam funcionalidade criptográfica são tipicamente orientados a pequenas falhas na codificação. Assim se explicam os numerosos "vulnerability reports" que nos dão conta de ataques que exploram "stack/heap buffer overflow", etc. Esse facto justifica que no desenho de uma linguagem orientada à codificação de técnicas criptográficas se invista em mecanismos que minimizem os problemas referidos.
Com a "análise estática" de programas pretende-se antecipar potenciais problemas na sua execução por análise do seu código. Um exemplo clássico é a verificação dos limites nos acessos a vectores - nesse caso, pretende-se garantir que esses acessos serão realizados sempre dentro da gama declarada.
Este projecto consiste em desenvolver um módulo de análise estática para a linguagem CALF/CAO --- uma linguagem de domínio específico orientada para a codificação de técnicas criptográficas, desenvolvido no projecto europeu CACE. Esse módulo deverá ser responsável por realizar a análise simbólica do programa e, com o auxílio de um demonstrador automático, fornecer garantias relativas à segurança do programa considerado.
Recomenda-se a utilização de uma linguagem funcional na realização do
projecto (e.g. Haskell ou OCaml).
Esta proposta enquadra-se no projecto FP7 CACE.
INFORMAÇÃO ADICIONAL:
No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).
LOCAL:
Dep. Informática
Extensões de Alto-Nivel Para uma Linguagem de Programação Criptográfica
ÁREA CIENTÍFICA:
SECURITY AND PROTECTION
ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
No âmbito do Projecto FP7 CACE (Computer Aided Cryptography Engineering) está a ser desenvolvida a linguagem de programação CAO. Esta linguagem foi desenhada com o objectivo de facilitar a implementação de algoritmos criptográficos numa notação que se aproxime daquela utilizada nas publicações científicas e normas criptográficas, e será suportada por um compilador que automatizará algumas optimizações e contra-medidas de segurança.
Pretende-se com este projecto explorar algumas extensões de alto-nível à linguagem CAO, que permitirão melhorar a usabilidade da linguagem, nomeadamente na implementação de bibliotecas criptográficas genéricas, que poderão ser instanciadas com parametrizações diferentes. Incluem-se nos objectivos deste trabalho a exploração de sistemas de tipos dependentes, funções de ordem superior, etc. A implementação das ferramentas de suporte a esta linguagem deverão ser realizadas na linguagem OCaml.
LOCAL
Dep. Informática
Suporte para raciocínio sobre estruturas algébricas
ÁREA CIENTÍFICA:
SECURITY AND PROTECTION
ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
PROPONENTES:
Carlos Bacelar Almeida
DESCRIÇÃO:
As estruturas algébricas são um ingrediente fundamental na codificação e na demonstração de segurança das técnicas criptográficas. Raciocinar formalmente sobre elas é assim um aspecto crítico quando está em causa a demonstração de correcção e segurança de software criptográfico.
Neste projecto pretende-se definir uma biblioteca para o Sistema de Prova COQ que incorpore factos e propriedades sobre as estruturas algébricas utilizadas em software criptográfico (grupos, grupos cíclicos, corpos finitos, etc.). Essa bibliotecas terá um papel importante na infra-estrutura de verificação na "toolbox CACE" na medida em que realizará a ponte entre as abstracções disponibilizadas pelas linguagens CAO/CALF, e as demonstrações de correcção/segurança que decorrem das propriedades matemáticas dessas estruturas.
Como base de trabalho, pretende-se adoptar o projecto "Math Components" (http://www.msr-inria.inria.fr/Projects/math-components), biblioteca construída sobre uma extensão da linguagem de tácticas do Coq (SSreflect) que incorpora facilidades avançadas para a gestão de scripts de prova e construção de provas por reflexão. Assim, e numa primeira fase, o projecto consistirá em dominar essa extensão e os conceitos associados. Numa segunda fase, o trabalho incidirá sobre a integração da biblioteca com o gerador de obrigações de prova para a linguagem CALF (desenvolvido no âmbito de outras tarefas do projecto CACE), e com a "toolbox" desenvolvida por David Nowak orientada para a demonstração de segurança de técnicas criptográficas.
Esta proposta enquadra-se no projecto FP7 CACE.
LOCAL:
Dep. Informática
Avaliação de Protocolos de Acordo de Chaves com Autenticação Baseada em Segredos Fracos
ÁREA CIENTÍFICA:
DATA ENCRYPTION
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
A execução de um protocolo de acordo de chaves tipicamente exige a existência de uma infra-estrutura de chave-pública para garantir a autenticação dos agentes. Quando isto não é possível, a autenticação é garantida pela pré-distribuição de um segredo partilhado que, muitas vezes é relativamente fraco no que respeita à informação que permanece desconhecida para os atacantes. As palavras-chave são um exemplo destes segredos, bem como as variáveis aleatórias partilhadas geradas a partir da exploração das características dos canais físicos em redes wireless.
No contexto do projecto de investigação Wireless Information Theoretic Security (WITS) pretende-se avaliar a aplicabilidade prática dos protocolos de acordo de chaves com autenticação baseada em segredos fracos já propostos na literatura. Para além da implementação dos protocolos, e dado que as soluções existentes são justificadas de formas distintas e com base em aproximações variadas que incluem a Teoria da Informação e a Segurança Computacional, será necessário estabelecer uma metodologia que permita medir a performance das diferentes soluções para níveis de segurança comparáveis.
LOCAL:
Dep. Informática
Exploração de Algorítmos de Anonimização de Bases de Dados
ÁREA CIENTÍFICA:
DATA ENCRYPTION
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
As técnicas de anonimização de bases de dados são uma tecnologia emergente. O seu objectivo é permitir a divulgação de listagens com informação útil para data mining, mas sujeitas a restrições devido a questões de privacidade. Um exemplo clássico é a divulgação de uma listagem com um conjunto de pacientes que deram entrada num hospital num dado período de tempo, conjuntamente com as condições médicas de que padeciam. A omissão da identidade do paciente, sendo necessária à preservação da sua privacidade, não elimina a possibilidade da sua identificação. De facto, campos como o código-postal, a idade e o sexo podem permitir, só por si, identificar um indivíduo univocamente. São, por este motivo, chamados de quasi-identificadores. No entanto, a eliminação de todos estes quasi-identificadores torna os dados inúteis de um ponto de vista estatístico.
A anonimização consiste em processar os dados, agrupando os registos que tenham valores suficientemente próximos dos quasi-identificadores, de maneira a que um número suficiente de indivíduos em questão se tornem indistinguíveis a um observador, mesmo que este tenha algum conhecimento externo. Pretende-se com este projecto a validação, implementação e benchmarking de um algoritmo desenvolvido no âmbito de um projecto de transferência de tecnologia terminado recentemente.
LOCAL:
Dep. Informática
Reutilização de alietoridade entre diversas primitivas criptográficas
ÁREA CIENTÍFICA:
DATA ENCRYPTION
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
A disponibilidade de bits perfeitamente aleatórios na implementação de algoritmos criptográficos é um dos pressupostos fundamentais à sua segurança. No entanto, a geração de bits aleatórios com qualidade adequada é uma operação custosa, que pode mesmo colocar em causa a viabilidade de implementação de determinados algoritmos criptográficos em plataformas com recursos limitados.
Uma das soluções para este problema, que permite obter ganhos significativos em termos do peso computacional e largura de banda, é amortizar esse custo reutilizando a mesma aleatoriedade em diversas execuções de um mesmo algoritmo. No entanto, este tipo de optimização tem de ser cuidadosamente analisado a nível teórico, para garantir que não implica perdas de segurança.
Pretende-se com este projecto estender os resultados teóricos existentes para o caso em que se reutiliza aleatoriedade entre algoritmos de natureza diferentes, nomeadamente entre algoritmos de cifra e assinatura digital.
LOCAL:
Dep. Informática
Extensões de Alto-Nível Para uma Linguagem de Programação Criptográfica
ÁREA CIENTÍFICA:
DATA ENCRYPTION
LANGUAGE CONSTRUCTS AND FEATURES
PROPONENTES:
Manuel Bernardo Barbosa
DESCRIÇÃO:
No âmbito do Projecto FP7 CACE (Computer Aided Cryptography Engineering) está a ser desenvolvida a linguagem de programação CAO. Esta linguagem foi desenhada com o objectivo de facilitar a implementação de algoritmos criptográficos numa notação que se aproxime daquela utilizada nas publicações científicas e normas criptográficas, e será suportada por um compilador que automatizará algumas optimizações e contra-medidas de segurança.
Pretende-se com este projecto explorar algumas extensões de alto-nível à linguagem CAO, que permitirão melhorar a usabilidade da linguagem, nomeadamente na implementação de bibliotecas criptográficas genéricas, que poderão ser instanciadas com parametrizações diferentes. Incluem-se nos objectivos deste trabalho a exploração de sistemas de tipos dependentes, funções de ordem superior, etc. A implementação das ferramentas de suporte a esta linguagem deverão ser realizadas na linguagem OCaml.
Functional programming support for language processing
Most of this software is programmed in the functional programming language Haskell. Some tools and libraries are also available as part of the UMinho Haskell Libraries & Tools.
The Theory and Formal Methods Seminar series (TfmSeminar) is a bi-weekly scientific colloquium organized by the Theory and Formal Methods group. The seminar continues the tradition of PURé Café in a wider scope.
Moderator: Jorge Sousa Pinto.
Attendance is open to all.
If you would like to contribute a talk, please contact the moderator.
Extended Static Checking by Strategic Rewriting of Pointfree Relational Expressions
Claudia Necco
We describe how a pointfree treatment of relations, their properties, their operators, and the laws that govern them can be captured in a type-directed strategic rewriting system for transformation of relational expressions. This rewriting tool can be used to simplify relational proof obligations and ultimately reduce them to tautologies. We demonstrate how such reductions provide extended static checking (ESC) for design contraints commonly found in software modeling and development.
XCentric: processamento de XML em programação em lógica
Jorge Coelho, LIACC
Nesta palestra vamos apresentar a linguagem de programação especializada no processamento de XML, XCentric. O XCentric é uma linguagem de programação em lógica baseada numa extensão ao algoritmo de unificação de Robinson para lidar com termos com functores de aridade arbitrária e num sistema de tipos que extende a noção de tipo regular para para permitir tipificar sequências de argumentos: os "regular sequence types". Vai ser apresentada a linguagem, vários exemplos de utilização, o uso de termos com functores de aridade flexivel para representar XML e de regular sequence types para representar linguages de tipos para XML (DTDs e XMLSchema). Em seguida vamos mostrar o uso da nova forma de unificação no processamento (muito compacto e declarativo) de XML e o uso dos tipos para validação desse processamento.
Compreensão de Algoritmos de Routing / Understanding Routing Algorithms
Mario Berón
Nesta palestra conceptualizamos Compreensão de Programas e Ferramentas de Compreensão de Programas. Depois descrevemos um esquema de anotação de código que permite a extracção de informação dinâmica de programas escritos em linguagem C. Como passo seguinte apresentamos um sistema de avaliação de algoritmos de routing denominado EAR (un Evaluador de Algoritmos de Ruteo) que utilizamos para analisar a aplicabilidade do nosso esquema de anotação de código. Também, apresentamos as diferentes visões de EAR que foram extraídas a partir do nosso esquema de anotação. Finalmente apresentamos BORS (Behavioral-Operational Relation Strategy), uma estratégia para relacionar as visões comportamental e operacional de sistemas.
We present an algebraic approach to transformation of structure-shy programs, in particular strategic functions (eg. Strafunski or SyB) and XML queries (eg. XPath). We formulate a rich set of algebraic laws and show how subsets of these laws can be used to construct rewrite systems for specialization, generalization, and optimization of structure-shy programs. Our approach demonstrates that the analogy between the Laplace/Fourier transforms and the point-wise/point-free transform can be extended with a structure-shy/point-free transform.
Secure Cryptographic Workflow in the Standard Model
Manuel Bernardo Barbosa
Following the work of Al-Riyami et al. we define the notion of key encapsulation mechanism supporting cryptographic workflow (WF-KEM) and prove a KEM-DEM composition theorem which extends the notion of hybrid encryption to cryptographic workflow. We then generically construct a WF-KEM from an identity-based encryption (IBE) scheme and a secret sharing scheme. Chosen ciphertext security is achieved using one-time signatures. Adding a public-key encryption scheme we are able to modify the construction to obtain escrow-freeness. We prove all our constructions secure in the standard model.
A two-level data transformation (2LT) consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. A typical example of a 2LT consists in transforming XML schemas into relational database schemas, coupled with the migration of the XML documents to relational tables. Recently, we have developed a type-safe Haskell library for 2LT, based on the theory of data refinement.
9:15
Generation and preservation of referential constraints during two-level tranformation
Pablo Berdaguer
Abstract not available yet
9:45
Luís Pedro Machado
On the correspondance between generic lenses and data refinement
Theory and Formal Methods Seminar Series Wednesdays at 9:00 in the DI meeting room The Theory and Formal Methods Seminar series (TfmSeminar) is a bi weekly scientific ...
FAST Seminar Series Wednesdays at 14:00 in the DI meeting room The FAST Seminar Series is a bi weekly scientific colloquium organized by the and Applications of ...
Propostas de Temas para Dissertações de Mestrado Extensões de Alto Nivel Para uma Linguagem de Programação Criptográfica ÁREA CIENTÍFICA: SECURITY AND PROTECTION ...
Post doctoral positions The Computer Science and Technology Center (Centro de Ciências e Tecnologias de Computação, CCTC) invites applications for a 3 year research ...
The research group on Foundations and Applications of Software Technology is part of the Center for Computing Sciences and Technologies (Centro de Ciências e Tecnologias ...
InPACT: Integrated Engineering Tools for Protection, Automation and Control Systems O projecto InPACT é um projecto de II DT com vista ao desenvolvimento de ferramentas ...
Propostas de Temas para Dissertações de Mestrado Um animador para a linguagem CALF. ÁREA CIENTÍFICA: SECURITY AND PROTECTION ANALYSIS OF ALGORITHMS AND ...
InPACT O projecto InPACT (Integrated Engineering Tools for Protection, Automation and Control Systems) é liderado pela EFACEC e acaba de obter financiamento do QREN ...
New Project: FAST members participate in EFACEC's InPACT project Co chair: J. C. Campos was designated co chair of the programme committee of INTERACÇÃO'08. ...
FAST News New Project: FAST members participate in EFACEC's InPACT project. FAST members J.C. Campos and P.R. Henriques will be cooperating with EFACEC over the ...
2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled with document migration ...
The following research challenges have been targetted in recent work: How to model, design and reason rigorously about highly complex software systems (including ...
2008 Model based Methodologies for Pervasive and Embedded Software 2008 3ª Conferência Interacção Pessoa Máquina 2008 6th national conference of XML: Applications ...
Forthcoming Events 2008 Model based Methodologies for Pervasive and Embedded Software MOMPES (Model based Methodologies for Pervasive and Embedded Software ...
Ph.D. MAP/I Doctoral Programme in Computer Science M.Sc. Courses Master courses in Computer science at Minho University are built upon the concept of specialisation ...
TWiki.DI/FAST Web Preferences The following settings are web preferences of the TWiki.DI/FAST web. These preferences overwrite the site level preferences in ...
The FAST group develops and maintains software tools and libraries that support its research and education activities. name description Camila VDM meets ...
Livros a comprar Por favor indiquem o número de cópias e um link para a página respectiva na editora. E verifiquem se já existe na biblioteca! Kees Doets and ...
body { background color : lightgray; font family: Verdana, Arial, Helvetica, sans serif; font size: 12px ; } a:link { text decoration : none ; color : darkblue ...
This is a subscription service to be automatically notified by e mail when topics change in this DI/FAST web. This is a convenient service, so you do not have to ...
The research group on Foundations and Applications of Software Technology is part of the Center for Computing Sciences and Technologies (Centro de Ciências e Tecnologias da Computação, CCTC) of the University of Minho (Braga, Portugal).
FAST's research is concerned with foundations (F), applications (A) and software (S) technology (T) and spreads over HCI, software components, reactive systems, language technology and security. Abstract modeling binds these concerns together.
Research in this area at the Department of Informatics has a long tradition at the scientific level, with significant links to national industry, and a deep involvement in the department's teaching activities, at both the undergraduate and the postgraduate level.
Regular group's activities include a research seminar that provides a stimulating meeting opportunity for the whole team, including post-grad and final year undergraduate students.
Ph.D. MAP/I Doctoral Programme in Computer Science M.Sc. Courses Master courses in Computer science at Minho University are built upon the concept of specialisation ...
Forthcoming Events 2008 Model based Methodologies for Pervasive and Embedded Software MOMPES (Model based Methodologies for Pervasive and Embedded Software ...
2008 Model based Methodologies for Pervasive and Embedded Software 2008 3ª Conferência Interacção Pessoa Máquina 2008 6th national conference of XML: Applications ...
FAST News New Project: FAST members participate in EFACEC's InPACT project. FAST members J.C. Campos and P.R. Henriques will be cooperating with EFACEC over the ...
New Project: FAST members participate in EFACEC's InPACT project Co chair: J. C. Campos was designated co chair of the programme committee of INTERACÇÃO'08. ...
Post doctoral positions The Computer Science and Technology Center (Centro de Ciências e Tecnologias de Computação, CCTC) invites applications for a 3 year research ...
InPACT: Integrated Engineering Tools for Protection, Automation and Control Systems O projecto InPACT é um projecto de II DT com vista ao desenvolvimento de ferramentas ...
The following research challenges have been targetted in recent work: How to model, design and reason rigorously about highly complex software systems (including ...
FAST Seminar Series Wednesdays at 14:00 in the DI meeting room The FAST Seminar Series is a bi weekly scientific colloquium organized by the and Applications of ...
2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled with document migration ...
body { background color : lightgray; font family: Verdana, Arial, Helvetica, sans serif; font size: 12px ; } a:link { text decoration : none ; color : darkblue ...
InPACT O projecto InPACT (Integrated Engineering Tools for Protection, Automation and Control Systems) é liderado pela EFACEC e acaba de obter financiamento do QREN ...
Livros a comprar Por favor indiquem o número de cópias e um link para a página respectiva na editora. E verifiquem se já existe na biblioteca! Kees Doets and ...
Propostas de Temas para Dissertações de Mestrado Um animador para a linguagem CALF. ÁREA CIENTÍFICA: SECURITY AND PROTECTION ANALYSIS OF ALGORITHMS AND ...
Propostas de Temas para Dissertações de Mestrado Extensões de Alto Nivel Para uma Linguagem de Programação Criptográfica ÁREA CIENTÍFICA: SECURITY AND PROTECTION ...
The FAST group develops and maintains software tools and libraries that support its research and education activities. name description Camila VDM meets ...
Theory and Formal Methods Seminar Series Wednesdays at 9:00 in the DI meeting room The Theory and Formal Methods Seminar series (TfmSeminar) is a bi weekly scientific ...
The research group on Foundations and Applications of Software Technology is part of the Center for Computing Sciences and Technologies (Centro de Ciências e Tecnologias ...
This is a subscription service to be automatically notified by e mail when topics change in this DI/FAST web. This is a convenient service, so you do not have to ...
TWiki.DI/FAST Web Preferences The following settings are web preferences of the TWiki.DI/FAST web. These preferences overwrite the site level preferences in ...
This is a subscription service to be automatically notified by e-mail when topics change in this DI/FAST web. This is a convenient service, so you do not have to come back and check all the time if something has changed. To subscribe, please add a bullet with your WikiName in alphabetical order to this list:
Format: <space><space><space>, followed by: * Main.yourWikiName (if you want that the e-mail address in your home page is used) * Main.yourWikiName - yourEmailAddress (if you want to specify a different e-mail address) * Main.anyTWikiGroup (if you want to notify all members of a particular TWikiGroup)
Related topics:TWikiUsers, TWikiRegistration
The following settings are web preferences of the TWiki.DI/FAST web. These preferences overwrite the site-level preferences in TWikiPreferences, and can be overwritten by user preferences (your personal topic, i.e. TWikiGuest in the TWiki.Main web)
Preferences:
Set SKIN=nat
Set SKINSTYLE = Kubrick
Set STYLEBORDER = thin
Set STYLEBUTTONS = off
Set STYLESIDEBAR = left
Set STYLEVARIATION = none
Set STYLESEARCHBOX = off
Set PAGETITLE = FAST
Set NATWEBLOGO = FAST
Set WEBLOGOALT = Foundations and Applications of Software Technology
If yes, set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Make sure to list only links that include the name of the web, e.g. DI/FAST.Topic links.
Set SITEMAPLIST = on
Set SITEMAPWHAT = Foundations and Applications of Software Technology
Set SITEMAPUSETO = Foundations and Applications of Software Technology
Exclude web from a web="all" search: (Set to on for hidden webs)
Set NOSEARCHALL =
Default template for new topics and form(s) for this web:
WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
Set FINALPREFERENCES = WEBTOPICLIST, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME
Notes:
A preference is defined as: 6 spaces * Set NAME = value Example:
Set WEBBGCOLOR = #FFFFC0
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #FFCC66 .
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce new preferences variables and use them in your topics and templates. There is no need to change the TWiki engine (Perl scripts).
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #FFCC66
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce your own preferences variables and use them in your topics and templates.
TWiki's DI/FAST web
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST
The DI/FAST web of TWiki. TWiki is a Web-Based Collaboration Platform for the Corporate World.en-usCopyright 2020 by contributing authorsTWiki Administrator [webmaster@di.uminho.pt]The contributing authors of TWikiTWikiDIUM.DI/FAST
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST
/twiki/pub/Main/LocalLogos/um_eengP.jpgTfmSeminar
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/TfmSeminar
Theory and Formal Methods Seminar Series Wednesdays at 9:00 in the DI meeting room The Theory and Formal Methods Seminar series (TfmSeminar) is a bi weekly scientific ... (last changed by JoseNunoOliveira)2010-05-14T00:01:27ZJoseNunoOliveiraFastSeminar
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastSeminar
FAST Seminar Series Wednesdays at 14:00 in the DI meeting room The FAST Seminar Series is a bi weekly scientific colloquium organized by the and Applications of ... (last changed by JoseNunoOliveira)2010-05-13T23:54:40ZJoseNunoOliveiraMscThemes0910
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/MscThemes0910
Propostas de Temas para Dissertações de Mestrado Extensões de Alto Nivel Para uma Linguagem de Programação Criptográfica ÁREA CIENTÍFICA: SECURITY AND PROTECTION ... (last changed by ManuelBernardoBarbosa)2009-09-29T16:49:44ZManuelBernardoBarbosaFastOpportunities
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastOpportunities
Post doctoral positions The Computer Science and Technology Center (Centro de Ciências e Tecnologias de Computação, CCTC) invites applications for a 3 year research ... (last changed by JoseBacelarAlmeida)2009-09-29T15:04:07ZJoseBacelarAlmeidaWebHome
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/WebHome
The research group on Foundations and Applications of Software Technology is part of the Center for Computing Sciences and Technologies (Centro de Ciências e Tecnologias ... (last changed by PedroRangelHenriques)2009-06-28T00:49:26ZPedroRangelHenriquesFastProjects
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastProjects
InPACT: Integrated Engineering Tools for Protection, Automation and Control Systems O projecto InPACT é um projecto de II DT com vista ao desenvolvimento de ferramentas ... (last changed by AntonioNestorRibeiro)2009-06-23T13:18:07ZAntonioNestorRibeiroMscThemes0809
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/MscThemes0809
Propostas de Temas para Dissertações de Mestrado Um animador para a linguagem CALF. ÁREA CIENTÍFICA: SECURITY AND PROTECTION ANALYSIS OF ALGORITHMS AND ... (last changed by JoseBacelarAlmeida)2008-09-26T17:00:42ZJoseBacelarAlmeidaInPACT
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/InPACT
InPACT O projecto InPACT (Integrated Engineering Tools for Protection, Automation and Control Systems) é liderado pela EFACEC e acaba de obter financiamento do QREN ... (last changed by JoseCampos)2008-09-08T23:41:19ZJoseCamposFastNewsHeadlines
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastNewsHeadlines
New Project: FAST members participate in EFACEC's InPACT project Co chair: J. C. Campos was designated co chair of the programme committee of INTERACÇÃO'08. ... (last changed by TWikiGuest)2008-09-08T23:30:49ZguestFastNews
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastNews
FAST News New Project: FAST members participate in EFACEC's InPACT project. FAST members J.C. Campos and P.R. Henriques will be cooperating with EFACEC over the ... (last changed by JoseCampos)2008-09-08T23:30:49ZJoseCamposFastPeople
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastPeople
Staff (All email addresses are AT di.uminho.pt except where indicated) Nuno Oliveira (PI, Associate Professor) http://repositorium.sdum.uminho.pt/items ... (last changed by JoseBacelarAlmeida)2008-08-29T14:00:45ZJoseBacelarAlmeidaFastTools
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastTools
2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled with document migration ... (last changed by JoseBacelarAlmeida)2008-04-09T17:16:21ZJoseBacelarAlmeidaFastResearch
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastResearch
The following research challenges have been targetted in recent work: How to model, design and reason rigorously about highly complex software systems (including ... (last changed by JoseBacelarAlmeida)2008-04-09T16:53:41ZJoseBacelarAlmeidaFastPastProjects
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastPastProjects
Past Projects Program Understanding and Re engineering: Calculi and Applications (FCT contract POSI/CHS/44304/2002) http://www.di.uminho.pt/~jmf/ ... (last changed by JoseBacelarAlmeida)2008-03-30T16:02:34ZJoseBacelarAlmeidaFastEventsHeadlines
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastEventsHeadlines
2008 Model based Methodologies for Pervasive and Embedded Software 2008 3ª Conferência Interacção Pessoa Máquina 2008 6th national conference of XML: Applications ... (last changed by TWikiGuest)2008-03-29T04:51:56ZguestFastEvents
http://wiki.di.uminho.pt/twiki/bin/view/DI/FAST/FastEvents
Forthcoming Events 2008 Model based Methodologies for Pervasive and Embedded Software MOMPES (Model based Methodologies for Pervasive and Embedded Software ... (last changed by JoseBacelarAlmeida)2008-03-29T04:51:56ZJoseBacelarAlmeida
Rename, move or delete this web: 
If you already know the name of the topic, enter the name of the topic into the 
List topics that start with the letter: 
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.