Languages And Tools for Critical Real-time Systems
The goal of this project is to contribute to a change to the current paradigm of secure ITC infrastructure, according to which the deployment and operation of a critical system implies security enforcement as a reactive process. This, not only requires a significant management overhead, but also fails to provide rigorous security guarantees. The project pursues the development of the theoretical and technological tools to support this shift, building on the state-of-the-art of formal methods, information security and dependability that, independently, are more consolidated research areas.
Project NORTE-07-0124-FEDER-000062 is co-financed by the North Portugal Regional Operational Programme (ON.2 – O Novo Norte), under the National Strategic Reference Framework (NSRF), through the European Regional Development Fund (ERDF). (437.5 KEuro)
WP1: Verification for trustworthy critical real-time systems This work package will develop work on the verification of safety critical real-time software, both advancing the state of the art at the theoretical level and on producing tools that can be used by companies developing critical applications with a particular emphasis in robotics. This will build on current link with non-academic partners in Portugal (e.g. Critical Software), as well as abroad (e.g. aerospace partners in Brazil).
WP Team: J.C. Campos; J. C. Alves; G. Silva; P. Rodrigues
WP2: Programming Languages, Compilers and Virtual Machines The goal of this work-package is to develop advanced programming languages, compilers and runtime systems for embedded systems. The emphasis is on producing applications that are: (a) correct by construction, statically excluding the occurrence of a large class of runtime errors; (b) adaptable, allowing the applications to detect and react to runtime errors, and; (c) efficient, optimizing speed and hardware resource usage.
WP Leader: L. Lopes (FCUP)
WP Team: R. M. Abreu; J. M. P. Cardoso; R. Mendes; J. C. Alves; I. Costa
Publications
João Bispo, Pedro Pinto, Ricardo Nobre, Tiago Carvalho, João M. P. Cardoso, Pedro C. Diniz, “The MATISSE MATLAB Compiler - A MATrix(MATLAB)-aware compiler InfraStructure? for embedded computing SystEms? ,” in IEEE International Conference on Industrial Informatics (INDIN’2013), Bochum, Germany, 29-31 July 2013, IEEE Xplorer, pp. 602-608.
S. Gupta, R. Abreu, J. de Kleer, and A.J.C. van Gemund, "Automatic Systems Diagnosis Without Behavioral Models”. In Proceedings of the IEEE Aerospace Conference 2014, Yellowstone Conference Center in Big Sky, Montana, March 1–8, 2014. IEEE, pp. 1-8.
Ricardo Nobre, João M.P. Cardoso and José Alves, “A DSE Example of Using LARA for Identifying Compiler Optimization Sequences,” in X Jornadas sobre Sistemas Reconfiguráveis (REC'2014), 13 de Abril, 2014, Vilamoura, Algarve, Portugal.
M. Sousa, J.C. Campos, M. Alves and M.D. Harrison. Formal Verification of Safety-Critical User Interfaces: a space system case study. In Formal Verification and Modeling in Human Machine Systems: Papers from the AAAI Spring Symposium, pages 62-67. AAAI Press. 2014. [PDF]
R. Couto, A.N. Ribeiro and J.C. Campos. Application of Ontologies in Identifying Requirements Patterns in Use Cases. In 11th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2014), volume 147 of Electronic Proceedings in Theoretical Computer Science, pages 62-76. 2014. [PDF]
J.C. Campos. High assurance interactive computing systems. In J. Ziegler, J. C. Campos and L. Nigay, editors, HCI Engineering: Charting the Way towards Methods and Tools for Advanced Interactive Systems, pages 39-42. 2014.
R. Couto, A.N. Ribeiro, and J.C. Campos. The Modelery: A Collaborative Web Based Repository. In Computational Science and Its Applications - ICCSA 2014, volume 8584 of Lecture Notes in Computer Science, pages 1-16. Springer. 2014.
C.E. Silva and J.C. Campos. Characterizing the Control Logic of Web Applications' User Interfaces. In Computational Science and Its Applications - ICCSA 2014, volume 8584 of Lecture Notes in Computer Science, pages 263-276. Springer. 2014.
R. Abreu, J. Cunha, J.P. Fernandes, P. Martins, A. Perez, and J. Saraiva. Smelling Faults in Spreadsheets. In IEEE International Conference on Software Maintenance and Evolution (ICSME 2014), pages 111-120. IEEE. 2014.
E. Neto, R. Mendes, and L. Lopes. An architecture for seamless configuration, deployment, and management of wireless sensor-actuator networks. In 3rd International Conference on Sensor Networks (SENSORNETS 2014), pages 73–81, Lisbon, 2013. SCITEPRESS.
L.G.A. Martins, R. Nobre, A.C.B. Delbem, E. Marques, J.M.P. Cardoso, A clustering-based approach for exploring sequences of compiler optimizations. In IEEE Congress on Evolutionary Computation (CEC’14), Beijing, China, July 6-11, 2014, pp. 2436-2443.
L. Martins, R. Nobre, A. Delbem, E. Marques, and J.M.P. Cardoso, Exploration of Compiler Optimization Sequences using Clustering-Based Selection. In ACM SIGPLAN Conference on Languages, Compilers and Tools for Embedded Systems (LCTES’14), Edinburgh, UK, June 12-13, 2014, pp. 63-72.
J. Bispo, L. Reis, and J.M.P. Cardoso, Multi-Target C Code Generation from MATLAB. In ACM/SIGPAN International Workshop on Libraries, Languages and Compilers for Array Programming (ARRAY’2014), Edinburgh, UK, 13 June, 2014.
R. Nobre, P. Pinto, T. Carvalho, J.M.P. Cardoso, and P.C. Diniz, On Expressing Strategies for Directive-Driven Multicore Programing Models. In Proceedings of Workshop on Parallel Programming and Run-Time Management Techniques for Many-core Architectures and Design Tools and Architectures for Multicore Embedded Computing Platforms (PARMA-DITAM '14). ACM, New York, NY, USA, 6 pages.
R. Couto, A.N. Ribeiro and J.C. Campos. A Study on the Viability of Formalizing Use Cases. In 9th International Conference on the Quality of Information and Communications Technology, QUATIC 2014, pages 130-133. IEEE. 2014. [PDF]
J.C. Campos, P. Masci, P. Curzon and M.D. Harrison. Layers, resources and property templates in the specification and analysis of two interactive systems. In Proceedings of the Workshop on Formal Methods in Human Computer Interaction (FoMHCI? ) 2015, pages 38-43. Universitätsbibliothek, RWTH Aachen University. 2015. [PDF]
J.C. Campos, M. Sousa, M. Alves and M.D. Harrison (2015) Formal Verification of a Space System's User Interface with the IVY workbench. IEEE Transactions on Human-Machine Systems. (early access)
R. Couto, A.N. Ribeiro and J.C. Campos (2015) The Modelery: A Model-Based Software Development Repository. International Journal of Web Information Systems, 11(2):205-225.
N. Macedo, A. Cunha, T. Guimarães. Exploring Scenario Exploration. In Fundamental Approaches to Software Engineering, Volume 9033 of Lecture Notes in Computer Science, pp 301-315. Springer, 2015.
M.D. Harrison, P. Masci, J.C. Campos and P. Curzon. Demonstrating that medical devices satisfy user related safety requirements. In Foundations of Health Information Engineering and Systems, Lecture Notes in Computer Science. Springer. (in press)
G. Ferro, R. Silva, and L. Lopes. “Towards Out-of-the-Box Programming for Wireless Sensor Networks,” in 18th IEEE International Conference on Computational Science and Engineering (CSE 2015), IEEE Press, Porto, Portugal, 2015.
João Bispo, Luís Reis, and João M. P. Cardoso, “Techniques for efficient MATLAB-to-C compilation,” In Proceedings of the 2nd ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming (ARRAY 2015). ACM, New York, NY, USA, 7-12.
Ricardo Nobre, Luiz Martins and João M.P. Cardoso, “Use of Previously Acquired Positioning of Optimizations for Phase Ordering Exploration,” in 18th International Workshop on Software and Compilers for Embedded Systems (SCOPES’15), June 1-3, 2015, Schloss Rheinfels, St. Goar, Germany. ACM, New York, NY, USA, pp. 58-67.
João Bispo, Luís Reis, João M. P. Cardoso, “C and OpenCL? Generation from MATLAB,” in 30th ACM Symposium on Applied Computing (SAC 2015), Apr. 13-17, 2015, Salamanca, Spain, ACM Press, 2015.
Nuno Paulino, João Canas Ferreira, João Bispo, and João M. P. Cardoso, “Transparent Acceleration of Program Execution using Reconfigurable Hardware,” in Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE '15), Hot Topic - Transparent use of accelerators in heterogeneous computing systems, Grenoble, France, Mar 9-13, 2015.. EDA Consortium, San Jose, CA, USA, pp. 1066-1071.
Master courses in Computer science at Minho University are built upon the concept of a specialisation course.
Each of these corresponds to a half-time academic year (30 ECTS), 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.
HASLab group members are involved in the following courses:
New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709–728, WSP Company. DOI: 10.1142/S0129054113400145New Paper: H.D. Macedo and J.N. Oliveira. Typing Linear Algebra: a Biproduct-oriented Approach. SCP 78:11, pp.2160-2191 (DOI 10.1016/j.scico.2012.07.012)
New Paper: J.C. Campos and J. Machado, A Specification Patterns System for Discrete Event Systems Analysis, Int. J. Adv. Robotic Systems, vol. 10, 2013, doi:110.5772/56412Job Opportunities: We are opening five post-doctoral positions. Details hereNew Paper: José N. Oliveira, Miguel A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15
New Paper: Nuno Macedo and Alcino Cunha: Implementing QVT-R Bidirectional Model Transformations using Alloy. Accepted at FASE'13.
New Paper: Shin-Cheng Mu, J.N. Oliveira. Programming from Galois connections. The Journal of Logic and Algebraic Programming 81 (2012) 680–704 (DOI 10.1016/j.jlap.2012.05.003).
New Position:Hugo Macedo is since this month (Jan. 2013) a post-doct at Deducteam in Paris.
New Paper: J.N. Oliveira. Towards a Linear Algebra of Programming. Formal Aspects of Computing (2012) 24: 433–458 (DOI 10.1007/s00165-012-0240-9)
New Position:Hugo Macedo is since this month (Apr. 2012) an Invited Researcher at LIAFA in Paris.
New Paper:Formal analysis of Ubiquitous Computing environments through the APEX framework, J.L. Silva, J.C. Campos and M.D. Harrison. In the proceedings of EICS'12, Copenhagen, Denmark, June 25-28, 2012 (to appear).
Software: Just released the latest version of the AlloyMDA tools, for bidirectional transformation between Alloy and UML class diagrams annotated with OCL.
New Paper:Towards an Evaluation of Bidirectional Model-driven Spreadsheets, J. Cunha, J.P. Fernandes, J. Mendes and J. Saraiva. In the proc. of USER'12, an ICSE'12 Workshop, Zurich, Switzerland, June 5, 2012 (to appear).
New Poster:A Bidirectional Model-driven Spreadsheet Environment, J. Cunha, J. Paulo Fernandes, J. Mendes and J. Saraiva. In the Posters Session of ICSE'12, Zurich, Switzerland, June 2-9, 2012 (to appear).
New Paper:Program and Aspect Metrics for Matlab, P. Martins, P. Lopes, J. Paulo Fernandes, J. Saraiva and J. Cardoso. In the proceedings of the ICCSA'12, Salvador da Bahia, Brasil, June 18-21, 2012 (to appear).
New Paper:Towards a Catalog of Spreadsheet Smells, J. Cunha, J. Paulo Fernandes, H. Ribeiro, J. Saraiva. In the proceedings of the The 12th International Conference on Computational Science and Its Applications (ICCSA'12), Salvador de Bahia, Brazil, June 18-21, 2012 (to appear).
New Paper:Bidirectional Transformation of Model-Driven Spreadsheets, J. Cunha, J. Paulo Fernandes, J. Mendes, H. Pacheco and J. Saraiva. In the proceedings of the 5th International Conference on Model Transformation (ICMT'12), Prague, Czech Republic, 28–29 May 2012 (to appear).
New Paper:MDSheet, A Framework for Model driven Spreadsheet Engineering, J. Cunha, J. Paulo Fernandes, Jorge Mendes and João Saraiva. In the proceedings of the 34th International Conference on Software Engineering 2012 (ICSE'12, Formal demonstration), Zurich, Switzerland, June 2-9, 2012 (to appear).
New Paper:From Relational ClassSheets to UML+OCL, J. Cunha, J. Paulo Fernandes and J. Saraiva. In the proceedings of the Software Engineering Track at the 27th Annual ACM Symposium On Applied Computing (SAC 2012), Riva del Garda (Trento), Italy, March 2012 (to appear).
New Paper:Alloy Meets the Algebra of Programming: A Case Study. By J.N. Oliveira and M. Ferreira. IEEE Transactions on Software Engineering, 2012.
Visit: The SAB/Scientific Advisory Board of INESC TEC visited HASLab on 30-Jan - see BIP 124.
Award: HASLab post-doc fellow Alexandra Silva was awarded the IBM Scientific Prize 2011 for her work on Kleene Coalgebra. The ceremony took place on 18th October 2011 at Universidade do Minho.
Workshop: A research workshop to celebrate the awarding of the IBM Scientific Prize 2010 to Alexandra Silva and launching the new QAIS project will take place next Monday, 17 October (details).
New project: FATBIT (Foundations, Applications and Tools for Bidirectional Transformation) recommended for funding by FCT (73K).
New project: Qais (Quantitative Analysis of Reactive Systems) recommended for funding by FCT (105K).
New project: APEX (Agile Prototyping for user EXperience) will develop a software framework enabling rapid prototyping of ubiquitous systems. Developers and users will be able to navigate simulations of built environments to develop an impression of what it will be like to use the final system once fielded.
New Paper:Bigraphical Modelling of Architectural Patterns. By A. Sanchez, L. S. Barbosa and D. Riesco, accepted at FACS'11.
New Paper:The role of coordination analysis in software integration projects. By N. Rodrigues, N. Oliveira and L. S. Barbosa, accepted at EI2N'11.
New Paper:Hybrid specification of reactive systems: An institutional approach. By A. Madeira, J. M. Faria, M. A. Martins and L. S. Barbosa, accepted at SEFM'11.
New Paper:Hybridization of Institutions. By M. A. Martins, A. Madeira, R. Diaconescu and L. Barbosa, accepted at CALCO'2011.
Award: HASLab paper Worldwide Consensus wins the Best Paper award at DisCoTec'11.
New Paper:Programming from Galois connections. By Shin-C. Mu and J.N. Oliveira. In LNCS Vol.6663, June 2011. Follow a discussion on this paper visit Shin's research blog.
Award: HASLab/MAPi PhD student Nuno Castro wins the Google sponsored Best Student Paper award at SDM'2011.
New Paper:Safe Controllers Design for Industrial Automation Systems. By Machado et al. Computers & Industrial Engineering, 60(4):635-653, May 2011.
March 12, 2011
New book: Rigorous Software Development - An Introduction to Program Verification, by HASLab members J.B. Almeida, M.J. Frade, J.S. Pinto and S. Melo de Sousa.
'Cum laude' award: HASLab external student Alexandra Silva was awarded the "cum laude" mention for her doctoral thesis on Kleene Coalgebra, on Dec., 21st, 2010, at Radboud Universiteit Nijmegen. more...
This distinction is only given in the NL in very exceptional cases (less then 5% of all possible candidates). It requires the explicit support of the thesis committee as well as of two other experts in the area (in this case Samson Abramsky, Oxford, and Larry Moss, Indiana). During the committee meeting, Dexter Kozen gave the following justification for his own vote (quoted from memory): "in very rare occasions a doctoral thesis and defense changes the way one sees his own main research area: this was such an occasion and that is all I have to say". Congratulations, Alexandra!
December 22, 2010
New project: APEX proposal recommended for funding by FCT. more...
APEX (Agile Prototyping for user EXperience) will develop a software framework enabling rapid prototyping of ubiquitous systems. Developers and users will be able to navigate simulations of built environments to develop an impression of what it will be like to use the final system once fielded.
September 3, 2010
Paper accepted at OPENCERT'10: J.C. Silva, J.C. Campos, J. Saraiva. GUI Inspection from Source Code Analysis
July 28, 2010
Paper accepted at HCSE'10: J.L. Silva, Ó.R. Ribeiro, J.M. Fernandes, J.C. Campos, M.D. Harrison. The APEX framework: prototyping of ubiquitous environments based on Petri nets
July 22, 2010
Paper accepted at ESORICS'10: J. Almeida, E. Bangerter, M. Barbosa, S. Krenn, A. Sadeghi, T. Schneider. A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Σ-Protocols
June 15, 2010
Paper accepted at FLACOS'10: D. da Cruz, P. R. Henriques, and J. S. Pinto. Contract-based slicing
June 1, 2010
Paper accepted at SEFM'10: J. Barros, D. da Cruz, P. R. Henriques, and J. S. Pinto. Assertion-based Slicing and Slice Graphs.
June 1, 2010
Paper accepted at EICS'10: J.C. Silva et al. The GUISurfer tool: towards a language independent approach to reverse engineering GUI code.
Apr 8, 2010
Talk by Daniel Seidel (Univ. Bonn) today: "Strictification of Circular Lazy Programs in a Calculational Form"
Apr 7, 2010
Just published in "Science of Computer Programming": N. F. Rodrigues and L. S. Barbosa. Slicing for Architectural Analysis.
Mar 20, 2010
Paper accepted at MPC'10: H.D. Macedo and J.N. Oliveira. Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra.
Feb 20, 2010
Paper accepted at MPC'10: Hugo Pacheco and Alcino Cunha. Generic Point-Free Lenses.
Feb 20, 2010
New project: GWS - providing consultancy in the development of Cachapuz's next generation software development framework. J.C. Campos (HASLab) and A.N. Ribeiro.
Feb 10, 2010
Paper accepted at Ada-Europe'2010: Program Verification in SPARK and ACSL: A Comparative Case Study by E. Brito and J. Sousa Pinto
Feb 1, 2010
EASST Best Paper Award at FMICS'09 to J. Bacelar Almeida, M. Barbosa, J. Sousa Pinto, and B. Vieira, for their paper Verifying Cryptographic Software Correctness with Respect to Reference Implementations.
New Paper:Bringing Class Diagrams to Life. By Luis Barbosa and Sun Meng.
In Springer Journal in Innovations in Systems and Software Engineering (forthcoming).
Nov 10, 2009 1:40 AM
New Paper:Towards the introduction of Qos information in a Component Model. By Sun Meng, Luis Barbosa.
SAC'2010 Symp, Coordination track. Mar 2010.
Nov 10, 2009 1:40 AM
New Paper: Which Mathematics for the Information Society? by João Ferreira, Alexandra Mendes, Roland Backhouse, Luis Barbosa.
TFM Conference, Springer LNCS 5846. Nov, 2009.
Nov 10, 2009 1:40 AM
Two Papers at Refine'09: FMweek, Eindhoven, Nov. 2009.
César Rodrigues, José Nuno Oliveira, Luis Barbosa. "A single, complete rule for coalgebraic refinement".
Manuel Martins, Alexandre Madeira, Luis Barbosa. "Refinement by interpretation in a general setting"
The Refine Workshop, 2009, ENTCS (to appear).
Nov 10, 2009 1:40 AM
New Paper: Refinement by interpretation
Manuel Martins, Alexandre Madeira, Luis Barbosa. IEEE SEFM'2009. Nov, 2009.
Nov 10, 2009 1:40 AM
New Project: lab members participate in EFACEC's InPACT project.
lab 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 10, 2009 1:40 AM
Best paper at SBMF'09, VFS GC track:
Miguel Ferreira, José Nuno Oliveira. "An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model". In M.V. Oliveira and J. Woodcock, editors, SBMF, volume 5902 of LNCS, pages 153-169. Springer, 2009.
Aug 21, 2009
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
New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709–728, WSP Company. DOI: 10.1142/S0129054113400145
New Paper: H.D. Macedo and J.N. Oliveira. Typing Linear Algebra: a Biproduct-oriented Approach. SCP 78:11, pp.2160-2191 (DOI 10.1016/j.scico.2012.07.012)
New Paper: J.C. Campos and J. Machado, A Specification Patterns System for Discrete Event Systems Analysis, Int. J. Adv. Robotic Systems, vol. 10, 2013, doi:110.5772/56412
Job Opportunities: We are opening five post-doctoral positions. Details here
New Paper: José N. Oliveira, Miguel A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15
HASLab is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of Scimago IBE ranking. We are part of the INESC TEC Associate Laboratory. Braga is very close to the Peneda-Gerês Natural Park, and has good connections to Porto (and its vibrant cultural life) and the International Airport (30 min shuttle bus to Braga). It also has a very competitive cost of living in comparison to other European cities.
Algorithms and tools for mutable data aggregation and monitoring.
BIM-2013_BestCase_RL3.2_UMINHO
Reliable data management of large volumes of data for storage and analytic processing
BIM-2013_BestCase_RL5.1_UMINHO
Secure broadcast and data management protocols for smartgrids
BIM-2013_BestCase_RL8.1_UMINHO
Tools for the formal verification of critical interactive systems through model checking and theorem proving
BIM-2013_BestCase_RL8.2_UMINHO
The role of different verification tools – software model checkers, timed model checkers, theorem provers – in the verification of real time software applied to critical systems
Additionally, the group is currently offering the following opportunities to PhD candidates, in the context of the MAPi doctoral programme. Some of these provide project-supported funding for the first year of the programme as indicated; funding for the remaining years should be obtained by applying to an FCT grant.
Verification and Validation of Software Systems for Space Projects (IAE/AEB, 2010-12) (Verificação e Validação de Sistemas de Software para Projetos Espaciais - a project of the Brazilian Institute of Aeronauitcs and Space where José Campos acts as a Consultant)
Software technology is pre-scientific in its lack of an effective basis for predicting computers' behaviour. HASLab research aims at improving scientific standards in software design through rigorous methods and mathematical techniques.
HASLab researchers have a long tradition of linking their research to national and international industry partners, 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 (Ph.D and M.Sc) students.
In the period 2003-2008, the lab members have published around 80 research papers, and edited 6
volumes as program chairs. 10 doctoral theses were defended. The lab has also coordinated an international
ALFA network and participated in the TYPES and APPSEM II coordination actions, as well as in an FP7 project.
At the national level three FCT-funded projects were coordinated, together with a number of transfer projects.
Concerning the organisation of events, the highlight was the ETAPS conference, held in 2007.
HASLab "Tripod"
Formal methods
Dependable Distributed Systems
Cryptography & Information security
Research Topics
High-assurance Model-driven Software Engineering
Foundations for architectural design (service certification, dynamic reconfiguration and self-adaptability)
Formal verification of real-time Systems
Secure embedded systems (static ckecking of embedded systems against safety policies)
Theoretical Cryptography / Provable Security
Implementation, Verification, and Analysis of Cryptographic Software
Dependability of interactive systems (model checking-based analysis of interactive systems)
The goal is to advance the state of the art in dependable distributed data management and dependable distributed systems, in particular (i) developing replication protocols based on group communication for different circumstances, with performance and availability as main concerns; (ii) supporting optimistic replication with novel logical clock mechanisms; (iii) scaling data management in a cloud computing environment; and (iv) developing agreement protocols and highly scalable information dissemination/aggregation protocols.
Rui Carlos Oliveira
José Orlando Pereira
António Luís Sousa
Paulo Sérgio Almeida
Carlos Baquero
Victor Francisco Fonte
Information Security
HASLab researchers develop techniques for constructing formal arguments of security for cryptographic schemes and protocols, in particular (i) formalizing security models (goals and attack scenarios) suitable for practical applications; (ii) constructing security arguments to support new and existing protocols that are used in the real world without theoretical validation; (iii) developing formal verification tools that can be used to mechanically check theoretical security proofs at the highest levels of assurance. Enabling the use of cryptography in new application scenarios and computing paradigms, both in terms of the necessary functionality and efficient implementation, by pursuing the development of domain-specific software development tools for cryptography.
José Bacelar Almeida
Manuel Bernardo Barbosa
José Esgalhado Valença
Fault Detection
Statistics-based approaches take as their only input dynamic information collected at run-time (such as component involvement in the execution of a test case), using no prior knowledge of the system under analysis. Such approaches have therefore intrinsically no modeling costs attached. Amongst the best statistical approaches in terms of diagnostic cost/performance ratio are those based on the computation of a statistical similarity between component activity and failure behavior using a so-called similarity coefficient s, which we refer to as spectrum-based fault localization (SFL). Component activity is recorded as program spectra (collected in a matrix A), and information on whether each of the program spectra in A corresponds to a passed of failed execution is collected in a vector e. The diagnostic process can be explained as (A, e) ---s---> D, where D is the yielded diagnostic report. SFL is a light-weight approach since for each component only a similarity coefficient (scalar operation) has to be computed, after which the M components in the system are sorted into D in order of likelihood to be at fault. Besides, dynamically collecting (A, e) requires only marginal overhead.
J.N. Oliveira, M.A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15
Shin-Cheng Mu, J.N. Oliveira. Programming from Galois connections. The Journal of Logic and Algebraic Programming 81 (2012): 680–704 (DOI 10.1016/j.jlap.2012.05.003).
Filippo Bonchi, Marcello Bonsangue, Michele Boreale, Jan Rutten and Alexandra Silva. A coalgebraic perspective on linear weighted automata. In Information and Computation, vol. 211, pp. 77-105, 2012.
J.N. Oliveira. Towards a Linear Algebra of Programming. Formal Aspects of Computing (2012) 24: 433–458 (DOI 10.1007/s00165-012-0240-9)
Alípio Mário Jorge, Paulo J. Azevedo: Optimal leverage association rules with numerical interval conditions. Intell. Data Anal. 16(1): 25-47 (2012)
Nuno Castro and Paulo J. Azevedo. Significant Motifs in Time Series. in Statistical Analysis and Data Mining, Volume 5, Issue 1, pages 35–53, February 2012, John Wiley and Sons.
M. A. Martins, A. Madeira, L. S. Barbosa. A coalgebraic perspective on logical interpretation. Studia Logica, Springer (accepted, September 2011)
J. Bacelar Almeida, Manuel Barbosa, Jorge S. Pinto, Bárbara Vieira. Formal Verification of Side Channel Countermeasures Using Self-Composition. Science of Computer Programming (accepted, available on-line, 2011).
Alberto Pardo, João Paulo Fernandes, João Saraiva. Shortcut Fusion Rules for the Derivation of Circular and Higher-order Programs, Accepted for publication at the Journal Higher-Order and Symbolic Computation (HOSC), ISSN 1388-3690, pages 1-35, Springer.
José Bernardo Barros, Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto: Assertion-based slicing and slice graphs. Formal Asp. Comput. 24(2): 217-248 (2012)
Luciana Lopes Freire, Pedro Miguel Arezes and José Creissac Campos. A literature review about usability evaluation methods for e-learning platforms. Work: A Journal of Prevention, Assessment and Rehabilitation, Volume 41, Supplement 1, pp. 1038-1044, 2012.
Carlos Baquero, Paulo Sérgio Almeida, Raquel Menezes. Extrema Propagation: Fast Distributed Estimation of Sums and Network Sizes. IEEE Transactions on Parallel and Distributed Systems, July 2011. IEEE computer Society Digital Library.
Di Jin, Bo Yang, Carlos Baquero, Dayou Liu, Dongxiao He, Jie Liu.Markov random walk under constraint for discovering overlapping communities in complex networks. Journal of Statistical Mechanics: Theory and Experiment (JSTAT). IOP Science, May 2011.
M. J. Frade, J. S. Pinto. Verification Conditions for Source-level Imperative Programs. In Computer Science Review, Volume 5, Issue 3, pp. 252-277, 2011. Elsevier. DOI: 10.1016/j.cosrev.2011.02.002
Alcino Cunha and Joost Visser: Transformation of Structure-Shy Programs with Application to XPath Queries and Strategic Functions, In Science of Computer Programming, 76(6):516-539. Elsevier, 2011.
J. Machado, E. Seabra, J.C. Campos, F. Soares, C. Leão. Safe Controllers Design for Industrial Automation Systems. Computers and Industrial Engineering. 60(4): 635-653 (2010)
Nuno Rodrigues, Luís Soares Barbosa: Slicing for architectural analysis. Sci. Comput. Program. 75 (10): 828-847 (2010)
Sun Meng, Luís Soares Barbosa: Bringing Class Diagrams to Life. ISSE (Jour. Innovations in Systems and Software Engineering, Springer). 6 (1-2): 91-98 (2010)
Paulo J. Azevedo, Alípio Mário Jorge: Ensembles of jittered association rule classifiers. Data Min. Knowl. Discov. 21(1): 91-129 (2010)
Paulo J. Azevedo: Rules for contrast sets. Intell. Data Anal. 14(6): 623-640 (2010)
Selected Conference Papers
F. Maia, M. Matos, J. Pereira, and R. Oliveira. Worldwide consensus. In Distributed Applications and Interoperable Systems (DAIS, with DisCoTec), number 6723 in LNCS, 2011. DisCoTec'2011 Best Paper Award.
Nuno C. Castro and Paulo Azevedo: Time Series Motifs Statistical Significance. Best Student Paper Award, SIAM SDM 2011.
M.A. Ferreira, J.N. Oliveira: An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model. Best paper in the GC track of SBMF 2009.
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira. Verifying Cryptographic Software Correctness with Respect to Reference Implementations. Best paper Award in FMICS 2009.
José Creissac Campos, Michael D. Harrison: Systematic Analysis of Control Panel Interfaces Using Formal Tools. DSV-IS 2008 (BCS HCI International Excellence Award 2009).
A model is (for purposes of this talk) an abstract, usually graphical, representation of some aspect of a software-intensive system. Software engineering has, since its invention, involved the use of models. In recent decades, a perceived need for greater automation of processes in software engineering, the wish to develop software faster and more cheaply, and the drive for higher quality have motivated ever more reliance on models. Languages for modelling and techniques for working with models have struggled to keep pace, hindered in some cases by conflicting requirements arising from the different motivations. We are currently in a dangerous state in which models sometimes endanger rather than support the developers' aims. I will explain some of the problems, and discuss the progress that I think we will/may/should/must/cannot expect to see in the coming years.
Keywords: tba
Slides: tba
Lightning Talk 1 (5 min.): tba
Lightning Talk 2 (5 min.): tba
19th of June, 2013
Towards fully trustworthy and cross domain safety engineering
Safety engineering standards are amongst the best practice examples on how systems engineering should be done. Nevertheless, these standards are very heuristic, complex to apply and different from domain to domain. The top level requirement for safety critical systems is the SIL, or Safety Integrity Level, but the way it is defined and quantified differs also from domain to domain and is hence the reason why cross-domain reuse of safety process artefacts and components is very difficult, often even impossible. We argue that a better criterion is to use QoS (Quality of Service) as this expresses the point of view of the user in terms of trustworthiness, independently of the domain. The cross domain reuse as goal is also hampered by the way the SIL level is obtained with SIL as such is a system specific property. This is in contrast with the engineering practice to reuse components whenever possible. Altreonic defined a new criterion called ARRL (Assured Reliability and Resilience Level) that can be used to guide the architectural design and validation. The ARRL criterion takes into account the functional properties when faults occur. It complements the SIL criterion similarly like a HARA and FMEA complement each other. It also allows to define rules whereby components are assembled in a system to meet a corresponding SIL level, hence allowing composable safety. The ARRL criterion is also the driving criterion behind the R&D roadmap of Altreonic. This will briefly be illustrated by the formal development of the network-centric OpenComRTOS and by the development of the traceability and requirements driven metamodel behind the GoedelWorks project portal. The latter will use a generic process pattern. The combination of OpenComRTOS Designer and GoedelWorks portal provides for cross domain and cost efficient support for safety and systems engineering.
Distributed transaction processing has benefited greatly from optimistic concurrency control protocols thus avoiding costly fine-grained synchronization. However, the performance of these protocols degrades significantly when the workload increases, namely, by leading to a substantial amount of aborted transactions due to concurrency conflicts. Our approach stems from the observation that the abort rate increases with the load as already executed transactions queue for longer periods of time waiting for their turn to be certified and committed. We thus propose an adaptive algorithm for judiciously scheduling transactions to minimize the time during which these are vulnerable to being aborted by concurrent transactions, thereby reducing the overall abort rate. We do so by throttling transaction execution using an adaptive mechanism based on the locally known state of globally executing transactions, that includes out-of-order execution.Our evaluation using traces from the industry standard TPC-E workload shows that the amount of aborted transactions can be kept bounded as system load increases, while at the same time fully utilizing system resources and thus scaling transaction processing throughput.
Interaction constraints are an expressive formalism for describing coordination patterns, such as those underlying the coordination language Reo, that can be efficiently implemented using constraint satisfaction technologies such as SAT and SMT solvers. Existing implementations of interaction constraints interact with external components only in a very simple way: interaction occurs only between rounds of constraint satisfaction. What is missing is any means for the constraint solver to interact with the external world during constraint satisfaction.This work introduces interactive interaction constraints which enable interaction during constraint satisfaction, and in turn increase the expressiveness of coordination languages based on interaction constraints by allowing a larger class of operations to be considered to occur atomically. We describe how interactive interaction constraints are implemented and detail a number of strategies for guiding constraint solvers. The benefit of interactive interaction constraints is illustrated using small examples. From a general perspective, our work describes how to open up and exploit constraint solvers as the basis of a coordination engine.
Statically enforcing complex invariants in structured documents
Dario Teixeira
Lambdoc is an open-source library offering support for semantically rich structured documents in web applications [1]. It is particularly aimed at web sites that accept user-contributed content and wish to ensure that such content follows strict guidelines regarding soundness and typographic conventions. This talk consists of two parts. The first part provides the context and motivation for the Lambdoc library, together with a brief overview of its features. The second part comprises the bulk of the talk, and discusses the application of the type system of statically typed functional languages such as OCaml and Haskell to enforce complex invariants on document structure. This latter discussion takes the form of a journey, which begins with Phantom Types and ends with Generalized Abstract Data Types (GADTs). Each of these concepts is briefly introduced and its strengths and weaknesses in a practical setting evaluated. Note that the presentation focuses mainly on the OCaml language. However, given the prevalence of Haskell in academia, a brief "OCaml for Haskellers" overview is also provided. Moreover, the OCaml code samples are simple enough to be understandable by anyone with some familiarity with Haskell or any other functional language with parametric polymorphism and algebraic data types.
NoSQL databases manage the bulk of data produced by modern Web applications such as social networks. This stems from their ability to partition and spread data to all available nodes, allowing NoSQL systems to scale. Unfortunately, current solutions’ scale out is oblivious to the underlying data access patterns, resulting in both highly skewed load across nodes and suboptimal node configurations. In this paper, we first show that judicious placement of HBase partitions taking into account data access patterns can improve overall throughput by 35%. Next, we go beyond current state of the art elastic systems limited to uninformed replica addition and removal by: i) reconfiguring existing replicas according to access patterns and ii) adding replicas specifically configured to the expected access pattern. MET is a prototype for a Cloud-enabled framework that can be used alone or in conjunction with OpenStack for the automatic and heterogeneous reconfiguration of a HBase deployment. Our evaluation, conducted using the YCSB workload generator and a TPC-C workload, shows that MET is able to i) autonomously achieve the performance of a manual configured cluster and ii) quickly reconfigure the cluster according to unpredicted workload changes.
Hugo Pacheco (National Institute of Informatics (NII), Tóquio, Japão)
Bidirectional transformations and in particular lenses, programs with a forward get transformation and a backward putback transformation, are routinely written in ways that do not let programmers specify their behavior completely. Several bidirectional programming languages exist to aid programmers in writing a (usually simpler) forward transformation, and deriving a backward transformation for free. However, the maintainability offered by such languages comes at the cost of expressiveness because the ambiguity of synchronization – handled by the putback transformation – is solved by default strategies which are hidden from programmers. In this paper, we argue that such ambiguity is essential for bidirectional transformations and propose a novel putback-based bidirectional language in which programmers write putback synchronization strategies from the start. In sharp contrast with traditional get-based languages, our putback-based language allows programmers to describe the behavior of a bidirectional transformation completely, while retaining the maintainability of writing a single program. We demonstrate that this additional power is manageable in practice through a series of examples, ranging from simple ones that illustrate traditional lenses to complex ones for which our putback-based approach is central to specifying their non-trivial update strategies. Our examples are inspired by existing problems from the functional and database programming fields.
Large-scale distributed systems appear as the major infrastructures for supporting planet-scale services. These systems call for appropriate management mechanisms and protocols. Slicing is an example of an autonomous, fully decentralized protocol suitable for large-scale environments. It aims at organizing the system into groups of nodes, called slices, according to an application-specific criteria where the size of each slice is relative to the size of the full system. This allows assigning a certain fraction of nodes to different task, according to their capabilities. Although useful, current slicing techniques lack some features of considerable practical importance. This paper proposes a slicing protocol, that builds on existing solutions, and addresses some of their frailties. We present novel solutions to deal with non-uniform slices and to perform online and dynamic slices schema reconfiguration. Moreover, we describe how to provision a slice-local Peer Sampling Service for upper protocol layers and how to enhance slicing protocols with the capability of slicing over more than one attribute. Slicing is presented as a complete, dependable and integrated distributed systems primitive for large-scale systems.
Keywords: tba
Slides: tba
20th of March, 2013
On the semantic security of functional encryption schemes
Functional encryption (FE) is a powerful cryptographic primitive that generalizes many asymmetric encryption systems proposed in recent years. Syntax and security definitions for FE were proposed by Boneh, Sahai, and Waters (BSW) (TCC 2011) and independently by O’Neill (ePrint 2010/556). In this paper we revisit these definitions, identify several shortcomings in them, and propose a new definitional approach that overcomes these limitations. Our definitions display good compositionality properties and allow us to obtain new feasibility and impossibility results for adaptive token-extraction attack scenarios that shed further light on the potential reach of general FE for practical applications.
Non-trivial bidirectional transformations (BXs) are inherently ambiguous, as there are in general many different ways to consistently translate an update from one side to the other. Existing BX languages and frameworks typically satisfy only fundamental first principles which ensure acceptable and stable (well-behaved) translation. Unfortunately, these requirements give little insight about how a particular update translation is chosen among the myriad possible. From the user perspective, such unpredictability may hinder the adoption of BX frameworks. This problem can be remedied by imposing a "principle of least change": in a state-based framework this amounts to translating updates so that the result is as close as possible to the original state according to some distance measure. In this paper we start by formalizing such BXs, focusing on the particular framework of lenses. We then discuss whether such least-change lenses can be defined by composition, an essential construct of BX frameworks. For sequential composition, we present two (dual) update translation alternatives: a classical deterministic one and a nondeterministic one where composition may require backtracking. A key ingredient of our paper is the reasoning style which, carried out in relational algebra, achieves elegant formalizations and exposes several similarities and dualities.
Keywords: Bidirectional Transformations, Lenses
Slides: tba
27th of February, 2013
Implementing QVT-R Bidirectional Model Transformations using Alloy
QVT Relations (QVT-R) is the standard language proposed by the OMG to specify bidirectional model transformations. Unfortunately, due to ambiguities in its original semantics, acceptance and development of effective tool support has been slow. Although the bidirectional check semantics have been clarified recently, none of the existing QVT-R tools have been shown to correctly implement it. Even worst, many tools do not even comply to the standard language, none supports OCL constraints over the meta-models (thus being prone to return ill-formed models), and none clearly formalizes how enforce semantics picks a target model from the myriad consistent candidates. In this paper we propose a QVT-R tool that overcomes all these issues: it supports a large subset of QVT-R and UML class diagrams annotated with OCL, complies to the bidirectional check semantics of [1], and enforces update propagation according to the predictable ``principle of least change''. We achieve this by embedding both QVT-R transformations and UML class diagrams (annotated with OCL) in Alloy, a lightweight formal specification language with support for automatic model finding via SAT solving. The proposed tool already proved effective in debugging existing transformations, namely unveiling several errors in the well-known object-relational mapping that illustrates OMG's QVT-R specification.
Just Do It While Compiling! Fast Extensible Records In Haskell
Alberto Pardo (Instituto de Computacion, Universidad de la Republica, Montevideo, Uruguay)
The library for strongly typed heterogeneous collections HList provides an implementation of extensible records in Haskell that needs only a few common extensions of the language. In HList, records are represented as linked lists of label-value pairs with a lookup operation that is linear-time in the number of fields. In this paper, we use type-level programming techniques to develop a more efficient representation of extensible records for HList. We propose two internal encodings for extensible records that improve lookup at runtime without needing a total order on the labels. One of the encodings performs lookup in constant time but at a cost of linear time insertion. The other one performs lookup in logarithmic time while preserving the fast insertion of simple linked lists. Through staged compilation, the required slow search for a field is moved to compile time in both cases. This is a joint work with Bruno Martinez and Marcos Viera recently presented at PEPM 2013.
Slides: tba
6th of March, 2013
Exceptionally, this seminar will take place in the Physics Department at 14:30h.
The logic of non-locality and quantum informatics
Rui Soares Barbosa (Department of Computer Science - University of Oxford)
tba
Keywords: tba
Slides: tba
12th of December, 2012
Clouder: A Flexible Large Scale Decentralized Object Store
Large scale data stores have been initially introduced to support a few concrete extreme scale applications, such as social networks. Their scalability and availability requirements often sacrifice richer data and processing models, and even elementary data consistency. In strong contrast with traditional relational databases (RDBMS), large scale data stores present very simple data models and APIs, lacking most of the established relational data management operations, and presenting relaxed consistency guarantees, providing eventual consistency. This thesis aims at reducing the gap between traditional RDBMS and large scale data stores by seeking mechanisms to provide additional consistency guarantees, and higher-level data processing primitives in large scale data stores. The devised mechanisms should not hinder the scalability and dependability of large scale data stores. Regarding higher-level data processing primitives, this thesis explores two complementary approaches: extending data stores with additional operations such as general multi-item operations; and coupling data stores with other existing processing facilities without hindering scalability. We demonstrate our approaches with running prototypes and extensive experimental evaluation using proper workloads.
Keywords: tba
Slides: tba
Lightning Talk 1 (5 min.): tba
Lightning Talk 2 (5 min.): tba
5th of December, 2012
Calculating Fault Propagation in Functional Programs using the Linear Algebra of Programming (LAoP)
How do software faults propagate in computer programs/systems? Can faulty behavior be predicted in some way, eg. by calculation? Are there versions of the same program / software system which are "better" than others concerning fault propagation? This talk will not provide definite answers to these questions but it will point towards a strategy to handle them. First, faulty behavior can be mimicked probabilistically, and faults can be injected and simulated using monadic programming (see eg. the Probabilistic Functional Programming - PFP library developed in Haskell by M. Erwig). Second, rather than observing propagation patterns by repeated simulation, such programs can be converted into isomorphic matricial versions and reasoned about in the so-called Linear Algebra of Programming (LAoP), an extension of the AoP towards quantitative reasoning. Simple examples (such as those given in eg. DOI: 10.1007/s00165-012-0240-9) show that faulty-program fusion can be calculated and the way faults combine with each other can be expressed using probabilistic (choice) combinators. Future work includes extending the approach to component-oriented software systems modeled as co-algebras of functors involving the distribution monad, thus scaling up from functional programs to software architectures.
HCI for Safety Critical Interactive Applications: Commonalities and Differences between Air Traffic Control, Satelite Ground Segments and Large Civil Aircrafts Cockpits
Philippe Palanque (IRIT, Toulouse)
Recent years have seen an increasing use of sophisticated interaction techniques in the field of command and control systems. The use of such techniques has been required in order to increase the bandwidth between the users and the systems and thus to help them deal efficiently to increasingly complex systems. These techniques come from research and innovation done in the field of HCI but very little has been done to improve their reliability and their tolerance to human error. It can be difficult to know how to assess the risks that such systems can create for the successful operation of safety-critical systems. One consequence of this is that interaction issues are almost entirely missing from international development standards in safety-critical systems, such as IEC615098 or DO 178B. This presentation will present lessons learnt over the last 20 years on developing research in HCI for safety critical interactive systems as well as applying the results in different application domains such as cockpits of large civil aircrafts, air traffic management and satellite ground segments.
Can GUI implementation markup languages be used for modelling?
Carlos E. Silva (HASLab)
The current diversity of available devices and form factors increases the need for model-based techniques to support adapting applications from one device to another. Most work on user interface modelling is built around declarative markup languages. Markup languages play a relevant role, not only in the modelling of user interfaces, but also in their implementation. However, the languages used by each community (modellers/developers) have, to a great extent evolved separately. This means that the step from concrete model to final interface becomes needlessly complicated, requiring either compilers or interpreters to bridge this gap. In this paper we compare a modelling language (UsiXML? ) with several markup implementation languages. We analyse if it is feasible to use the implementation languages as modelling languages.
Keywords: User Interfaces, Modelling, Markup languages
Slides: tba
10th of October, 2012
Dynamic contracts for verification and enforcement of real-time systems properties
André Pedro
Real-time systems are systems where clearly the runtime verification is indispensable, not only due to the high complexity which make static approaches practically unfeasible, but also due to their high dependence of temporal constraints (e.g., model checking -- where models becomes undecidable to check due to the time clock operations: addiction, subtraction by a constant, etc.). The research of techniques for such systems has been growing progressively along the past years due to high need of reliable and safe development complements and alternatives to static approaches. However, the trend towards the research of new dynamic approaches has been higher for soft real-time systems rather than for hard real-time systems (i.e., focusing essentially on the functional aspects). The talk presents briefly the underlying concepts of runtime verification, its motivation, and introduces a specification language prototype proposed by us for monitor generation as well as a practical case study, focusing on hard real-time embedded systems.
Keywords: tba
Slides: tba
26th of September, 2012
Extension and Implementation of ClassSheet Models
Jácome Cunha (HASLab)
In this talk we explore the use of models in the context of spreadsheet engineering. We review a successful spreadsheet modeling language, whose semantics we further extend. With this extension we bring spreadsheet models closer to the business models of spreadsheets themselves. An addon for a widely used spreadsheet system, providing bidirectional model-driven spreadsheet development, was also improved to include the proposed model extension.
Keywords: tba
Slides: tba
A Web Portal for the Certification of Open Source Software
Pedro Martins (HASLab)
In this talk we will present a web portal for the certification of open source software. The portal aims at helping programmers in the internet age, when there are (too) many open source reusable libraries and tools available. Our portal offers programmers a web-based and easy setting to analyze and certify open source software, which is a crucial step to help programmers choosing among many available alternatives, and to get some guarantees before using one piece of software. We will also present our first prototype of such web portal. We will describe in detail a domain specific language that allows programmers to describe with a high degree of abstraction specific open source software certifications. The design and implementation of this language is the core of the web portal.
Keywords: tba
Slides: tba
12th of September, 2012
Bidirectional Data Transformation by Calculation
Hugo Pacheco (HASLab)
The advent of bidirectional programming, in recent years, has led to the development of a vast number of approaches from various computer science disciplines. These are often based on domain-specific languages in which a program can be read both as a forward and a backward transformation that satisfy some desirable consistency properties. Despite the high demand and recognized potential of intrinsically bidirectional languages, they have still not matured to the point of mainstream adoption. This dissertation contemplates some usually disregarded features of bidirectional transformation languages that are vital for deployment at a larger scale. The first concerns efficiency. Most of these languages provide a rich set of primitive combinators that can be composed to build more sophisticated transformations. Although convenient, such compositional languages are plagued by inefficiency and their optimization is mandatory for a serious application. The second relates to configurability. As update translation is inherently ambiguous, users shall be allowed to control the choice of a suitable strategy. The third regards genericity. Writing a bidirectional transformation typically implies describing the concrete steps that convert values in a source schema to values a target schema, making it impractical to express very complex transformations, and practical tools shall support concise and generic coding patterns.
Keywords: Bidirectional Transformations, Data Calculation
Slides: tba
Evolution of Model-Driven Spreadsheets Spreadsheets
Jorge Mendes (HASLab)
Spreadsheets are the most used programming environment, mostly because they are very flexible. This is due to the lack of restrictions imposed on them which can lead to lots of errors. Model-Driven Engineering was already suggested to improve spreadsheets, providing them with specications and checking tools. However, users have to learn to use these tools on top of their existing spreadsheet host system.To remove that difficulty, the work for this thesis describes an embedding of spreadsheet models within spreadsheet themselves. Moreover, a set of operations that can be performed on these models and respective instances is defined. This way, users interact with models and spreadsheets in the same environment with the objective to improve work performance and reduce errors.Resulting from this work, a prototype was created and is also discussed in this dissertation. This prototype can be used to validate the approach taken in this thesis and to provide a base framework for future developments.
Designing interactive software for medical device user interfaces: case studies on drug infusion pumps
Paolo Masci (Queen Mary University of London)
This seminar will be of interest to anybody involved in the design or development of interactive systems. We will discuss some of our recent work carried out within the CHI+MED project (http://www.chi-med.ac.uk), where we integrate empirical approaches with mathematical methods to deliver a richer analysis of safety-critical interactive systems. We will focus on automated analysis of interactive software incorporated in infusion pumps --- interactive medical devices used in healthcare to deliver drugs and nutrients to patients. Case studies based on commercial infusion pumps will be presented. First, we present our recent work [1,2] on the verification of 'predictability', an interaction design principle that concerns the ability of a user to determine the outcome of future interactions. We will illustrate how: (i) precise insights can be gained about situations where interaction design seems awkward and may lead to use errors; (ii) verified solutions can be developed that fix the interaction design; (iii) simple user strategies can be identified that can be safely used to overcome identified issues in devices already on the market. Second, we present our on-going work on the UNI-Pump framework, a formal framework to support a uniform and rigorous approach for specifying and verifying safety requirements for interactive software incorporated in infusion pump user interfaces. This work aims to complement the Generic Infusion Pump (GIP) framework supported by the University of Pennsylvania and the FDA for model-driven development of software incorporated in infusion pumps. The existing GIP is restricted to software for the control logic of infusion pumps. It does not directly tackle interactive software for the user interface, which is also necessary to demonstrate device safety. The UNI-Pump framework addresses this gap. [1] P. Masci, R. Ruksenas, P. Curzon, et.al., "On formalising interactive number entry on infusion pumps.", ECEASST 45 (2011), available at http://www.eecs.qmul.ac.uk/~masci/ [2] P. Masci, R. Ruksenas, P. Curzon, et.al., "The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps.", submitted for publication to Innovations in Systems and Software Engineering (2012). Preprint available at http://tinyurl.com/masci-QMpreprints
Keywords: tba
Slides: tba
20th of June, 2012
Formal Verification of Cryptographic Software Implementations
We explore how formal techniques, namely deductive verification techniques, can be used to increase the guarantees that cryptographic software implementations indeed work as prescribed. First we identify relevant security policies that may be at play in cryptographic systems, as well as the language-based mechanisms that can be used to enforce such policies in those systems. We propose methodologies based on deductive verification to formalise and verify relevant security policies in cryptographic software. We also propose a deductive verification tool for a domain-specific language for cryptographic implementations, that can be used to verify the previously identified security policies. At the very end, we conclude our work by reasoning about the soundness of our verification tool.
Keywords: tba
Slides: tba
6th of June, 2012
Automatic parameter estimation of the iSAX time series representation
The key to scalable mining algorithms is to select a suitable representation of the data. From the existing techniques, the Symbolic Aggregate Approximation (SAX) has been widely used in the time series data mining community. Its popularity arises from the fact that it is symbolic, reduces the dimensionality of the series, allows lower bounding and is space efficient. However, the need to set the symbolic length and alphabet size parameters limits the applicability of the representation since the best parameter setting is highly application dependent. Typically, these are either set to a fixed value (e.g. 8) or experimentally probed for the best configuration. In this work, we aim to tackle this limitation by introducing a novel technique to automatically derive these parameters. The technique, referred as AutoiSAX, not only discovers the best parameter setting for each time series in the database but also finds the alphabet size for each iSAX symbol within the same word. It is based on the simple and intuitive ideas of time series complexity and segment standard deviation. The technique can be smoothly embedded in existing data mining tasks as an efficient sub-routine. We analyse the impact of using AutoiSAX in visualisation interpretability, and motif mining results. Our contribution aims to make iSAX a more general approach as it evolves towards a parameter-free method.
Keywords: tba
Slides: tba
23rd of May, 2012
Modelling and systematic analysis of interactive systems (tentative title)
In this talk I will address some of the more recent work on the modelling and systematic analysis of interactive system being done at HASLab. The main focus will be on ubiquitous computing system. The is the rehearsal of an invited talk to be given at QMUL the following week.
Keywords: tba
Slides: tba
9th of May, 2012
Strong Eventual Consistency for scalable distribution
In this presentation we establish the conditions for strong eventual consistent datatypes (with no rollback allowed) and present two equivalent implementation flavors: State Based, with a defined merge operation and constraints that ensure that mutating operations are compatible with merge; Operation Based, building on top of a causal delivery middleware and ensuring that concurrent operations commute. In particular, we will show Set implementations that match this design.
Slides: tba
28th of March, 2012
Middleware for the NOSQL generation: Challenges and opportunities
José Orlando Pereira (HASLab)
The middleware stack based on a relational database management system (RDBMS) has been the workhorse of the IT industry, incrementally extending the decades old RDBMS with concepts such as object-relational mapping, caching, sharding, and replication. More recently, there has been a growing shift towards the so called NoSQL databases, stemming mostly from the requirements of extremely large applications offered as services (SaaS), but also from novel platforms as a service (PaaS). By departing from the traditional architecture and interfaces of the venerable RDBMS, this movement shatters the foundation of database middleware stack. In this talk we start by examining the assumptions and goals of each layer in the the traditional stack, including the RDBMS. Then we re-evaluate those assumptions and goals in the context of a NoSQL database such as Cassandra or HBase. This leads us to discuss to what extent the role of the database has changed and what should now be expected from middleware. Although there is room for some of the traditional middleware concepts, there are others that have become obsolete, and also some new challenges and opportunities.
Keywords: tba
Slides: tba
21st of March, 2012
From Relational ClassSheets to UML+OCL
Jácome Cunha (HASLab)
Spreadsheets are among the most popular programming languages in the world. Unfortunately, spreadsheet systems were not tailored from scratch with modern programming language features that guarantee, as much as possible, program correctness. As a consequence, spreadsheets are populated with unacceptable amounts of errors. In other programming language settings, model-based approaches have been proposed to increase productivity and program effectiveness. Within spreadsheets, this approach has also been followed, namely by ClassSheets. In this paper, we propose an extension to ClassSheets to allow the specification of spreadsheets that can be viewed as relational databases. Moreover, we present a transformation from ClassSheet models to UML class diagrams enriched with OCL constraints. This brings to the spreadsheet realm the entire paraphernalia of model validation techniques that are available for UML.
Keywords: Spreadsheets, UML, OCL, ClassSheets
Slides: tba
14th of February, 2012
Robust Distributed Data Aggregation
Paulo Jesus (HASLab)
Distributed aggregation algorithms are an important building block of modern large scale systems, as it allows the determination of meaningful system-wide properties (e.g., network size, total storage capacity, average load, or majorities) which are required to direct the execution of distributed applications. In the last decade, several algorithms have been proposed to address the distributed computation of aggregation functions (e.g., COUNT, SUM, AVERAGE, and MAX/MIN), exhibiting different properties in terms of accuracy, speed and communication tradeoffs. However, existing approaches exhibit many issues when challenged in faulty and dynamic environments, lacking in terms of fault-tolerance and support to churn. This study details a novel distributed aggregation approach, named Flow Updating, which is fault-tolerant and able to operate on dynamics networks. The algorithm is based on manipulating flows (inspired by the concept from graph theory), that are updated using idempotent messages, providing it with unique robustness capabilities. Experimental results showed that Flow Updating outperforms previous averaging algorithms in terms of time and message complexity, and unlike them it self-adapts to churn and changes of the initial input values without requiring any periodic restart, supporting node crashes and high levels of message loss.
Keywords: Data aggregation, Distributed algorithms, Dynamic networks, Fault-tolerance
Slides: tba
22th of February, 2012
Subgroup Discovery driven by a user defined property of interest
Paulo Azevedo (HASLab)
In this talk I will describe a framework based on association rules for the discovery of pertinent subgroups of a population according to a defined property of interest. The main idea of subgroup mining is to identify the characteristics of subpopulations that deviate from the global population, according to a user defined property. This property can be represented by categorical values, numerical, a contrast (frequency comparison) or even a distribution. A classical application on census data identifies discrimination on wage for subgroups formed by females with low education when compared to the global population. Other example on medical data identifies characteristics of subgroups with abnormal distribution of the Cholesterol values when compared to the global population. Several instances of this framework will be described, like contrast sets mining, distribution rules and Distribution Learning.
Every transformation is a lens: Taming partiality using invariants and non-determinism
Nuno Macedo (HASLab)
Total well-behaved lenses are restricted to surjective functions. However, many useful transformations are not surjective. To support these, most lens frameworks relax the totality requirement and weaken the round-tripping laws, opening the door to unpredictable synchronization behaviors. We propose a framework where any transformation written in a point-free functional language can be lifted to a total well-behaved lens, by capturing the exact range and domain of the transformation as invariants on the target and source datatypes. To enforce such invariants, the proposed framework relies on non-deterministic execution of backward transformations. Both these and the data invariants are naturally specified using a point-free relational calculus that enables concise and agile algebraic reasoning.
Keywords: Bidirectional transformations, Point-free relational calculus, Data invariants, Non-determinism
Slides: tba
1st of February, 2012
Delegatable Homomorphic Encryption with Applications to Secure Outsourcing of Computation
Manuel Barbosa (HASLab)
In this work we propose a new cryptographic primitive called Delegatable Homomorphic Encryption (DHE). This allows a Trusted Authority to control/delegate the capability to evaluate circuits over encrypted data to untrusted workers/evaluators by issuing tokens. This primitive can be both seen as a public-key counterpart to Verifiable Computation, where input generation and output verification are performed by different entities, or as a generalisation of Fully Homomorphic Encryption enabling control over computations on encrypted data. Our primitive comes with a series of extra features as follows: 1) there is a one-time setup procedure for all circuits; 2) senders do not need to be aware of the functions which will be evaluated on the encrypted data, nor do they need to register keys; 3) tokens are independent of senders and receiver; and 4) receivers are able to verify the correctness of computation given short auxiliary information on the input data and the function, independently of the complexity of the computed circuit. We give a modular construction of such a DHE scheme from three components: Fully Homomorphic Encryption (FHE), Functional Encryption (FE), and a (customised) MAC. As a stepping stone, we first define Verifiable Functional Encryption (VFE), and then show how one can build a secure DHE scheme from a VFE and an FHE scheme. We also show how to build the required VFE from a standard FE together with a MAC scheme. All our results hold in the standard model. Finally, we show how one can build a verifiable computation (VC) scheme generically from a DHE. As a corollary, we get the first VC scheme which remains verifiable even if the attacker can observe verification results.
Implementing sound in a CAVE-like system while ensuring the “synchrony” of the virtual world
Carlos CL Silva (HASLab/LVP)
Although great developments have been made in the generation of ever more visually immersive virtual reality (VR) environments, audiovisual interactive VR environments are still conceived as an enormous challenge, mostly due to ignorance about some audiovisual processes, such as the audiovisual perception of synchrony. Psychophysically, audiovisual perception is still an intriguing phenomenon, especially when we think about time differences – both at the physical and neural level – underlying the perception of sound and light. Thus, in order to develop a truly immersive audiovisual VR environment we need to know how human beings deal with these differences and perceive synchrony between sound and image. This presentation intends to expose these problems and discuss possible solutions for the implementation process of an auditory VR environment in a CAVE-like system at the Laboratory of Visualization and Perception in the University of Minho. Moreover, we will explore this case as an example of the historical contribution of Psychology and Psychophysical research as a start and an ending point in the processes of developing technology for interactive VR environments.
Flow-Updating (FU) is a fault-tolerant technique that has proved to be efficient in practice for the distributed computation of aggregate functions in communication networks where individual processors do not have access to global information. Previous distributed aggregation protocols, based on repeated sharing of input values (or mass) among processors, sometimes called Mass-Distribution (MD) protocols, are not resilient to communication failures (or message loss) because such failures yield a loss of mass. In this paper, we present a protocol which we call Mass-Distribution with Flow-Updating (MDFU). We obtain MDFU by applying FU techniques to classic MD. We analyze the convergence time of MDFU showing that stochastic message loss produces low overhead. This is the first convergence proof of an FU-based algorithm. We evaluate MDFU experimentally, comparing it with previous MD and FU protocols, and verifying the behavior predicted by the analysis. Finally, given that MDFU incurs a fixed deviation proportional to the message-loss rate, we adjust the accuracy of MDFU heuristically in a new protocol called MDFU with Linear Prediction (MDFU-LP). The evaluation shows that both MDFU and MDFU-LP behave very well in practice, even under high rates of message loss and even changing the input values dynamically.
Slides: tba
21st of December, 2011
Translating Alloy Specifications to UML Class Diagrams Annotated with OCL
Ana Garis (HASLab/Universidad Nacional de San Luis, Argentina)
Model-Driven Engineering (MDE) is a Software Engineering approach based on model transformations at different abstraction levels. It prescribes the development of software by successively transforming models from abstract (specifications) to more concrete ones (code). Alloy is an increasingly popular lightweight formal specification language that supports automatic verification. Unfortunately, its widespread industrial adoption is hampered by the lack of an ecosystem of MDE tools. We present a model transformation between Alloy and UML Class Diagrams annotated with OCL. The proposed transformation enables current UML-based tools to also be applied to Alloy specifications, thus unleashing its potential for MDE.
Slides: tba
21st of December, 2011
Archery - Modelling of Architectural Patterns
Alejandro Sanchez (HASLab/Universidad Nacional de San Luis, Argentina)
In a number of contexts the term “architectural pattern” is used as an architectural abstraction. The expression is taken in the usual sense of pattern in object oriented programming - a known design solution to recurring problems. Available pattern catalogs allow to design and evolve architectures by applying them. However, its characterizations remain largely informal, enough to generate a vocabulary for design discussions at a high abstraction level, but insufficient to underpin, for instance, executable models. We describe Archery, a language for modelling of architectural patterns, supporting hierarchical composition and a type discipline. We provide formal semantics for the behavioural and structural dimensions by respective translations to mCRL2 and to bigraphical reactive systems.
Slides: tba
14th of December, 2011
Systems Biology, a holistic approach to the "algebra" of Life
Daniel Machado (IBB/CEB - UMinho)
The cell is the fundamental building block of life. From this basic unit, a myriad of life forms have emerged. Systems Biology is a recent field that studies the complex interactions that happen inside a cell. It represents a new holistic paradigm when compared to the traditional reductionist perspective to biology. The multidisciplinary nature of this field requires the integration of several areas such as computer science, mathematics, physics, chemistry, biology and systems engineering. Building a whole-cell model is its ultimate goal, hampered by the difficulty of "reverse engineering" the specification of a system that evolved in nature. Although still far from this goal, several models of different organisms have been built. These provide a platform for performing "in silico" experiments that allow us to understand the cellular behavior and also to predict the optimal manipulations towards a specific objective. Therefore, they have several applications in biomedical research for the study of diseases and novel drug discovery, as well as in industrial biotechnology for the creation of microbial cell factories that produce a wide range of commodity chemicals.
Slides: tba
7th of November, 2011
Experimental Evaluation of Distributed Middleware with a Virtualized Java Environment
The correctness and performance of large scale service oriented systems depend on distributed middleware components performing various communication and coordination functions. It is, however, very difficult to experimentally assess such middleware components, as interesting behavior often arises exclusively in large scale settings, but such deployments are costly and time consuming. We address this challenge with MINHA, a system that virtualizes multiple JVM instances within a single JVM while simulating key environment components, thus reproducing the concurrency, distribution, and performance characteristics of the actual system. The usefulness of MINHA is demonstrated by applying it to the WS4D Java stack, a popular implementation of the Devices Profile for Web Services (DPWS) specification.
Slides: tba
7th of November, 2011
Formal Verification of Ada Programs: An Approach based on Model Checking
João Martins (HASLab)
The rapid growth of the complexity of software systems demands, now more than ever, a rigorous validation of these systems in order to maintain or even increase their reliability. The talk will describe a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automatically extracts from an Ada program a SPIN model, together with a set of desirable properties. ATOS is also capable of extracting properties from a specification annotated by the user in the program, inspired by the Spark Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada programs, based on model checking.
Slides: tba
30th of November, 2011
Dotted Version Vectors: Efficient Causality Tracking for Distributed Key-Value Stores
Carlos Baquero (HASLab)
In cloud computing environments, data storage systems often rely on optimistic replication to provide good performance to geographically disperse users and to allow operation even in the presence of failures or network partitions. In this scenario, it is important to be able to accurately and efficiently identify updates executed concurrently. In this paper, first we review, and expose problems with current approaches to causality tracking in optimistic replication: these either lose information about causality or do not scale, as they require replicas to maintain information that grows linearly with the number of clients or updates. Then, we propose a novel, scalable solution that fully captures causality: it maintains very concise information that grows linearly only with the number of servers that register updates for a given data element, bounded by the degree of replication. Moreover, causality can be checked in $O(1)$ time instead of O(n) time for version vectors. We have integrated our solution in Riak, and results with realistic benchmarks show that it can use as little as 10% of the space consumed by current version vector implementation, which includes an unsafe pruning mechanism.
Slides: tba
23rd of November, 2011
Estimativa de funções de probabilidade cumulativa em redes de larga escala
Miguel Borges (HASLab)
A capacidade de agregar dados é uma característica fundamental na concepção de sistemas de informação escaláveis, que permite a determinação de propriedades globais importantes de forma descentralizada, para a coordenação de aplicações distribuídas, ou para fins de monitorização. No entanto, são ainda relativamente escassos os trabalhos que se focam sobre a agregação de métricas expressivas dessas propriedades. Tomando como ponto de partida o actual estado da arte, será apresentado neste trabalho um algoritmo distribuído para a determinação de funções cumulativas de probabilidade em redes de larga escala. O mecanismo mostra resiliência quando submetido a perda de mensagens, é adaptável a alterações no valor amostrado e resiliente a dinamismo no número de nodos na rede.
Avaliação realista e controlada de aplicações distribuídas é ainda hoje muito difícil de alcançar, especialmente em cenários de grande escala. Modelos de simulação pura podem ser uma solução para este problema, mas criar modelos abstractos a partir de implementações reais nem sempre é possível ou mesmo desejável, sobretudo na fase de desenvolvimento na qual ainda podem não existir todos os componentes ou a sua funcionalidade estar incompleta. Esta falha pode ser colmatada com a plataforma Minha, que permite uma avaliação realista das aplicações através da combinação de modelos abstractos de simulação e implementações reais num ambiente centralizado. O ponto principal desta dissertação consiste na criação de um modelo de rede a ser usado pela plataforma de modo a incluir na avaliação variáveis como os tempos necessários para a troca de mensagens, elevando assim a precisão dos resultados gerados. Para isto é apresentado o método de calibração do modelo através do qual é possível aproximar o modelo do ambiente real. Este sistema permite reproduzir as condições de um sistema em grande escala e através da manipulação de bytecode Java, suporta componentes de middleware inalterados. A utilidade deste sistema é demonstrada aplicando-o ao WS4D, uma pilha que cumpre a especificação Device Profile for Web Services.
Slides: tba
2nd of November, 2011
Designing an Algorithmic Proof of the Two-Squares Theorem
João Ferreira (University of Teesside, UK, and HASLab)
I show a new and constructive proof of the two-squares theorem, based on a somewhat unusual but very effective, way of rewriting the so-called extended Euclid's algorithm. Rather than simply verifying the result---as it is usually done in the mathematical community---I use Euclid's algorithm as an interface to investigate which numbers can be written as sums of two squares. The precise formulation of the problem as an algorithmic problem is the key, since it allows the use of algorithmic techniques. The notion of invariance, in particular, plays a central role in the development: it is used initially to observe that Euclid's algorithm can actually be used to represent a given number as a sum of two squares, and then it is used throughout the argument to prove other relevant properties. I also show how the use of program inversion techniques can make mathematical arguments more precise.
HaExcel: a model-based spreadsheet evolution system
Jácome Cunha/Jorge Mendes (HASLab)
This paper describes the embedding of ClassSheet models in spreadsheet systems. ClassSheet models are well-known and describe the business logic of spreadsheet data. We embed this domain specific model representation on the (general purpose) spreadsheet system. By defining such an embedding, we provide end users a model-driven engineering spreadsheet developing environment. End users can interact with both the model and the spreadsheet data in the same environment. Moreover, we use advanced techniques to evolve spreadsheets and models and to have them synchronized. In this paper we present our work on extending a widely used spreadsheet system with such a model-driven spreadsheet engineering environment.
WHISPER: Middleware for Confidential Communication in Large-Scale Networks
Etienne Riviere (University of Neuchâtel)
A wide range of distributed applications requires some form of confidential communication between groups of users. In particular, the messages exchanged between the users and the identity of group members should not be visible to external observers. Classical approaches to confidential group communication rely upon centralized servers, which limit scalability and represent single points of failure. In this talk, I will introduce our work on WHISPER, a fully decentralized middleware that supports confidential communications within groups of nodes in large-scale systems. It builds upon a peer sampling service that takes into account network limitations such as NAT and firewalls. WHISPER implements confidentiality in two ways: it protects the content of messages exchanged between the members of a group, and it keeps the group memberships secret to external observers. Using multi-hops paths allows these guarantees to hold even if attackers can observe the link between two nodes, or be used as content relays for NAT bypassing. Evaluation in real-world settings indicates that the price of confidentiality remains reasonable in terms of network load and processing costs.
Slides: tba
12th of October, 2011
The Role of Coordination Analysis in Software Integration Projects
Nuno Oliveira (HASLab)
What sort of component coordination strategies emerge in a software integration process? How can such strategies be discovered and further analysed? How close are they to the coordination component of the envisaged architectural model which was supposed to guide the integration process? This talk introduces a framework in which such questions can be discussed and illustrates its use by describing part of a real case-study. The approach is based on a methodology which enables semi-automatic discovery of coordination patterns from source code, combining generalized slicing techniques and graph manipulation.
Slides: tba
28th of September, 2011
Some lightweight approaches to formal HCI
Andy Gimblett (Swansea University)
In this talk I will review some recent work at Swansea University in exploring application of "lightweight" formal methods to questions of HCI, whose common thread is the use of graph-based models of system structure. The approaches encompass specification, reverse engineering of running systems, and analysis of the models for HCI-relevant properties; the intent is to discover techniques which could feasibly be integrated into mainstream software development toolchains without requiring extensive expertise on the part of the tool user - hence "lightweight". The talk will be fairly informal and high level.
Slides: tba
27th of July, 2011
Exploiting shared interests without disclosing them in topic-based publish/subscribe
Miguel Matos (HASLab)
Topic-based publish/subscribe abstracts news dissemination systems typified by RSS feeds. Existing systems either fail to take advantage of shared interests in topic subscriptions, thus incurring high maintenance/traffic costs, or require full disclosure of interests raising privacy concerns and leading to brittle structures due to clustering. We present StaN? a decentralized protocol that leverages shared interests to optimize physical resource usage of topic-based pub/sub without inducing clustering. StaN? does not require interest disclosure thus offering simple but naive privacy. With privacy being a recent concern in p2p networks we seek how to incorporate it in the existing scalable infrastructure.
Slides: tba
Lightning Talk 2 (5 min.): Where do algorithms "come from"? (JNO)
20th of July, 2011
Benchmark-based Software Product Quality
Tiago Alves (HASLab/SIG)
Key to software product quality is the ability to measure, evaluate and rank software systems. In this presentation we will introduce a novel methodology to use source code metrics to evaluate and rank software systems against a benchmark. Thresholds are derived from a benchmark and used in a two-stage process to aggregate metrics, first to risk profiles and afterwards to ratings. A rating summarizes a metric at system-level, allowing it to compare and evaluate a software. Thresholds also allow to drill down from ratings to measurements, enabling root-cause analysis. We explain the methodologies to derive thresholds from benchmark data and their role in the SIG quality model. Finally, using two space-domain software systems, we show how the whole process enables meaningful analysis and evaluation of software systems.
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino) - see the HASLab blog
Lightning Talk 2 (5 min.): Where do algorithms "come from"? (JNO)
6th of July, 2011
(Semi-) Automatic Fault Diagnosis
Rui Maranhão (FEUP/HASLab)
Automatic fault localization techniques aid developers/testers to pinpoint the root cause of software faults, thereby reducing the debugging effort. Depending on the amount of knowledge that is required about the system’s internal component structure and behavior, current, predominant approaches to automatic software fault localization can be classified as (1) statistics-based approaches, and (2) reasoning approaches. Statistics-based fault localization techniques such as SFL use program spectra to find a statistical relationship with observed failures. While modeling costs and computational complexity are minimal, SFL’s diagnostic accuracy is inherently limited as no reasoning is used. In contrast to SFL, model-based reasoning approaches use prior knowledge of the system, such as component interconnection and statement semantics, to build a model of the correct behavior of the system. While delivering higher diagnostic accuracy, they suffer from high computation complexity. In this talk, we present a novel, low-cost, Bayesian reasoning approach to spectrum-based multiple fault localization, coined Barinel. A central feature of our contribution is the use of a generic, intermittent component failure model. Whereas previous approaches have used approximations instead, in Barinel component intermittency rate is computed as part of the posterior candidate probability computation, using a maximum likelihood estimation procedure. This procedure optimally exploits all information contained by the program spectra. Our synthetic and real software experiments (not only including well-known benchmark programs, but also experiments on the Philips TV software) show that Barinel outperforms other state-of-the-art approaches.
Slides: tba
29th of June, 2011
Worldwide Consensus - Best paper award
Francisco Maia (HASLab)
Consensus is an abstraction of a variety of important challenges in dependable distributed systems. Thus a large body of theoretical knowledge is focused on modeling and solving consensus within different system assumptions. However, moving from theory to practice imposes compromises and design decisions that may impact the elegance, trade-offs and correctness of theoretical appealing consensus protocols. In this paper we present the implementation and detailed analysis, in a real environment with a large number of nodes, of mutable consensus, a theoretical appealing protocol able to offer a wide range of trade-offs (called mutations) between decision latency and message complexity. The analysis sheds light on the fundamental behavior of the mutations, and leads to the identification of problems related to the real environment. Such problems are addressed without ever affecting the correctness of the theoretical proposal.
Slides: tba
22nd of June, 2011
Reasoning about Alloy Specifications using Pointfree Relational Calculus
Nuno Macedo (HASLab)
As a lightweight formal modeling language, Alloy focusses on quick and automatic verification of specifications, at the expense of the size of the scope of analysis. However, when modeling safety-critical systems, the need for unbounded proofs arises. Since in Alloy everything is a relation, the calculus of relations is a natural candidate to represent its specifications. As such, we propose a possible translation of Alloy models into a pointfree relational calculus, whose resulting expressions are still simple and easy to manipulate.
Slides: (pdf) ; see also a paper in preparation on this subject
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)
15th of June, 2011
Formalizing and Implementing a Type System for a Cryptographic Language
Paulo Silva (HASLab)
Cryptographic software development is a challenging field not only by the inherent mathematical issues but also by the need of correctness and the lack of supporting tools. CAO is a DSL designed to aid the development of cryptographic software. The language incorporates a series of syntactic and semantic features that facilitate the development of correct and optimised cryptographic software. One of the central key features of CAO is its original type system, introducing native types such as pre-defined sized vectors and matrices as well as integer and polynomial moduli types. This paper presents the formalisation and the implementation of this rich CAO type system. We also show, resorting to practical examples, how this type system enforces strong typing rules and how these rules detect several common run-time errors in cryptographic algorithms.
Slides: tba
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)
8th of June, 2011
Test case generation from mutated task models
José Creissac Campos (HASLab)
This talk describes an approach to the model-based testing of graphical user interfaces from task models. Starting from a task model of the system under test, oracles are generated whose behaviour is compared with the execution of the running system. The use of task models means that the effort of producing the test oracles is reduced. It does also mean, however, that the oracles are confined to the set of expected user behaviours for the system. The talk focuses on solving this problem. It shows how task mutations can be generated automatically, enabling a broader range of user behaviours to be considered. The is the rehearsal of a talk to be given at EICS 2011 the following week.
Slides: tba
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)
1st of June, 2011
Do the middle letters of "OLAP" stand for Linear Algebra (LA)?
H. Macedo and J.N. Oliveira (HASLab)
Inspired by work on pointfree relational data processing, we investigate how the generation of cross tabulations (pivot tables) and data cubes essential to on-line analytical processing (OLAP) and data mining can be expressed in terms of matrix multiplication, transposition and the Khatri-Rao matrix product, a variant of the Kronecker product. This offers much potential for parallel OLAP, as such matrix operations have a well-defined parallelization theory. We propose a simple roadmap for parallel OLAP based on a separation of concerns: rather than depending on SQL-querying and heavy machinery, one encodes the data in matrix format and relies solely on LA operations to perform OLAP operations; then such LA scripts run on a parallel machine, trusting on the efficiency of well-established, parallel LA kernels which have become available in areas such as eg. DSP and computer graphics.
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)
25th of May, 2011
Distributed Systems Cloud Platform
Francisco Maia (HASLab)
Regardless all the theoretical results and research in the field, Distributed Systems remain considered to be a topic somehow difficult and mastered by a small group of people. However, designing and implementing Distributed Systems is essential to achieve highly resilient and robust systems. Moreover, there is still a gap between the design of distributed protocols and their implementation and deployment processes. There are a number of systems aimed at solving these problems. These systems try to provide a programming paradigm that eases the development of Distributed Systems from design to deployment. However, a unifying solution is still lacking. Recently Declarative Networking (Hellerstein et al) appeared solving some of these problems. Namely, focusing on a data-centric approach to application design. However, providing consistency guarantees in such programming model seems to require a posteriori verification of the code and, in some cases, requires the developer to rewrite the code. Building on all these observations it becomes clear that there is room for a new Distributed Systems Cloud Platform.
Time series motif discovery is the task of extracting previously unknown recurrent patterns from time series data. It is an important problem within applications that range from finance to health. Many algorithms have been proposed for the task of efficiently finding motifs. Surprisingly, most of these proposals do not focus on how to evaluate the discovered motifs. They are typically evaluated by human experts. This is unfeasible even for moderately sized datasets, since the number of discovered motifs tends to be prohibitively large. Statistical significance tests are widely used in bioinformatics and association rules mining communities to evaluate the extracted patterns. In this work we present an approach to calculate time series motifs statistical significance. Our proposal leverages work from the bioinformatics community by using a symbolic definition of time series motifs to derive each motif's p-value. We estimate the expected frequency of a motif by using Markov Chain models. The p-value is then assessed by comparing the actual frequency to the estimated one using statistical hypothesis tests. Our contribution gives means to the application of a powerful technique - statistical tests - to a time series setting. This provides researchers and practitioners with an important tool to evaluate automatically the degree of relevance of each extracted motif.
Formal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive low-level optimisations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. We apply state-of-the art deductive verification tools to check security-relevant properties of cryptographic software, including safety, absence of error propagation, and correctness with respect to reference implementations.
Requirements management in the CESAR project: Boilerplates and Ontologies together
J.M. Faria (Critical Software)
Presentation of tools and methodologies for semi-automation of requirement analysis in requirements engineering. Prospect of enriching such methodologies with formal methods support.
Calculating (Haskell) programs from Galois connections
J.N. Oliveira (HASLab); joint work with Shin-Cheng Mu (IIS, Academia Sinica, Taiwan)
Problem statements (and software requirements) resorting to superlatives such as in eg. "... the smallest such number", "... the best approximation", "... the longest such list" lead to specifications made of two parts: one defining a broad class of solutions (the "easy" part) and the other requesting one particular such solution, which is optimal in some sense (the "hard" part). I will talk about a binary relational combinator which mirrors this linguistic structure and exploit (using pointfree relational algebra) its potential for calculating programs by optimization. This applies to handling Galois connections in which one of the adjoints delivers the optimal solution. The framework is also shown to encompass, as special cases, thinning strategies already known for refining non-deterministic, inductive specifications (vulg. "relational (un)folds"). This includes the elegant re-factoring of two results by Bird-de Moor (the two Greedy Theorems and the Dynamic Programming Theorem) dispensing with powersets and the power transpose.
The APEX framework: prototyping of ubiquitous environments based on Petri nets
José Luís Silva (HASLab)
The user experience of ubiquitous environments is a determining factor in their success. The characteristics of such systems must be explored as early as possible to anticipate potential user problems, and to reduce the cost of redesign. However, the development of early prototypes to be evaluated in the target environment can be disruptive to the ongoing system and therefore unacceptable. This talk reports on an ongoing effort to explore how model-based rapid prototyping of ubiquitous environments might be used to avoid actual deployment while still enabling users to interact with a representation of the system. The paper describes APEX, a framework that brings together an existing 3D Application Server with CPN Tools. APEX-based prototypes enable users to navigate a virtual world simulation of the envisaged ubiquitous environment. The APEX architecture and the proposed CPN-based modelling approach are described. An example illustrates their use.
Fastest: a Model-Based Testing Tool for the Z Notation
Maximiliano Cristiá (Universidad Nacional de Rosario, Argentina)
Fastest is a model-based testing tool for the Z formal notation providing an almost automatic implementation of the Test Template Framework. Z is one of the first and most studied industrial-strength formal methods to formally specify software systems. In this talk I will show how to use Fastest to automatically derive abstract test cases from a Z specification.
Matrices as Arrows! A Biproduct Approach to Typed Linear Algebra
Hugo Macedo (MAPi PhD student)
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of programming. The derivation of fusion, cancellation and abide laws from the biproduct equations makes it easy to calculate algorithms implementing matrix multiplication, the kernel operation of matrix algebra, ranging from its divide-and-conquer version to the conventional, iterative one. From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.
Lenses are one the most popular approaches to define bidirectional transformations between data models. A bidirectional transformation with "view-update", denoted a "lens", encompasses the definition of a forward transformation projecting "concrete models" into "abstract views", together with a backward transformation instructing how to translate an abstract view to an update over concrete models. In this presentation we show that most of the standard point-free combinators can be lifted to lenses with suitable backward semantics, allowing us to use the point-free style to define powerful bidirectional transformations by composition. We also demonstrate how to define generic lenses over arbitrary inductive data types by lifting standard recursion patterns, like folds or unfolds. To exemplify the power of this approach, we "lensify" some standard functions over naturals and lists, which are tricky to define directly "by-hand" using explicit recursion.
The GUISurfer tool: towards a language independent approach to reverse engineering GUI code
J. Carlos Silva (MAPi PhD student)
Graphical user interfaces (GUIs) are critical components of today's software. Developers are dedicating a larger portion of code to implementing them. Given their increased importance, correctness of GUIs code is becoming essential. This talk describes the latest results in the development of GUISurfer, a tool to reverse engineer the GUI layer of interactive computing systems. The ultimate goal of the tool is to enable analysis of interactive system from source code.
Can we teach computers to generate fast OLAP code?
Hugo Macedo (MAPi PhD student) and J.N. Oliveira
Inspired by previous pointfree relational approaches to data processing, we investigate how the generation of pivot tables in data mining (such as those produced by Microsoft Excel) can be expressed using matrix multiplication and transposition. This generalizes relational projections and provides a linear algebra approach to FD detection and the drill-down/roll-up operations typical of OLAP. In this context, the prospect of using SPIRAL to generate fast code for OLAP is envisaged.
Slides: there is a technical note (version of July-10th) about this talk
Formal analysis of user interfaces: state of the art and future prospects
Michael Harrison (Newcastle University)
This talk will give a (biased) survey of the use of mathematically based tools in the analysis of aspects of the user interface. It will discuss the role that these tools can play in improving interface design, how they complement more conventional HCI techniques and why their integration with existing techniques remains a future prospect. The talk will discuss future challenges and opportunities. Amongst these, scale and genericity, the prospects for tools that are accessible to HCI experts and the need for a common language will be a particular focus.
Free theorems establish interesting properties of parametrically polymorphic functions, solely from their types, and serve as a nice proof tool. For pure and lazy functional programming languages, they can be used with very few preconditions. Unfortunately, in the presence of selective strictness, as provided in languages like Haskell, their original strength is reduced. In this paper we present an approach for restrengthening them. By a refined type system which tracks the use of strict evaluation, we rule out unnecessary restrictions that otherwise emerge from the general suspicion that strict evaluation may be used at any point. Additionally, we provide an implemented algorithm determining all refined types for a given term.
Alberto Pardo, InCo, Universidad de La República, Uruguai
We show the main aspects of a compiler, written in Haskell, which preserves the property of noninterference between a simple imperative language and structured machine code with loop and branch primitives. The compiler is based on the use of typed abstract syntax (represented in terms of GADTs and type families) both for the source and target language. In this case typed abstract syntax is used to model the type system for noninterference of each language where types correspond to security types. That way it is possible, on the one hand, to use Haskell's type checker to verify that programs enforce security restrictions, and on the other hand, verify that the compiler is correct (in the sense that preserves security restrictions) by construction. Joint work with Cecilia Manzino.
Program Repair as Sound Optimization of Broken Programs
Tarmo Uustalu, Institute of Cybernetics, Tallinn University of Technology
We present a new, semantics-based approach to mechanical program repair where the intended meaning of broken programs (i.e., programs that may abort under a given, error-admitting language semantics) can be defined by a special, error-compensating semantics. Program repair can then become a compile-time, mechanical program transformation based on a program analysis. It turns a given program into one whose evaluations under the error-admitting semantics agree with those of the given program under the error-compensating semantics. We present the analysis and transformation as a type system with a transformation component, following the type-systematic approach to program optimization from our earlier work. The type-systematic method allows for simple soundness proofs of the repairs, based on a relational interpretation of the type system, as well as mechanical transformability of program correctness proofs between the Hoare logics for the error-compensating and error-admitting semantics. We first demonstrate our approach on the repair of file-handling programs with missing or superfluous open and close statements. Our framework shows that this repair is strikingly similar to partial redundancy elimination optimization commonly used by compilers. In a second example, we demonstrate the repair of programs operating a queue that can over- and underflow, including mechanical transformation of program correctness proofs. (Joint work with Bernd Fischer, Ando Saabas.)
TR-HASLab:01:2014 - Jácome Cunha, João Paulo Fernandes, Jorge Mendes, João Saraiva. Embedding, Evolution, and Validation of Model-Driven Spreadsheets. April. 2014.
TR-HASLab:02:2014 - João Saraiva et al., !SSaaPP: SpreadSheets as a Programming Paradigm. August. 2014.
TR-HASLab:03:2014 - Victor Miraldo, Object Oriented Programming with Monadic Mealy Machines (PDF). QAIS Project, October 2014.
TR-HASLab:04:2014 - Jorge Mendes, Model-driven Spreadsheets on Google Drive. December, 2014.
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).
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).
Technical Reports LaTeX style file: haslab report.sty 2011 TR HASLab:01:2011 L. S. Barbosa and Dimitrios Settas (eds). Pre Proceedings of the Fifth International ...
Languages And Tools for Critical Real time Systems The goal of this project is to contribute to a change to the current paradigm of secure ITC infrastructure, according ...
This page has been moved to the new HASLab web site at http://haslab.uminho.pt/calendar HASLab Seminar Series The HASLab Seminar Series is a scientific colloquium ...
Welcome to HASLab Our Motto "Improving Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting ...
Imprensa Universidade do Minho desenvolve aplicação que evita erros no Excel http://www.tvi.iol.pt/videos/13893309 UMinho recebe polo do INESC TEC http://www.cienciahoje ...
Working at HASLab HASLab is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of ...
Recent Publications Journal Papers J.N. Oliveira, M.A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering ...
Lemma "Improve Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting computers' behaviour. HASLab ...
Ph.D. MAP/I Doctoral Programme in Computer Science. See eg. units such as PSVC. M.Sc. Master courses in Computer science at Minho University are built upon the ...
TWiki.DI/FMHAS Web Preferences The following settings are web preferences of the TWiki.DI/FMHAS web. These preferences overwrite the site level preferences ...
Forthcoming Events GTTSE'11 4th Summer School on Generative and Transformational Techniques in Software Engineering, 2011. Past Events 2010 7th Int ...
GTTSE'11 4th Summer School on Generative and Transformational Techniques in Software Engineering, 2011 2010 7th Int. Conference on Formal Aspects of Component ...
Dependable Distributed Systems The goal is to advance the state of the art in dependable distributed data management and dependable distributed systems, in particular ...
(Under revision) 2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled ...
This is a subscription service to be automatically notified by e mail when topics change in this DI/FMHAS web. This is a convenient service, so you do not have to ...
Software technology is pre-scientific in its lack of an effective basis for predicting computers' behaviour. HASLab research aims at improving scientific standards in software design through rigorous methods and mathematical techniques.
HASLab researchers have a long tradition of linking their research to national and international industry partners, 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 (Ph.D and M.Sc) students.
The HASLab "Tripod"
Formal methods
Dependable Distributed Systems
Cryptography & Information security
Research Topics
High-assurance Model-driven Software Engineering
Foundations for architectural design (service certification, dynamic reconfiguration and self-adaptability)
Formal verification of real-time Systems
Secure embedded systems (static ckecking of embedded systems against safety policies)
Theoretical Cryptography / Provable Security
Implementation, Verification, and Analysis of Cryptographic Software
Dependability of interactive systems (model checking-based analysis of interactive systems)
Languages And Tools for Critical Real time Systems The goal of this project is to contribute to a change to the current paradigm of secure ITC infrastructure, according ...
Ph.D. MAP/I Doctoral Programme in Computer Science. See eg. units such as PSVC. M.Sc. Master courses in Computer science at Minho University are built upon the ...
Forthcoming Events GTTSE'11 4th Summer School on Generative and Transformational Techniques in Software Engineering, 2011. Past Events 2010 7th Int ...
GTTSE'11 4th Summer School on Generative and Transformational Techniques in Software Engineering, 2011 2010 7th Int. Conference on Formal Aspects of Component ...
Imprensa Universidade do Minho desenvolve aplicação que evita erros no Excel http://www.tvi.iol.pt/videos/13893309 UMinho recebe polo do INESC TEC http://www.cienciahoje ...
Working at HASLab HASLab is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of ...
Lemma "Improve Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting computers' behaviour. HASLab ...
Dependable Distributed Systems The goal is to advance the state of the art in dependable distributed data management and dependable distributed systems, in particular ...
Recent Publications Journal Papers J.N. Oliveira, M.A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering ...
This page has been moved to the new HASLab web site at http://haslab.uminho.pt/calendar HASLab Seminar Series The HASLab Seminar Series is a scientific colloquium ...
Technical Reports LaTeX style file: haslab report.sty 2011 TR HASLab:01:2011 L. S. Barbosa and Dimitrios Settas (eds). Pre Proceedings of the Fifth International ...
(Under revision) 2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled ...
Welcome to HASLab Our Motto "Improving Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting ...
This is a subscription service to be automatically notified by e mail when topics change in this DI/FMHAS web. This is a convenient service, so you do not have to ...
TWiki.DI/FMHAS Web Preferences The following settings are web preferences of the TWiki.DI/FMHAS web. These preferences overwrite the site level preferences ...
This is a subscription service to be automatically notified by e-mail when topics change in this DI/FMHAS 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/FMHAS 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 = HASLab
Set NATWEBLOGO = HASLab
Set WEBLOGOALT = High-Assurance Software Laboratory
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/FMHAS.Topic links.
Set SITEMAPLIST = on
Set SITEMAPWHAT = High-Assurance Software Laboratory
Set SITEMAPUSETO = High-Assurance Software Laboratory
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 #D0D0D0 .
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 #D0D0D0
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.
HASLab web
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS
The DI/FMHAS 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/FMHAS
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS
/twiki/pub/Main/LocalLogos/um_eengP.jpgTechnicalReports
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/TechnicalReports
Technical Reports LaTeX style file: haslab report.sty 2011 TR HASLab:01:2011 L. S. Barbosa and Dimitrios Settas (eds). Pre Proceedings of the Fifth International ... (last changed by JoseNunoOliveira)2020-06-19T09:48:28ZJoseNunoOliveiraBestCaseRL8
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/BestCaseRL8
Languages And Tools for Critical Real time Systems The goal of this project is to contribute to a change to the current paradigm of secure ITC infrastructure, according ... (last changed by JoseCampos)2015-11-02T00:12:05ZJoseCamposSeminar
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Seminar
This page has been moved to the new HASLab web site at http://haslab.uminho.pt/calendar HASLab Seminar Series The HASLab Seminar Series is a scientific colloquium ... (last changed by JoseNunoOliveira)2015-04-04T20:32:47ZJoseNunoOliveiraNewsHeadlines
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/NewsHeadlines
New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709 #8211;728, WSP Company. DOI: 10.1142/S0129054113400145 ... (last changed by TWikiGuest)2013-12-30T11:29:41ZguestNews
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/News
News New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709 #8211;728, WSP Company. DOI: 10.1142/S0129054113400145 ... (last changed by JoseNunoOliveira)2013-12-30T11:29:41ZJoseNunoOliveiraPeople
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/People
(All email addresses are AT di.uminho.pt) Staff Maranhão Abreu email: rui computer org http://portal.acm.org/author page.cfm?id 81321488948 ACM repositoriUM ... (last changed by PauloSilva)2013-11-25T20:31:40ZPauloSilvaWebHome
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/WebHome
Welcome to HASLab Our Motto "Improving Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting ... (last changed by JoseNunoOliveira)2013-10-25T12:27:50ZJoseNunoOliveiraPastProjects
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/PastProjects
Past Projects Research Projects (FP7) (FCT) Evolve (ADI) MathIS (FCT) (FCT) (FCT) AudioBrowser (FCT) KARMA (ADI) ... (last changed by JoseNunoOliveira)2013-10-23T09:33:56ZJoseNunoOliveiraHASLabPress
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/HASLabPress
Imprensa Universidade do Minho desenvolve aplicação que evita erros no Excel http://www.tvi.iol.pt/videos/13893309 UMinho recebe polo do INESC TEC http://www.cienciahoje ... (last changed by JacomeCunha)2013-06-14T13:26:39ZJacomeCunhaProjects
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Projects
#ResearchProjects Research Projects SmartGrids (ON.2, 2013 2015) Network Sensing for Critical Systems Monitoring (ON.2, 2013 2015) Cooperation and ... (last changed by JoseCampos)2013-06-07T23:01:04ZJoseCamposOpportunities
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Opportunities
Working at HASLab HASLab is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of ... (last changed by AlcinoCunha)2013-05-31T13:31:23ZAlcinoCunhaWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/WebSideBar
Overview Home People Selected Publications Technical Reports BookShelf Projects Seminar Blog Press ... (last changed by JoseNunoOliveira)2013-05-06T16:29:07ZJoseNunoOliveiraSelectedPublications
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/SelectedPublications
Recent Publications Journal Papers J.N. Oliveira, M.A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering ... (last changed by JoseNunoOliveira)2013-04-10T14:13:28ZJoseNunoOliveiraPastPeople
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/PastPeople
#FormerStudents Former Researchers and Ph.D Students Post Doc Visser (2003 2007) Uustalu (2000 2002) Pons (2000 2001) Barthe (1998 1999) Ph ... (last changed by JoseNunoOliveira)2013-04-10T14:09:10ZJoseNunoOliveiraLinks
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Links
#OldWebPages Sites: File System GC (VFS @ Minho) Old webpages: FAST (CCTC) and Formal Methods (DIUM) and Formal Methods Group 2361 (INESC ... (last changed by JorgeSousaPinto)2012-10-12T10:47:54ZJorgeSousaPintoResearch
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Research
Lemma "Improve Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting computers' behaviour. HASLab ... (last changed by JorgeSousaPinto)2012-10-09T14:27:31ZJorgeSousaPinto
Languages And Tools for Critical Real-time Systems
The goal of this project is to contribute to a change to the current paradigm of secure ITC infrastructure, according to which the deployment and operation of a critical system implies security enforcement as a reactive process. This, not only requires a significant management overhead, but also fails to provide rigorous security guarantees. The project pursues the development of the theoretical and technological tools to support this shift, building on the state-of-the-art of formal methods, information security and dependability that, independently, are more consolidated research areas.
Project NORTE-07-0124-FEDER-000062 is co-financed by the North Portugal Regional Operational Programme (ON.2 – O Novo Norte), under the National Strategic Reference Framework (NSRF), through the European Regional Development Fund (ERDF). (437.5 KEuro)
WP1: Verification for trustworthy critical real-time systems This work package will develop work on the verification of safety critical real-time software, both advancing the state of the art at the theoretical level and on producing tools that can be used by companies developing critical applications with a particular emphasis in robotics. This will build on current link with non-academic partners in Portugal (e.g. Critical Software), as well as abroad (e.g. aerospace partners in Brazil).
WP Team: J.C. Campos; J. C. Alves; G. Silva; P. Rodrigues
WP2: Programming Languages, Compilers and Virtual Machines The goal of this work-package is to develop advanced programming languages, compilers and runtime systems for embedded systems. The emphasis is on producing applications that are: (a) correct by construction, statically excluding the occurrence of a large class of runtime errors; (b) adaptable, allowing the applications to detect and react to runtime errors, and; (c) efficient, optimizing speed and hardware resource usage.
WP Leader: L. Lopes (FCUP)
WP Team: R. M. Abreu; J. M. P. Cardoso; R. Mendes; J. C. Alves; I. Costa
Publications
João Bispo, Pedro Pinto, Ricardo Nobre, Tiago Carvalho, João M. P. Cardoso, Pedro C. Diniz, “The MATISSE MATLAB Compiler - A MATrix(MATLAB)-aware compiler InfraStructure? for embedded computing SystEms? ,” in IEEE International Conference on Industrial Informatics (INDIN’2013), Bochum, Germany, 29-31 July 2013, IEEE Xplorer, pp. 602-608.
S. Gupta, R. Abreu, J. de Kleer, and A.J.C. van Gemund, "Automatic Systems Diagnosis Without Behavioral Models”. In Proceedings of the IEEE Aerospace Conference 2014, Yellowstone Conference Center in Big Sky, Montana, March 1–8, 2014. IEEE, pp. 1-8.
Ricardo Nobre, João M.P. Cardoso and José Alves, “A DSE Example of Using LARA for Identifying Compiler Optimization Sequences,” in X Jornadas sobre Sistemas Reconfiguráveis (REC'2014), 13 de Abril, 2014, Vilamoura, Algarve, Portugal.
M. Sousa, J.C. Campos, M. Alves and M.D. Harrison. Formal Verification of Safety-Critical User Interfaces: a space system case study. In Formal Verification and Modeling in Human Machine Systems: Papers from the AAAI Spring Symposium, pages 62-67. AAAI Press. 2014. [PDF]
R. Couto, A.N. Ribeiro and J.C. Campos. Application of Ontologies in Identifying Requirements Patterns in Use Cases. In 11th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2014), volume 147 of Electronic Proceedings in Theoretical Computer Science, pages 62-76. 2014. [PDF]
J.C. Campos. High assurance interactive computing systems. In J. Ziegler, J. C. Campos and L. Nigay, editors, HCI Engineering: Charting the Way towards Methods and Tools for Advanced Interactive Systems, pages 39-42. 2014.
R. Couto, A.N. Ribeiro, and J.C. Campos. The Modelery: A Collaborative Web Based Repository. In Computational Science and Its Applications - ICCSA 2014, volume 8584 of Lecture Notes in Computer Science, pages 1-16. Springer. 2014.
C.E. Silva and J.C. Campos. Characterizing the Control Logic of Web Applications' User Interfaces. In Computational Science and Its Applications - ICCSA 2014, volume 8584 of Lecture Notes in Computer Science, pages 263-276. Springer. 2014.
R. Abreu, J. Cunha, J.P. Fernandes, P. Martins, A. Perez, and J. Saraiva. Smelling Faults in Spreadsheets. In IEEE International Conference on Software Maintenance and Evolution (ICSME 2014), pages 111-120. IEEE. 2014.
E. Neto, R. Mendes, and L. Lopes. An architecture for seamless configuration, deployment, and management of wireless sensor-actuator networks. In 3rd International Conference on Sensor Networks (SENSORNETS 2014), pages 73–81, Lisbon, 2013. SCITEPRESS.
L.G.A. Martins, R. Nobre, A.C.B. Delbem, E. Marques, J.M.P. Cardoso, A clustering-based approach for exploring sequences of compiler optimizations. In IEEE Congress on Evolutionary Computation (CEC’14), Beijing, China, July 6-11, 2014, pp. 2436-2443.
L. Martins, R. Nobre, A. Delbem, E. Marques, and J.M.P. Cardoso, Exploration of Compiler Optimization Sequences using Clustering-Based Selection. In ACM SIGPLAN Conference on Languages, Compilers and Tools for Embedded Systems (LCTES’14), Edinburgh, UK, June 12-13, 2014, pp. 63-72.
J. Bispo, L. Reis, and J.M.P. Cardoso, Multi-Target C Code Generation from MATLAB. In ACM/SIGPAN International Workshop on Libraries, Languages and Compilers for Array Programming (ARRAY’2014), Edinburgh, UK, 13 June, 2014.
R. Nobre, P. Pinto, T. Carvalho, J.M.P. Cardoso, and P.C. Diniz, On Expressing Strategies for Directive-Driven Multicore Programing Models. In Proceedings of Workshop on Parallel Programming and Run-Time Management Techniques for Many-core Architectures and Design Tools and Architectures for Multicore Embedded Computing Platforms (PARMA-DITAM '14). ACM, New York, NY, USA, 6 pages.
R. Couto, A.N. Ribeiro and J.C. Campos. A Study on the Viability of Formalizing Use Cases. In 9th International Conference on the Quality of Information and Communications Technology, QUATIC 2014, pages 130-133. IEEE. 2014. [PDF]
J.C. Campos, P. Masci, P. Curzon and M.D. Harrison. Layers, resources and property templates in the specification and analysis of two interactive systems. In Proceedings of the Workshop on Formal Methods in Human Computer Interaction (FoMHCI? ) 2015, pages 38-43. Universitätsbibliothek, RWTH Aachen University. 2015. [PDF]
J.C. Campos, M. Sousa, M. Alves and M.D. Harrison (2015) Formal Verification of a Space System's User Interface with the IVY workbench. IEEE Transactions on Human-Machine Systems. (early access)
R. Couto, A.N. Ribeiro and J.C. Campos (2015) The Modelery: A Model-Based Software Development Repository. International Journal of Web Information Systems, 11(2):205-225.
N. Macedo, A. Cunha, T. Guimarães. Exploring Scenario Exploration. In Fundamental Approaches to Software Engineering, Volume 9033 of Lecture Notes in Computer Science, pp 301-315. Springer, 2015.
M.D. Harrison, P. Masci, J.C. Campos and P. Curzon. Demonstrating that medical devices satisfy user related safety requirements. In Foundations of Health Information Engineering and Systems, Lecture Notes in Computer Science. Springer. (in press)
G. Ferro, R. Silva, and L. Lopes. “Towards Out-of-the-Box Programming for Wireless Sensor Networks,” in 18th IEEE International Conference on Computational Science and Engineering (CSE 2015), IEEE Press, Porto, Portugal, 2015.
João Bispo, Luís Reis, and João M. P. Cardoso, “Techniques for efficient MATLAB-to-C compilation,” In Proceedings of the 2nd ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming (ARRAY 2015). ACM, New York, NY, USA, 7-12.
Ricardo Nobre, Luiz Martins and João M.P. Cardoso, “Use of Previously Acquired Positioning of Optimizations for Phase Ordering Exploration,” in 18th International Workshop on Software and Compilers for Embedded Systems (SCOPES’15), June 1-3, 2015, Schloss Rheinfels, St. Goar, Germany. ACM, New York, NY, USA, pp. 58-67.
João Bispo, Luís Reis, João M. P. Cardoso, “C and OpenCL? Generation from MATLAB,” in 30th ACM Symposium on Applied Computing (SAC 2015), Apr. 13-17, 2015, Salamanca, Spain, ACM Press, 2015.
Nuno Paulino, João Canas Ferreira, João Bispo, and João M. P. Cardoso, “Transparent Acceleration of Program Execution using Reconfigurable Hardware,” in Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE '15), Hot Topic - Transparent use of accelerators in heterogeneous computing systems, Grenoble, France, Mar 9-13, 2015.. EDA Consortium, San Jose, CA, USA, pp. 1066-1071.
Master courses in Computer science at Minho University are built upon the concept of a specialisation course.
Each of these corresponds to a half-time academic year (30 ECTS), 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.
HASLab group members are involved in the following courses:
New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709–728, WSP Company. DOI: 10.1142/S0129054113400145New Paper: H.D. Macedo and J.N. Oliveira. Typing Linear Algebra: a Biproduct-oriented Approach. SCP 78:11, pp.2160-2191 (DOI 10.1016/j.scico.2012.07.012)
New Paper: J.C. Campos and J. Machado, A Specification Patterns System for Discrete Event Systems Analysis, Int. J. Adv. Robotic Systems, vol. 10, 2013, doi:110.5772/56412Job Opportunities: We are opening five post-doctoral positions. Details hereNew Paper: José N. Oliveira, Miguel A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15
New Paper: Nuno Macedo and Alcino Cunha: Implementing QVT-R Bidirectional Model Transformations using Alloy. Accepted at FASE'13.
New Paper: Shin-Cheng Mu, J.N. Oliveira. Programming from Galois connections. The Journal of Logic and Algebraic Programming 81 (2012) 680–704 (DOI 10.1016/j.jlap.2012.05.003).
New Position:Hugo Macedo is since this month (Jan. 2013) a post-doct at Deducteam in Paris.
New Paper: J.N. Oliveira. Towards a Linear Algebra of Programming. Formal Aspects of Computing (2012) 24: 433–458 (DOI 10.1007/s00165-012-0240-9)
New Position:Hugo Macedo is since this month (Apr. 2012) an Invited Researcher at LIAFA in Paris.
New Paper:Formal analysis of Ubiquitous Computing environments through the APEX framework, J.L. Silva, J.C. Campos and M.D. Harrison. In the proceedings of EICS'12, Copenhagen, Denmark, June 25-28, 2012 (to appear).
Software: Just released the latest version of the AlloyMDA tools, for bidirectional transformation between Alloy and UML class diagrams annotated with OCL.
New Paper:Towards an Evaluation of Bidirectional Model-driven Spreadsheets, J. Cunha, J.P. Fernandes, J. Mendes and J. Saraiva. In the proc. of USER'12, an ICSE'12 Workshop, Zurich, Switzerland, June 5, 2012 (to appear).
New Poster:A Bidirectional Model-driven Spreadsheet Environment, J. Cunha, J. Paulo Fernandes, J. Mendes and J. Saraiva. In the Posters Session of ICSE'12, Zurich, Switzerland, June 2-9, 2012 (to appear).
New Paper:Program and Aspect Metrics for Matlab, P. Martins, P. Lopes, J. Paulo Fernandes, J. Saraiva and J. Cardoso. In the proceedings of the ICCSA'12, Salvador da Bahia, Brasil, June 18-21, 2012 (to appear).
New Paper:Towards a Catalog of Spreadsheet Smells, J. Cunha, J. Paulo Fernandes, H. Ribeiro, J. Saraiva. In the proceedings of the The 12th International Conference on Computational Science and Its Applications (ICCSA'12), Salvador de Bahia, Brazil, June 18-21, 2012 (to appear).
New Paper:Bidirectional Transformation of Model-Driven Spreadsheets, J. Cunha, J. Paulo Fernandes, J. Mendes, H. Pacheco and J. Saraiva. In the proceedings of the 5th International Conference on Model Transformation (ICMT'12), Prague, Czech Republic, 28–29 May 2012 (to appear).
New Paper:MDSheet, A Framework for Model driven Spreadsheet Engineering, J. Cunha, J. Paulo Fernandes, Jorge Mendes and João Saraiva. In the proceedings of the 34th International Conference on Software Engineering 2012 (ICSE'12, Formal demonstration), Zurich, Switzerland, June 2-9, 2012 (to appear).
New Paper:From Relational ClassSheets to UML+OCL, J. Cunha, J. Paulo Fernandes and J. Saraiva. In the proceedings of the Software Engineering Track at the 27th Annual ACM Symposium On Applied Computing (SAC 2012), Riva del Garda (Trento), Italy, March 2012 (to appear).
New Paper:Alloy Meets the Algebra of Programming: A Case Study. By J.N. Oliveira and M. Ferreira. IEEE Transactions on Software Engineering, 2012.
Visit: The SAB/Scientific Advisory Board of INESC TEC visited HASLab on 30-Jan - see BIP 124.
Award: HASLab post-doc fellow Alexandra Silva was awarded the IBM Scientific Prize 2011 for her work on Kleene Coalgebra. The ceremony took place on 18th October 2011 at Universidade do Minho.
Workshop: A research workshop to celebrate the awarding of the IBM Scientific Prize 2010 to Alexandra Silva and launching the new QAIS project will take place next Monday, 17 October (details).
New project: FATBIT (Foundations, Applications and Tools for Bidirectional Transformation) recommended for funding by FCT (73K).
New project: Qais (Quantitative Analysis of Reactive Systems) recommended for funding by FCT (105K).
New project: APEX (Agile Prototyping for user EXperience) will develop a software framework enabling rapid prototyping of ubiquitous systems. Developers and users will be able to navigate simulations of built environments to develop an impression of what it will be like to use the final system once fielded.
New Paper:Bigraphical Modelling of Architectural Patterns. By A. Sanchez, L. S. Barbosa and D. Riesco, accepted at FACS'11.
New Paper:The role of coordination analysis in software integration projects. By N. Rodrigues, N. Oliveira and L. S. Barbosa, accepted at EI2N'11.
New Paper:Hybrid specification of reactive systems: An institutional approach. By A. Madeira, J. M. Faria, M. A. Martins and L. S. Barbosa, accepted at SEFM'11.
New Paper:Hybridization of Institutions. By M. A. Martins, A. Madeira, R. Diaconescu and L. Barbosa, accepted at CALCO'2011.
Award: HASLab paper Worldwide Consensus wins the Best Paper award at DisCoTec'11.
New Paper:Programming from Galois connections. By Shin-C. Mu and J.N. Oliveira. In LNCS Vol.6663, June 2011. Follow a discussion on this paper visit Shin's research blog.
Award: HASLab/MAPi PhD student Nuno Castro wins the Google sponsored Best Student Paper award at SDM'2011.
New Paper:Safe Controllers Design for Industrial Automation Systems. By Machado et al. Computers & Industrial Engineering, 60(4):635-653, May 2011.
March 12, 2011
New book: Rigorous Software Development - An Introduction to Program Verification, by HASLab members J.B. Almeida, M.J. Frade, J.S. Pinto and S. Melo de Sousa.
'Cum laude' award: HASLab external student Alexandra Silva was awarded the "cum laude" mention for her doctoral thesis on Kleene Coalgebra, on Dec., 21st, 2010, at Radboud Universiteit Nijmegen. more...
This distinction is only given in the NL in very exceptional cases (less then 5% of all possible candidates). It requires the explicit support of the thesis committee as well as of two other experts in the area (in this case Samson Abramsky, Oxford, and Larry Moss, Indiana). During the committee meeting, Dexter Kozen gave the following justification for his own vote (quoted from memory): "in very rare occasions a doctoral thesis and defense changes the way one sees his own main research area: this was such an occasion and that is all I have to say". Congratulations, Alexandra!
December 22, 2010
New project: APEX proposal recommended for funding by FCT. more...
APEX (Agile Prototyping for user EXperience) will develop a software framework enabling rapid prototyping of ubiquitous systems. Developers and users will be able to navigate simulations of built environments to develop an impression of what it will be like to use the final system once fielded.
September 3, 2010
Paper accepted at OPENCERT'10: J.C. Silva, J.C. Campos, J. Saraiva. GUI Inspection from Source Code Analysis
July 28, 2010
Paper accepted at HCSE'10: J.L. Silva, Ó.R. Ribeiro, J.M. Fernandes, J.C. Campos, M.D. Harrison. The APEX framework: prototyping of ubiquitous environments based on Petri nets
July 22, 2010
Paper accepted at ESORICS'10: J. Almeida, E. Bangerter, M. Barbosa, S. Krenn, A. Sadeghi, T. Schneider. A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Σ-Protocols
June 15, 2010
Paper accepted at FLACOS'10: D. da Cruz, P. R. Henriques, and J. S. Pinto. Contract-based slicing
June 1, 2010
Paper accepted at SEFM'10: J. Barros, D. da Cruz, P. R. Henriques, and J. S. Pinto. Assertion-based Slicing and Slice Graphs.
June 1, 2010
Paper accepted at EICS'10: J.C. Silva et al. The GUISurfer tool: towards a language independent approach to reverse engineering GUI code.
Apr 8, 2010
Talk by Daniel Seidel (Univ. Bonn) today: "Strictification of Circular Lazy Programs in a Calculational Form"
Apr 7, 2010
Just published in "Science of Computer Programming": N. F. Rodrigues and L. S. Barbosa. Slicing for Architectural Analysis.
Mar 20, 2010
Paper accepted at MPC'10: H.D. Macedo and J.N. Oliveira. Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra.
Feb 20, 2010
Paper accepted at MPC'10: Hugo Pacheco and Alcino Cunha. Generic Point-Free Lenses.
Feb 20, 2010
New project: GWS - providing consultancy in the development of Cachapuz's next generation software development framework. J.C. Campos (HASLab) and A.N. Ribeiro.
Feb 10, 2010
Paper accepted at Ada-Europe'2010: Program Verification in SPARK and ACSL: A Comparative Case Study by E. Brito and J. Sousa Pinto
Feb 1, 2010
EASST Best Paper Award at FMICS'09 to J. Bacelar Almeida, M. Barbosa, J. Sousa Pinto, and B. Vieira, for their paper Verifying Cryptographic Software Correctness with Respect to Reference Implementations.
New Paper:Bringing Class Diagrams to Life. By Luis Barbosa and Sun Meng.
In Springer Journal in Innovations in Systems and Software Engineering (forthcoming).
Nov 10, 2009 1:40 AM
New Paper:Towards the introduction of Qos information in a Component Model. By Sun Meng, Luis Barbosa.
SAC'2010 Symp, Coordination track. Mar 2010.
Nov 10, 2009 1:40 AM
New Paper: Which Mathematics for the Information Society? by João Ferreira, Alexandra Mendes, Roland Backhouse, Luis Barbosa.
TFM Conference, Springer LNCS 5846. Nov, 2009.
Nov 10, 2009 1:40 AM
Two Papers at Refine'09: FMweek, Eindhoven, Nov. 2009.
César Rodrigues, José Nuno Oliveira, Luis Barbosa. "A single, complete rule for coalgebraic refinement".
Manuel Martins, Alexandre Madeira, Luis Barbosa. "Refinement by interpretation in a general setting"
The Refine Workshop, 2009, ENTCS (to appear).
Nov 10, 2009 1:40 AM
New Paper: Refinement by interpretation
Manuel Martins, Alexandre Madeira, Luis Barbosa. IEEE SEFM'2009. Nov, 2009.
Nov 10, 2009 1:40 AM
New Project: lab members participate in EFACEC's InPACT project.
lab 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 10, 2009 1:40 AM
Best paper at SBMF'09, VFS GC track:
Miguel Ferreira, José Nuno Oliveira. "An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model". In M.V. Oliveira and J. Woodcock, editors, SBMF, volume 5902 of LNCS, pages 153-169. Springer, 2009.
Aug 21, 2009
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
New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709–728, WSP Company. DOI: 10.1142/S0129054113400145
New Paper: H.D. Macedo and J.N. Oliveira. Typing Linear Algebra: a Biproduct-oriented Approach. SCP 78:11, pp.2160-2191 (DOI 10.1016/j.scico.2012.07.012)
New Paper: J.C. Campos and J. Machado, A Specification Patterns System for Discrete Event Systems Analysis, Int. J. Adv. Robotic Systems, vol. 10, 2013, doi:110.5772/56412
Job Opportunities: We are opening five post-doctoral positions. Details here
New Paper: José N. Oliveira, Miguel A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15
HASLab is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of Scimago IBE ranking. We are part of the INESC TEC Associate Laboratory. Braga is very close to the Peneda-Gerês Natural Park, and has good connections to Porto (and its vibrant cultural life) and the International Airport (30 min shuttle bus to Braga). It also has a very competitive cost of living in comparison to other European cities.
Algorithms and tools for mutable data aggregation and monitoring.
BIM-2013_BestCase_RL3.2_UMINHO
Reliable data management of large volumes of data for storage and analytic processing
BIM-2013_BestCase_RL5.1_UMINHO
Secure broadcast and data management protocols for smartgrids
BIM-2013_BestCase_RL8.1_UMINHO
Tools for the formal verification of critical interactive systems through model checking and theorem proving
BIM-2013_BestCase_RL8.2_UMINHO
The role of different verification tools – software model checkers, timed model checkers, theorem provers – in the verification of real time software applied to critical systems
Additionally, the group is currently offering the following opportunities to PhD candidates, in the context of the MAPi doctoral programme. Some of these provide project-supported funding for the first year of the programme as indicated; funding for the remaining years should be obtained by applying to an FCT grant.
Verification and Validation of Software Systems for Space Projects (IAE/AEB, 2010-12) (Verificação e Validação de Sistemas de Software para Projetos Espaciais - a project of the Brazilian Institute of Aeronauitcs and Space where José Campos acts as a Consultant)
Software technology is pre-scientific in its lack of an effective basis for predicting computers' behaviour. HASLab research aims at improving scientific standards in software design through rigorous methods and mathematical techniques.
HASLab researchers have a long tradition of linking their research to national and international industry partners, 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 (Ph.D and M.Sc) students.
In the period 2003-2008, the lab members have published around 80 research papers, and edited 6
volumes as program chairs. 10 doctoral theses were defended. The lab has also coordinated an international
ALFA network and participated in the TYPES and APPSEM II coordination actions, as well as in an FP7 project.
At the national level three FCT-funded projects were coordinated, together with a number of transfer projects.
Concerning the organisation of events, the highlight was the ETAPS conference, held in 2007.
HASLab "Tripod"
Formal methods
Dependable Distributed Systems
Cryptography & Information security
Research Topics
High-assurance Model-driven Software Engineering
Foundations for architectural design (service certification, dynamic reconfiguration and self-adaptability)
Formal verification of real-time Systems
Secure embedded systems (static ckecking of embedded systems against safety policies)
Theoretical Cryptography / Provable Security
Implementation, Verification, and Analysis of Cryptographic Software
Dependability of interactive systems (model checking-based analysis of interactive systems)
The goal is to advance the state of the art in dependable distributed data management and dependable distributed systems, in particular (i) developing replication protocols based on group communication for different circumstances, with performance and availability as main concerns; (ii) supporting optimistic replication with novel logical clock mechanisms; (iii) scaling data management in a cloud computing environment; and (iv) developing agreement protocols and highly scalable information dissemination/aggregation protocols.
Rui Carlos Oliveira
José Orlando Pereira
António Luís Sousa
Paulo Sérgio Almeida
Carlos Baquero
Victor Francisco Fonte
Information Security
HASLab researchers develop techniques for constructing formal arguments of security for cryptographic schemes and protocols, in particular (i) formalizing security models (goals and attack scenarios) suitable for practical applications; (ii) constructing security arguments to support new and existing protocols that are used in the real world without theoretical validation; (iii) developing formal verification tools that can be used to mechanically check theoretical security proofs at the highest levels of assurance. Enabling the use of cryptography in new application scenarios and computing paradigms, both in terms of the necessary functionality and efficient implementation, by pursuing the development of domain-specific software development tools for cryptography.
José Bacelar Almeida
Manuel Bernardo Barbosa
José Esgalhado Valença
Fault Detection
Statistics-based approaches take as their only input dynamic information collected at run-time (such as component involvement in the execution of a test case), using no prior knowledge of the system under analysis. Such approaches have therefore intrinsically no modeling costs attached. Amongst the best statistical approaches in terms of diagnostic cost/performance ratio are those based on the computation of a statistical similarity between component activity and failure behavior using a so-called similarity coefficient s, which we refer to as spectrum-based fault localization (SFL). Component activity is recorded as program spectra (collected in a matrix A), and information on whether each of the program spectra in A corresponds to a passed of failed execution is collected in a vector e. The diagnostic process can be explained as (A, e) ---s---> D, where D is the yielded diagnostic report. SFL is a light-weight approach since for each component only a similarity coefficient (scalar operation) has to be computed, after which the M components in the system are sorted into D in order of likelihood to be at fault. Besides, dynamically collecting (A, e) requires only marginal overhead.
J.N. Oliveira, M.A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15
Shin-Cheng Mu, J.N. Oliveira. Programming from Galois connections. The Journal of Logic and Algebraic Programming 81 (2012): 680–704 (DOI 10.1016/j.jlap.2012.05.003).
Filippo Bonchi, Marcello Bonsangue, Michele Boreale, Jan Rutten and Alexandra Silva. A coalgebraic perspective on linear weighted automata. In Information and Computation, vol. 211, pp. 77-105, 2012.
J.N. Oliveira. Towards a Linear Algebra of Programming. Formal Aspects of Computing (2012) 24: 433–458 (DOI 10.1007/s00165-012-0240-9)
Alípio Mário Jorge, Paulo J. Azevedo: Optimal leverage association rules with numerical interval conditions. Intell. Data Anal. 16(1): 25-47 (2012)
Nuno Castro and Paulo J. Azevedo. Significant Motifs in Time Series. in Statistical Analysis and Data Mining, Volume 5, Issue 1, pages 35–53, February 2012, John Wiley and Sons.
M. A. Martins, A. Madeira, L. S. Barbosa. A coalgebraic perspective on logical interpretation. Studia Logica, Springer (accepted, September 2011)
J. Bacelar Almeida, Manuel Barbosa, Jorge S. Pinto, Bárbara Vieira. Formal Verification of Side Channel Countermeasures Using Self-Composition. Science of Computer Programming (accepted, available on-line, 2011).
Alberto Pardo, João Paulo Fernandes, João Saraiva. Shortcut Fusion Rules for the Derivation of Circular and Higher-order Programs, Accepted for publication at the Journal Higher-Order and Symbolic Computation (HOSC), ISSN 1388-3690, pages 1-35, Springer.
José Bernardo Barros, Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto: Assertion-based slicing and slice graphs. Formal Asp. Comput. 24(2): 217-248 (2012)
Luciana Lopes Freire, Pedro Miguel Arezes and José Creissac Campos. A literature review about usability evaluation methods for e-learning platforms. Work: A Journal of Prevention, Assessment and Rehabilitation, Volume 41, Supplement 1, pp. 1038-1044, 2012.
Carlos Baquero, Paulo Sérgio Almeida, Raquel Menezes. Extrema Propagation: Fast Distributed Estimation of Sums and Network Sizes. IEEE Transactions on Parallel and Distributed Systems, July 2011. IEEE computer Society Digital Library.
Di Jin, Bo Yang, Carlos Baquero, Dayou Liu, Dongxiao He, Jie Liu.Markov random walk under constraint for discovering overlapping communities in complex networks. Journal of Statistical Mechanics: Theory and Experiment (JSTAT). IOP Science, May 2011.
M. J. Frade, J. S. Pinto. Verification Conditions for Source-level Imperative Programs. In Computer Science Review, Volume 5, Issue 3, pp. 252-277, 2011. Elsevier. DOI: 10.1016/j.cosrev.2011.02.002
Alcino Cunha and Joost Visser: Transformation of Structure-Shy Programs with Application to XPath Queries and Strategic Functions, In Science of Computer Programming, 76(6):516-539. Elsevier, 2011.
J. Machado, E. Seabra, J.C. Campos, F. Soares, C. Leão. Safe Controllers Design for Industrial Automation Systems. Computers and Industrial Engineering. 60(4): 635-653 (2010)
Nuno Rodrigues, Luís Soares Barbosa: Slicing for architectural analysis. Sci. Comput. Program. 75 (10): 828-847 (2010)
Sun Meng, Luís Soares Barbosa: Bringing Class Diagrams to Life. ISSE (Jour. Innovations in Systems and Software Engineering, Springer). 6 (1-2): 91-98 (2010)
Paulo J. Azevedo, Alípio Mário Jorge: Ensembles of jittered association rule classifiers. Data Min. Knowl. Discov. 21(1): 91-129 (2010)
Paulo J. Azevedo: Rules for contrast sets. Intell. Data Anal. 14(6): 623-640 (2010)
Selected Conference Papers
F. Maia, M. Matos, J. Pereira, and R. Oliveira. Worldwide consensus. In Distributed Applications and Interoperable Systems (DAIS, with DisCoTec), number 6723 in LNCS, 2011. DisCoTec'2011 Best Paper Award.
Nuno C. Castro and Paulo Azevedo: Time Series Motifs Statistical Significance. Best Student Paper Award, SIAM SDM 2011.
M.A. Ferreira, J.N. Oliveira: An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model. Best paper in the GC track of SBMF 2009.
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira. Verifying Cryptographic Software Correctness with Respect to Reference Implementations. Best paper Award in FMICS 2009.
José Creissac Campos, Michael D. Harrison: Systematic Analysis of Control Panel Interfaces Using Formal Tools. DSV-IS 2008 (BCS HCI International Excellence Award 2009).
A model is (for purposes of this talk) an abstract, usually graphical, representation of some aspect of a software-intensive system. Software engineering has, since its invention, involved the use of models. In recent decades, a perceived need for greater automation of processes in software engineering, the wish to develop software faster and more cheaply, and the drive for higher quality have motivated ever more reliance on models. Languages for modelling and techniques for working with models have struggled to keep pace, hindered in some cases by conflicting requirements arising from the different motivations. We are currently in a dangerous state in which models sometimes endanger rather than support the developers' aims. I will explain some of the problems, and discuss the progress that I think we will/may/should/must/cannot expect to see in the coming years.
Keywords: tba
Slides: tba
Lightning Talk 1 (5 min.): tba
Lightning Talk 2 (5 min.): tba
19th of June, 2013
Towards fully trustworthy and cross domain safety engineering
Safety engineering standards are amongst the best practice examples on how systems engineering should be done. Nevertheless, these standards are very heuristic, complex to apply and different from domain to domain. The top level requirement for safety critical systems is the SIL, or Safety Integrity Level, but the way it is defined and quantified differs also from domain to domain and is hence the reason why cross-domain reuse of safety process artefacts and components is very difficult, often even impossible. We argue that a better criterion is to use QoS (Quality of Service) as this expresses the point of view of the user in terms of trustworthiness, independently of the domain. The cross domain reuse as goal is also hampered by the way the SIL level is obtained with SIL as such is a system specific property. This is in contrast with the engineering practice to reuse components whenever possible. Altreonic defined a new criterion called ARRL (Assured Reliability and Resilience Level) that can be used to guide the architectural design and validation. The ARRL criterion takes into account the functional properties when faults occur. It complements the SIL criterion similarly like a HARA and FMEA complement each other. It also allows to define rules whereby components are assembled in a system to meet a corresponding SIL level, hence allowing composable safety. The ARRL criterion is also the driving criterion behind the R&D roadmap of Altreonic. This will briefly be illustrated by the formal development of the network-centric OpenComRTOS and by the development of the traceability and requirements driven metamodel behind the GoedelWorks project portal. The latter will use a generic process pattern. The combination of OpenComRTOS Designer and GoedelWorks portal provides for cross domain and cost efficient support for safety and systems engineering.
Distributed transaction processing has benefited greatly from optimistic concurrency control protocols thus avoiding costly fine-grained synchronization. However, the performance of these protocols degrades significantly when the workload increases, namely, by leading to a substantial amount of aborted transactions due to concurrency conflicts. Our approach stems from the observation that the abort rate increases with the load as already executed transactions queue for longer periods of time waiting for their turn to be certified and committed. We thus propose an adaptive algorithm for judiciously scheduling transactions to minimize the time during which these are vulnerable to being aborted by concurrent transactions, thereby reducing the overall abort rate. We do so by throttling transaction execution using an adaptive mechanism based on the locally known state of globally executing transactions, that includes out-of-order execution.Our evaluation using traces from the industry standard TPC-E workload shows that the amount of aborted transactions can be kept bounded as system load increases, while at the same time fully utilizing system resources and thus scaling transaction processing throughput.
Interaction constraints are an expressive formalism for describing coordination patterns, such as those underlying the coordination language Reo, that can be efficiently implemented using constraint satisfaction technologies such as SAT and SMT solvers. Existing implementations of interaction constraints interact with external components only in a very simple way: interaction occurs only between rounds of constraint satisfaction. What is missing is any means for the constraint solver to interact with the external world during constraint satisfaction.This work introduces interactive interaction constraints which enable interaction during constraint satisfaction, and in turn increase the expressiveness of coordination languages based on interaction constraints by allowing a larger class of operations to be considered to occur atomically. We describe how interactive interaction constraints are implemented and detail a number of strategies for guiding constraint solvers. The benefit of interactive interaction constraints is illustrated using small examples. From a general perspective, our work describes how to open up and exploit constraint solvers as the basis of a coordination engine.
Statically enforcing complex invariants in structured documents
Dario Teixeira
Lambdoc is an open-source library offering support for semantically rich structured documents in web applications [1]. It is particularly aimed at web sites that accept user-contributed content and wish to ensure that such content follows strict guidelines regarding soundness and typographic conventions. This talk consists of two parts. The first part provides the context and motivation for the Lambdoc library, together with a brief overview of its features. The second part comprises the bulk of the talk, and discusses the application of the type system of statically typed functional languages such as OCaml and Haskell to enforce complex invariants on document structure. This latter discussion takes the form of a journey, which begins with Phantom Types and ends with Generalized Abstract Data Types (GADTs). Each of these concepts is briefly introduced and its strengths and weaknesses in a practical setting evaluated. Note that the presentation focuses mainly on the OCaml language. However, given the prevalence of Haskell in academia, a brief "OCaml for Haskellers" overview is also provided. Moreover, the OCaml code samples are simple enough to be understandable by anyone with some familiarity with Haskell or any other functional language with parametric polymorphism and algebraic data types.
NoSQL databases manage the bulk of data produced by modern Web applications such as social networks. This stems from their ability to partition and spread data to all available nodes, allowing NoSQL systems to scale. Unfortunately, current solutions’ scale out is oblivious to the underlying data access patterns, resulting in both highly skewed load across nodes and suboptimal node configurations. In this paper, we first show that judicious placement of HBase partitions taking into account data access patterns can improve overall throughput by 35%. Next, we go beyond current state of the art elastic systems limited to uninformed replica addition and removal by: i) reconfiguring existing replicas according to access patterns and ii) adding replicas specifically configured to the expected access pattern. MET is a prototype for a Cloud-enabled framework that can be used alone or in conjunction with OpenStack for the automatic and heterogeneous reconfiguration of a HBase deployment. Our evaluation, conducted using the YCSB workload generator and a TPC-C workload, shows that MET is able to i) autonomously achieve the performance of a manual configured cluster and ii) quickly reconfigure the cluster according to unpredicted workload changes.
Hugo Pacheco (National Institute of Informatics (NII), Tóquio, Japão)
Bidirectional transformations and in particular lenses, programs with a forward get transformation and a backward putback transformation, are routinely written in ways that do not let programmers specify their behavior completely. Several bidirectional programming languages exist to aid programmers in writing a (usually simpler) forward transformation, and deriving a backward transformation for free. However, the maintainability offered by such languages comes at the cost of expressiveness because the ambiguity of synchronization – handled by the putback transformation – is solved by default strategies which are hidden from programmers. In this paper, we argue that such ambiguity is essential for bidirectional transformations and propose a novel putback-based bidirectional language in which programmers write putback synchronization strategies from the start. In sharp contrast with traditional get-based languages, our putback-based language allows programmers to describe the behavior of a bidirectional transformation completely, while retaining the maintainability of writing a single program. We demonstrate that this additional power is manageable in practice through a series of examples, ranging from simple ones that illustrate traditional lenses to complex ones for which our putback-based approach is central to specifying their non-trivial update strategies. Our examples are inspired by existing problems from the functional and database programming fields.
Large-scale distributed systems appear as the major infrastructures for supporting planet-scale services. These systems call for appropriate management mechanisms and protocols. Slicing is an example of an autonomous, fully decentralized protocol suitable for large-scale environments. It aims at organizing the system into groups of nodes, called slices, according to an application-specific criteria where the size of each slice is relative to the size of the full system. This allows assigning a certain fraction of nodes to different task, according to their capabilities. Although useful, current slicing techniques lack some features of considerable practical importance. This paper proposes a slicing protocol, that builds on existing solutions, and addresses some of their frailties. We present novel solutions to deal with non-uniform slices and to perform online and dynamic slices schema reconfiguration. Moreover, we describe how to provision a slice-local Peer Sampling Service for upper protocol layers and how to enhance slicing protocols with the capability of slicing over more than one attribute. Slicing is presented as a complete, dependable and integrated distributed systems primitive for large-scale systems.
Keywords: tba
Slides: tba
20th of March, 2013
On the semantic security of functional encryption schemes
Functional encryption (FE) is a powerful cryptographic primitive that generalizes many asymmetric encryption systems proposed in recent years. Syntax and security definitions for FE were proposed by Boneh, Sahai, and Waters (BSW) (TCC 2011) and independently by O’Neill (ePrint 2010/556). In this paper we revisit these definitions, identify several shortcomings in them, and propose a new definitional approach that overcomes these limitations. Our definitions display good compositionality properties and allow us to obtain new feasibility and impossibility results for adaptive token-extraction attack scenarios that shed further light on the potential reach of general FE for practical applications.
Non-trivial bidirectional transformations (BXs) are inherently ambiguous, as there are in general many different ways to consistently translate an update from one side to the other. Existing BX languages and frameworks typically satisfy only fundamental first principles which ensure acceptable and stable (well-behaved) translation. Unfortunately, these requirements give little insight about how a particular update translation is chosen among the myriad possible. From the user perspective, such unpredictability may hinder the adoption of BX frameworks. This problem can be remedied by imposing a "principle of least change": in a state-based framework this amounts to translating updates so that the result is as close as possible to the original state according to some distance measure. In this paper we start by formalizing such BXs, focusing on the particular framework of lenses. We then discuss whether such least-change lenses can be defined by composition, an essential construct of BX frameworks. For sequential composition, we present two (dual) update translation alternatives: a classical deterministic one and a nondeterministic one where composition may require backtracking. A key ingredient of our paper is the reasoning style which, carried out in relational algebra, achieves elegant formalizations and exposes several similarities and dualities.
Keywords: Bidirectional Transformations, Lenses
Slides: tba
27th of February, 2013
Implementing QVT-R Bidirectional Model Transformations using Alloy
QVT Relations (QVT-R) is the standard language proposed by the OMG to specify bidirectional model transformations. Unfortunately, due to ambiguities in its original semantics, acceptance and development of effective tool support has been slow. Although the bidirectional check semantics have been clarified recently, none of the existing QVT-R tools have been shown to correctly implement it. Even worst, many tools do not even comply to the standard language, none supports OCL constraints over the meta-models (thus being prone to return ill-formed models), and none clearly formalizes how enforce semantics picks a target model from the myriad consistent candidates. In this paper we propose a QVT-R tool that overcomes all these issues: it supports a large subset of QVT-R and UML class diagrams annotated with OCL, complies to the bidirectional check semantics of [1], and enforces update propagation according to the predictable ``principle of least change''. We achieve this by embedding both QVT-R transformations and UML class diagrams (annotated with OCL) in Alloy, a lightweight formal specification language with support for automatic model finding via SAT solving. The proposed tool already proved effective in debugging existing transformations, namely unveiling several errors in the well-known object-relational mapping that illustrates OMG's QVT-R specification.
Just Do It While Compiling! Fast Extensible Records In Haskell
Alberto Pardo (Instituto de Computacion, Universidad de la Republica, Montevideo, Uruguay)
The library for strongly typed heterogeneous collections HList provides an implementation of extensible records in Haskell that needs only a few common extensions of the language. In HList, records are represented as linked lists of label-value pairs with a lookup operation that is linear-time in the number of fields. In this paper, we use type-level programming techniques to develop a more efficient representation of extensible records for HList. We propose two internal encodings for extensible records that improve lookup at runtime without needing a total order on the labels. One of the encodings performs lookup in constant time but at a cost of linear time insertion. The other one performs lookup in logarithmic time while preserving the fast insertion of simple linked lists. Through staged compilation, the required slow search for a field is moved to compile time in both cases. This is a joint work with Bruno Martinez and Marcos Viera recently presented at PEPM 2013.
Slides: tba
6th of March, 2013
Exceptionally, this seminar will take place in the Physics Department at 14:30h.
The logic of non-locality and quantum informatics
Rui Soares Barbosa (Department of Computer Science - University of Oxford)
tba
Keywords: tba
Slides: tba
12th of December, 2012
Clouder: A Flexible Large Scale Decentralized Object Store
Large scale data stores have been initially introduced to support a few concrete extreme scale applications, such as social networks. Their scalability and availability requirements often sacrifice richer data and processing models, and even elementary data consistency. In strong contrast with traditional relational databases (RDBMS), large scale data stores present very simple data models and APIs, lacking most of the established relational data management operations, and presenting relaxed consistency guarantees, providing eventual consistency. This thesis aims at reducing the gap between traditional RDBMS and large scale data stores by seeking mechanisms to provide additional consistency guarantees, and higher-level data processing primitives in large scale data stores. The devised mechanisms should not hinder the scalability and dependability of large scale data stores. Regarding higher-level data processing primitives, this thesis explores two complementary approaches: extending data stores with additional operations such as general multi-item operations; and coupling data stores with other existing processing facilities without hindering scalability. We demonstrate our approaches with running prototypes and extensive experimental evaluation using proper workloads.
Keywords: tba
Slides: tba
Lightning Talk 1 (5 min.): tba
Lightning Talk 2 (5 min.): tba
5th of December, 2012
Calculating Fault Propagation in Functional Programs using the Linear Algebra of Programming (LAoP)
How do software faults propagate in computer programs/systems? Can faulty behavior be predicted in some way, eg. by calculation? Are there versions of the same program / software system which are "better" than others concerning fault propagation? This talk will not provide definite answers to these questions but it will point towards a strategy to handle them. First, faulty behavior can be mimicked probabilistically, and faults can be injected and simulated using monadic programming (see eg. the Probabilistic Functional Programming - PFP library developed in Haskell by M. Erwig). Second, rather than observing propagation patterns by repeated simulation, such programs can be converted into isomorphic matricial versions and reasoned about in the so-called Linear Algebra of Programming (LAoP), an extension of the AoP towards quantitative reasoning. Simple examples (such as those given in eg. DOI: 10.1007/s00165-012-0240-9) show that faulty-program fusion can be calculated and the way faults combine with each other can be expressed using probabilistic (choice) combinators. Future work includes extending the approach to component-oriented software systems modeled as co-algebras of functors involving the distribution monad, thus scaling up from functional programs to software architectures.
HCI for Safety Critical Interactive Applications: Commonalities and Differences between Air Traffic Control, Satelite Ground Segments and Large Civil Aircrafts Cockpits
Philippe Palanque (IRIT, Toulouse)
Recent years have seen an increasing use of sophisticated interaction techniques in the field of command and control systems. The use of such techniques has been required in order to increase the bandwidth between the users and the systems and thus to help them deal efficiently to increasingly complex systems. These techniques come from research and innovation done in the field of HCI but very little has been done to improve their reliability and their tolerance to human error. It can be difficult to know how to assess the risks that such systems can create for the successful operation of safety-critical systems. One consequence of this is that interaction issues are almost entirely missing from international development standards in safety-critical systems, such as IEC615098 or DO 178B. This presentation will present lessons learnt over the last 20 years on developing research in HCI for safety critical interactive systems as well as applying the results in different application domains such as cockpits of large civil aircrafts, air traffic management and satellite ground segments.
Can GUI implementation markup languages be used for modelling?
Carlos E. Silva (HASLab)
The current diversity of available devices and form factors increases the need for model-based techniques to support adapting applications from one device to another. Most work on user interface modelling is built around declarative markup languages. Markup languages play a relevant role, not only in the modelling of user interfaces, but also in their implementation. However, the languages used by each community (modellers/developers) have, to a great extent evolved separately. This means that the step from concrete model to final interface becomes needlessly complicated, requiring either compilers or interpreters to bridge this gap. In this paper we compare a modelling language (UsiXML? ) with several markup implementation languages. We analyse if it is feasible to use the implementation languages as modelling languages.
Keywords: User Interfaces, Modelling, Markup languages
Slides: tba
10th of October, 2012
Dynamic contracts for verification and enforcement of real-time systems properties
André Pedro
Real-time systems are systems where clearly the runtime verification is indispensable, not only due to the high complexity which make static approaches practically unfeasible, but also due to their high dependence of temporal constraints (e.g., model checking -- where models becomes undecidable to check due to the time clock operations: addiction, subtraction by a constant, etc.). The research of techniques for such systems has been growing progressively along the past years due to high need of reliable and safe development complements and alternatives to static approaches. However, the trend towards the research of new dynamic approaches has been higher for soft real-time systems rather than for hard real-time systems (i.e., focusing essentially on the functional aspects). The talk presents briefly the underlying concepts of runtime verification, its motivation, and introduces a specification language prototype proposed by us for monitor generation as well as a practical case study, focusing on hard real-time embedded systems.
Keywords: tba
Slides: tba
26th of September, 2012
Extension and Implementation of ClassSheet Models
Jácome Cunha (HASLab)
In this talk we explore the use of models in the context of spreadsheet engineering. We review a successful spreadsheet modeling language, whose semantics we further extend. With this extension we bring spreadsheet models closer to the business models of spreadsheets themselves. An addon for a widely used spreadsheet system, providing bidirectional model-driven spreadsheet development, was also improved to include the proposed model extension.
Keywords: tba
Slides: tba
A Web Portal for the Certification of Open Source Software
Pedro Martins (HASLab)
In this talk we will present a web portal for the certification of open source software. The portal aims at helping programmers in the internet age, when there are (too) many open source reusable libraries and tools available. Our portal offers programmers a web-based and easy setting to analyze and certify open source software, which is a crucial step to help programmers choosing among many available alternatives, and to get some guarantees before using one piece of software. We will also present our first prototype of such web portal. We will describe in detail a domain specific language that allows programmers to describe with a high degree of abstraction specific open source software certifications. The design and implementation of this language is the core of the web portal.
Keywords: tba
Slides: tba
12th of September, 2012
Bidirectional Data Transformation by Calculation
Hugo Pacheco (HASLab)
The advent of bidirectional programming, in recent years, has led to the development of a vast number of approaches from various computer science disciplines. These are often based on domain-specific languages in which a program can be read both as a forward and a backward transformation that satisfy some desirable consistency properties. Despite the high demand and recognized potential of intrinsically bidirectional languages, they have still not matured to the point of mainstream adoption. This dissertation contemplates some usually disregarded features of bidirectional transformation languages that are vital for deployment at a larger scale. The first concerns efficiency. Most of these languages provide a rich set of primitive combinators that can be composed to build more sophisticated transformations. Although convenient, such compositional languages are plagued by inefficiency and their optimization is mandatory for a serious application. The second relates to configurability. As update translation is inherently ambiguous, users shall be allowed to control the choice of a suitable strategy. The third regards genericity. Writing a bidirectional transformation typically implies describing the concrete steps that convert values in a source schema to values a target schema, making it impractical to express very complex transformations, and practical tools shall support concise and generic coding patterns.
Keywords: Bidirectional Transformations, Data Calculation
Slides: tba
Evolution of Model-Driven Spreadsheets Spreadsheets
Jorge Mendes (HASLab)
Spreadsheets are the most used programming environment, mostly because they are very flexible. This is due to the lack of restrictions imposed on them which can lead to lots of errors. Model-Driven Engineering was already suggested to improve spreadsheets, providing them with specications and checking tools. However, users have to learn to use these tools on top of their existing spreadsheet host system.To remove that difficulty, the work for this thesis describes an embedding of spreadsheet models within spreadsheet themselves. Moreover, a set of operations that can be performed on these models and respective instances is defined. This way, users interact with models and spreadsheets in the same environment with the objective to improve work performance and reduce errors.Resulting from this work, a prototype was created and is also discussed in this dissertation. This prototype can be used to validate the approach taken in this thesis and to provide a base framework for future developments.
Designing interactive software for medical device user interfaces: case studies on drug infusion pumps
Paolo Masci (Queen Mary University of London)
This seminar will be of interest to anybody involved in the design or development of interactive systems. We will discuss some of our recent work carried out within the CHI+MED project (http://www.chi-med.ac.uk), where we integrate empirical approaches with mathematical methods to deliver a richer analysis of safety-critical interactive systems. We will focus on automated analysis of interactive software incorporated in infusion pumps --- interactive medical devices used in healthcare to deliver drugs and nutrients to patients. Case studies based on commercial infusion pumps will be presented. First, we present our recent work [1,2] on the verification of 'predictability', an interaction design principle that concerns the ability of a user to determine the outcome of future interactions. We will illustrate how: (i) precise insights can be gained about situations where interaction design seems awkward and may lead to use errors; (ii) verified solutions can be developed that fix the interaction design; (iii) simple user strategies can be identified that can be safely used to overcome identified issues in devices already on the market. Second, we present our on-going work on the UNI-Pump framework, a formal framework to support a uniform and rigorous approach for specifying and verifying safety requirements for interactive software incorporated in infusion pump user interfaces. This work aims to complement the Generic Infusion Pump (GIP) framework supported by the University of Pennsylvania and the FDA for model-driven development of software incorporated in infusion pumps. The existing GIP is restricted to software for the control logic of infusion pumps. It does not directly tackle interactive software for the user interface, which is also necessary to demonstrate device safety. The UNI-Pump framework addresses this gap. [1] P. Masci, R. Ruksenas, P. Curzon, et.al., "On formalising interactive number entry on infusion pumps.", ECEASST 45 (2011), available at http://www.eecs.qmul.ac.uk/~masci/ [2] P. Masci, R. Ruksenas, P. Curzon, et.al., "The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps.", submitted for publication to Innovations in Systems and Software Engineering (2012). Preprint available at http://tinyurl.com/masci-QMpreprints
Keywords: tba
Slides: tba
20th of June, 2012
Formal Verification of Cryptographic Software Implementations
We explore how formal techniques, namely deductive verification techniques, can be used to increase the guarantees that cryptographic software implementations indeed work as prescribed. First we identify relevant security policies that may be at play in cryptographic systems, as well as the language-based mechanisms that can be used to enforce such policies in those systems. We propose methodologies based on deductive verification to formalise and verify relevant security policies in cryptographic software. We also propose a deductive verification tool for a domain-specific language for cryptographic implementations, that can be used to verify the previously identified security policies. At the very end, we conclude our work by reasoning about the soundness of our verification tool.
Keywords: tba
Slides: tba
6th of June, 2012
Automatic parameter estimation of the iSAX time series representation
The key to scalable mining algorithms is to select a suitable representation of the data. From the existing techniques, the Symbolic Aggregate Approximation (SAX) has been widely used in the time series data mining community. Its popularity arises from the fact that it is symbolic, reduces the dimensionality of the series, allows lower bounding and is space efficient. However, the need to set the symbolic length and alphabet size parameters limits the applicability of the representation since the best parameter setting is highly application dependent. Typically, these are either set to a fixed value (e.g. 8) or experimentally probed for the best configuration. In this work, we aim to tackle this limitation by introducing a novel technique to automatically derive these parameters. The technique, referred as AutoiSAX, not only discovers the best parameter setting for each time series in the database but also finds the alphabet size for each iSAX symbol within the same word. It is based on the simple and intuitive ideas of time series complexity and segment standard deviation. The technique can be smoothly embedded in existing data mining tasks as an efficient sub-routine. We analyse the impact of using AutoiSAX in visualisation interpretability, and motif mining results. Our contribution aims to make iSAX a more general approach as it evolves towards a parameter-free method.
Keywords: tba
Slides: tba
23rd of May, 2012
Modelling and systematic analysis of interactive systems (tentative title)
In this talk I will address some of the more recent work on the modelling and systematic analysis of interactive system being done at HASLab. The main focus will be on ubiquitous computing system. The is the rehearsal of an invited talk to be given at QMUL the following week.
Keywords: tba
Slides: tba
9th of May, 2012
Strong Eventual Consistency for scalable distribution
In this presentation we establish the conditions for strong eventual consistent datatypes (with no rollback allowed) and present two equivalent implementation flavors: State Based, with a defined merge operation and constraints that ensure that mutating operations are compatible with merge; Operation Based, building on top of a causal delivery middleware and ensuring that concurrent operations commute. In particular, we will show Set implementations that match this design.
Slides: tba
28th of March, 2012
Middleware for the NOSQL generation: Challenges and opportunities
José Orlando Pereira (HASLab)
The middleware stack based on a relational database management system (RDBMS) has been the workhorse of the IT industry, incrementally extending the decades old RDBMS with concepts such as object-relational mapping, caching, sharding, and replication. More recently, there has been a growing shift towards the so called NoSQL databases, stemming mostly from the requirements of extremely large applications offered as services (SaaS), but also from novel platforms as a service (PaaS). By departing from the traditional architecture and interfaces of the venerable RDBMS, this movement shatters the foundation of database middleware stack. In this talk we start by examining the assumptions and goals of each layer in the the traditional stack, including the RDBMS. Then we re-evaluate those assumptions and goals in the context of a NoSQL database such as Cassandra or HBase. This leads us to discuss to what extent the role of the database has changed and what should now be expected from middleware. Although there is room for some of the traditional middleware concepts, there are others that have become obsolete, and also some new challenges and opportunities.
Keywords: tba
Slides: tba
21st of March, 2012
From Relational ClassSheets to UML+OCL
Jácome Cunha (HASLab)
Spreadsheets are among the most popular programming languages in the world. Unfortunately, spreadsheet systems were not tailored from scratch with modern programming language features that guarantee, as much as possible, program correctness. As a consequence, spreadsheets are populated with unacceptable amounts of errors. In other programming language settings, model-based approaches have been proposed to increase productivity and program effectiveness. Within spreadsheets, this approach has also been followed, namely by ClassSheets. In this paper, we propose an extension to ClassSheets to allow the specification of spreadsheets that can be viewed as relational databases. Moreover, we present a transformation from ClassSheet models to UML class diagrams enriched with OCL constraints. This brings to the spreadsheet realm the entire paraphernalia of model validation techniques that are available for UML.
Keywords: Spreadsheets, UML, OCL, ClassSheets
Slides: tba
14th of February, 2012
Robust Distributed Data Aggregation
Paulo Jesus (HASLab)
Distributed aggregation algorithms are an important building block of modern large scale systems, as it allows the determination of meaningful system-wide properties (e.g., network size, total storage capacity, average load, or majorities) which are required to direct the execution of distributed applications. In the last decade, several algorithms have been proposed to address the distributed computation of aggregation functions (e.g., COUNT, SUM, AVERAGE, and MAX/MIN), exhibiting different properties in terms of accuracy, speed and communication tradeoffs. However, existing approaches exhibit many issues when challenged in faulty and dynamic environments, lacking in terms of fault-tolerance and support to churn. This study details a novel distributed aggregation approach, named Flow Updating, which is fault-tolerant and able to operate on dynamics networks. The algorithm is based on manipulating flows (inspired by the concept from graph theory), that are updated using idempotent messages, providing it with unique robustness capabilities. Experimental results showed that Flow Updating outperforms previous averaging algorithms in terms of time and message complexity, and unlike them it self-adapts to churn and changes of the initial input values without requiring any periodic restart, supporting node crashes and high levels of message loss.
Keywords: Data aggregation, Distributed algorithms, Dynamic networks, Fault-tolerance
Slides: tba
22th of February, 2012
Subgroup Discovery driven by a user defined property of interest
Paulo Azevedo (HASLab)
In this talk I will describe a framework based on association rules for the discovery of pertinent subgroups of a population according to a defined property of interest. The main idea of subgroup mining is to identify the characteristics of subpopulations that deviate from the global population, according to a user defined property. This property can be represented by categorical values, numerical, a contrast (frequency comparison) or even a distribution. A classical application on census data identifies discrimination on wage for subgroups formed by females with low education when compared to the global population. Other example on medical data identifies characteristics of subgroups with abnormal distribution of the Cholesterol values when compared to the global population. Several instances of this framework will be described, like contrast sets mining, distribution rules and Distribution Learning.
Every transformation is a lens: Taming partiality using invariants and non-determinism
Nuno Macedo (HASLab)
Total well-behaved lenses are restricted to surjective functions. However, many useful transformations are not surjective. To support these, most lens frameworks relax the totality requirement and weaken the round-tripping laws, opening the door to unpredictable synchronization behaviors. We propose a framework where any transformation written in a point-free functional language can be lifted to a total well-behaved lens, by capturing the exact range and domain of the transformation as invariants on the target and source datatypes. To enforce such invariants, the proposed framework relies on non-deterministic execution of backward transformations. Both these and the data invariants are naturally specified using a point-free relational calculus that enables concise and agile algebraic reasoning.
Keywords: Bidirectional transformations, Point-free relational calculus, Data invariants, Non-determinism
Slides: tba
1st of February, 2012
Delegatable Homomorphic Encryption with Applications to Secure Outsourcing of Computation
Manuel Barbosa (HASLab)
In this work we propose a new cryptographic primitive called Delegatable Homomorphic Encryption (DHE). This allows a Trusted Authority to control/delegate the capability to evaluate circuits over encrypted data to untrusted workers/evaluators by issuing tokens. This primitive can be both seen as a public-key counterpart to Verifiable Computation, where input generation and output verification are performed by different entities, or as a generalisation of Fully Homomorphic Encryption enabling control over computations on encrypted data. Our primitive comes with a series of extra features as follows: 1) there is a one-time setup procedure for all circuits; 2) senders do not need to be aware of the functions which will be evaluated on the encrypted data, nor do they need to register keys; 3) tokens are independent of senders and receiver; and 4) receivers are able to verify the correctness of computation given short auxiliary information on the input data and the function, independently of the complexity of the computed circuit. We give a modular construction of such a DHE scheme from three components: Fully Homomorphic Encryption (FHE), Functional Encryption (FE), and a (customised) MAC. As a stepping stone, we first define Verifiable Functional Encryption (VFE), and then show how one can build a secure DHE scheme from a VFE and an FHE scheme. We also show how to build the required VFE from a standard FE together with a MAC scheme. All our results hold in the standard model. Finally, we show how one can build a verifiable computation (VC) scheme generically from a DHE. As a corollary, we get the first VC scheme which remains verifiable even if the attacker can observe verification results.
Implementing sound in a CAVE-like system while ensuring the “synchrony” of the virtual world
Carlos CL Silva (HASLab/LVP)
Although great developments have been made in the generation of ever more visually immersive virtual reality (VR) environments, audiovisual interactive VR environments are still conceived as an enormous challenge, mostly due to ignorance about some audiovisual processes, such as the audiovisual perception of synchrony. Psychophysically, audiovisual perception is still an intriguing phenomenon, especially when we think about time differences – both at the physical and neural level – underlying the perception of sound and light. Thus, in order to develop a truly immersive audiovisual VR environment we need to know how human beings deal with these differences and perceive synchrony between sound and image. This presentation intends to expose these problems and discuss possible solutions for the implementation process of an auditory VR environment in a CAVE-like system at the Laboratory of Visualization and Perception in the University of Minho. Moreover, we will explore this case as an example of the historical contribution of Psychology and Psychophysical research as a start and an ending point in the processes of developing technology for interactive VR environments.
Flow-Updating (FU) is a fault-tolerant technique that has proved to be efficient in practice for the distributed computation of aggregate functions in communication networks where individual processors do not have access to global information. Previous distributed aggregation protocols, based on repeated sharing of input values (or mass) among processors, sometimes called Mass-Distribution (MD) protocols, are not resilient to communication failures (or message loss) because such failures yield a loss of mass. In this paper, we present a protocol which we call Mass-Distribution with Flow-Updating (MDFU). We obtain MDFU by applying FU techniques to classic MD. We analyze the convergence time of MDFU showing that stochastic message loss produces low overhead. This is the first convergence proof of an FU-based algorithm. We evaluate MDFU experimentally, comparing it with previous MD and FU protocols, and verifying the behavior predicted by the analysis. Finally, given that MDFU incurs a fixed deviation proportional to the message-loss rate, we adjust the accuracy of MDFU heuristically in a new protocol called MDFU with Linear Prediction (MDFU-LP). The evaluation shows that both MDFU and MDFU-LP behave very well in practice, even under high rates of message loss and even changing the input values dynamically.
Slides: tba
21st of December, 2011
Translating Alloy Specifications to UML Class Diagrams Annotated with OCL
Ana Garis (HASLab/Universidad Nacional de San Luis, Argentina)
Model-Driven Engineering (MDE) is a Software Engineering approach based on model transformations at different abstraction levels. It prescribes the development of software by successively transforming models from abstract (specifications) to more concrete ones (code). Alloy is an increasingly popular lightweight formal specification language that supports automatic verification. Unfortunately, its widespread industrial adoption is hampered by the lack of an ecosystem of MDE tools. We present a model transformation between Alloy and UML Class Diagrams annotated with OCL. The proposed transformation enables current UML-based tools to also be applied to Alloy specifications, thus unleashing its potential for MDE.
Slides: tba
21st of December, 2011
Archery - Modelling of Architectural Patterns
Alejandro Sanchez (HASLab/Universidad Nacional de San Luis, Argentina)
In a number of contexts the term “architectural pattern” is used as an architectural abstraction. The expression is taken in the usual sense of pattern in object oriented programming - a known design solution to recurring problems. Available pattern catalogs allow to design and evolve architectures by applying them. However, its characterizations remain largely informal, enough to generate a vocabulary for design discussions at a high abstraction level, but insufficient to underpin, for instance, executable models. We describe Archery, a language for modelling of architectural patterns, supporting hierarchical composition and a type discipline. We provide formal semantics for the behavioural and structural dimensions by respective translations to mCRL2 and to bigraphical reactive systems.
Slides: tba
14th of December, 2011
Systems Biology, a holistic approach to the "algebra" of Life
Daniel Machado (IBB/CEB - UMinho)
The cell is the fundamental building block of life. From this basic unit, a myriad of life forms have emerged. Systems Biology is a recent field that studies the complex interactions that happen inside a cell. It represents a new holistic paradigm when compared to the traditional reductionist perspective to biology. The multidisciplinary nature of this field requires the integration of several areas such as computer science, mathematics, physics, chemistry, biology and systems engineering. Building a whole-cell model is its ultimate goal, hampered by the difficulty of "reverse engineering" the specification of a system that evolved in nature. Although still far from this goal, several models of different organisms have been built. These provide a platform for performing "in silico" experiments that allow us to understand the cellular behavior and also to predict the optimal manipulations towards a specific objective. Therefore, they have several applications in biomedical research for the study of diseases and novel drug discovery, as well as in industrial biotechnology for the creation of microbial cell factories that produce a wide range of commodity chemicals.
Slides: tba
7th of November, 2011
Experimental Evaluation of Distributed Middleware with a Virtualized Java Environment
The correctness and performance of large scale service oriented systems depend on distributed middleware components performing various communication and coordination functions. It is, however, very difficult to experimentally assess such middleware components, as interesting behavior often arises exclusively in large scale settings, but such deployments are costly and time consuming. We address this challenge with MINHA, a system that virtualizes multiple JVM instances within a single JVM while simulating key environment components, thus reproducing the concurrency, distribution, and performance characteristics of the actual system. The usefulness of MINHA is demonstrated by applying it to the WS4D Java stack, a popular implementation of the Devices Profile for Web Services (DPWS) specification.
Slides: tba
7th of November, 2011
Formal Verification of Ada Programs: An Approach based on Model Checking
João Martins (HASLab)
The rapid growth of the complexity of software systems demands, now more than ever, a rigorous validation of these systems in order to maintain or even increase their reliability. The talk will describe a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automatically extracts from an Ada program a SPIN model, together with a set of desirable properties. ATOS is also capable of extracting properties from a specification annotated by the user in the program, inspired by the Spark Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada programs, based on model checking.
Slides: tba
30th of November, 2011
Dotted Version Vectors: Efficient Causality Tracking for Distributed Key-Value Stores
Carlos Baquero (HASLab)
In cloud computing environments, data storage systems often rely on optimistic replication to provide good performance to geographically disperse users and to allow operation even in the presence of failures or network partitions. In this scenario, it is important to be able to accurately and efficiently identify updates executed concurrently. In this paper, first we review, and expose problems with current approaches to causality tracking in optimistic replication: these either lose information about causality or do not scale, as they require replicas to maintain information that grows linearly with the number of clients or updates. Then, we propose a novel, scalable solution that fully captures causality: it maintains very concise information that grows linearly only with the number of servers that register updates for a given data element, bounded by the degree of replication. Moreover, causality can be checked in $O(1)$ time instead of O(n) time for version vectors. We have integrated our solution in Riak, and results with realistic benchmarks show that it can use as little as 10% of the space consumed by current version vector implementation, which includes an unsafe pruning mechanism.
Slides: tba
23rd of November, 2011
Estimativa de funções de probabilidade cumulativa em redes de larga escala
Miguel Borges (HASLab)
A capacidade de agregar dados é uma característica fundamental na concepção de sistemas de informação escaláveis, que permite a determinação de propriedades globais importantes de forma descentralizada, para a coordenação de aplicações distribuídas, ou para fins de monitorização. No entanto, são ainda relativamente escassos os trabalhos que se focam sobre a agregação de métricas expressivas dessas propriedades. Tomando como ponto de partida o actual estado da arte, será apresentado neste trabalho um algoritmo distribuído para a determinação de funções cumulativas de probabilidade em redes de larga escala. O mecanismo mostra resiliência quando submetido a perda de mensagens, é adaptável a alterações no valor amostrado e resiliente a dinamismo no número de nodos na rede.
Avaliação realista e controlada de aplicações distribuídas é ainda hoje muito difícil de alcançar, especialmente em cenários de grande escala. Modelos de simulação pura podem ser uma solução para este problema, mas criar modelos abstractos a partir de implementações reais nem sempre é possível ou mesmo desejável, sobretudo na fase de desenvolvimento na qual ainda podem não existir todos os componentes ou a sua funcionalidade estar incompleta. Esta falha pode ser colmatada com a plataforma Minha, que permite uma avaliação realista das aplicações através da combinação de modelos abstractos de simulação e implementações reais num ambiente centralizado. O ponto principal desta dissertação consiste na criação de um modelo de rede a ser usado pela plataforma de modo a incluir na avaliação variáveis como os tempos necessários para a troca de mensagens, elevando assim a precisão dos resultados gerados. Para isto é apresentado o método de calibração do modelo através do qual é possível aproximar o modelo do ambiente real. Este sistema permite reproduzir as condições de um sistema em grande escala e através da manipulação de bytecode Java, suporta componentes de middleware inalterados. A utilidade deste sistema é demonstrada aplicando-o ao WS4D, uma pilha que cumpre a especificação Device Profile for Web Services.
Slides: tba
2nd of November, 2011
Designing an Algorithmic Proof of the Two-Squares Theorem
João Ferreira (University of Teesside, UK, and HASLab)
I show a new and constructive proof of the two-squares theorem, based on a somewhat unusual but very effective, way of rewriting the so-called extended Euclid's algorithm. Rather than simply verifying the result---as it is usually done in the mathematical community---I use Euclid's algorithm as an interface to investigate which numbers can be written as sums of two squares. The precise formulation of the problem as an algorithmic problem is the key, since it allows the use of algorithmic techniques. The notion of invariance, in particular, plays a central role in the development: it is used initially to observe that Euclid's algorithm can actually be used to represent a given number as a sum of two squares, and then it is used throughout the argument to prove other relevant properties. I also show how the use of program inversion techniques can make mathematical arguments more precise.
HaExcel: a model-based spreadsheet evolution system
Jácome Cunha/Jorge Mendes (HASLab)
This paper describes the embedding of ClassSheet models in spreadsheet systems. ClassSheet models are well-known and describe the business logic of spreadsheet data. We embed this domain specific model representation on the (general purpose) spreadsheet system. By defining such an embedding, we provide end users a model-driven engineering spreadsheet developing environment. End users can interact with both the model and the spreadsheet data in the same environment. Moreover, we use advanced techniques to evolve spreadsheets and models and to have them synchronized. In this paper we present our work on extending a widely used spreadsheet system with such a model-driven spreadsheet engineering environment.
WHISPER: Middleware for Confidential Communication in Large-Scale Networks
Etienne Riviere (University of Neuchâtel)
A wide range of distributed applications requires some form of confidential communication between groups of users. In particular, the messages exchanged between the users and the identity of group members should not be visible to external observers. Classical approaches to confidential group communication rely upon centralized servers, which limit scalability and represent single points of failure. In this talk, I will introduce our work on WHISPER, a fully decentralized middleware that supports confidential communications within groups of nodes in large-scale systems. It builds upon a peer sampling service that takes into account network limitations such as NAT and firewalls. WHISPER implements confidentiality in two ways: it protects the content of messages exchanged between the members of a group, and it keeps the group memberships secret to external observers. Using multi-hops paths allows these guarantees to hold even if attackers can observe the link between two nodes, or be used as content relays for NAT bypassing. Evaluation in real-world settings indicates that the price of confidentiality remains reasonable in terms of network load and processing costs.
Slides: tba
12th of October, 2011
The Role of Coordination Analysis in Software Integration Projects
Nuno Oliveira (HASLab)
What sort of component coordination strategies emerge in a software integration process? How can such strategies be discovered and further analysed? How close are they to the coordination component of the envisaged architectural model which was supposed to guide the integration process? This talk introduces a framework in which such questions can be discussed and illustrates its use by describing part of a real case-study. The approach is based on a methodology which enables semi-automatic discovery of coordination patterns from source code, combining generalized slicing techniques and graph manipulation.
Slides: tba
28th of September, 2011
Some lightweight approaches to formal HCI
Andy Gimblett (Swansea University)
In this talk I will review some recent work at Swansea University in exploring application of "lightweight" formal methods to questions of HCI, whose common thread is the use of graph-based models of system structure. The approaches encompass specification, reverse engineering of running systems, and analysis of the models for HCI-relevant properties; the intent is to discover techniques which could feasibly be integrated into mainstream software development toolchains without requiring extensive expertise on the part of the tool user - hence "lightweight". The talk will be fairly informal and high level.
Slides: tba
27th of July, 2011
Exploiting shared interests without disclosing them in topic-based publish/subscribe
Miguel Matos (HASLab)
Topic-based publish/subscribe abstracts news dissemination systems typified by RSS feeds. Existing systems either fail to take advantage of shared interests in topic subscriptions, thus incurring high maintenance/traffic costs, or require full disclosure of interests raising privacy concerns and leading to brittle structures due to clustering. We present StaN? a decentralized protocol that leverages shared interests to optimize physical resource usage of topic-based pub/sub without inducing clustering. StaN? does not require interest disclosure thus offering simple but naive privacy. With privacy being a recent concern in p2p networks we seek how to incorporate it in the existing scalable infrastructure.
Slides: tba
Lightning Talk 2 (5 min.): Where do algorithms "come from"? (JNO)
20th of July, 2011
Benchmark-based Software Product Quality
Tiago Alves (HASLab/SIG)
Key to software product quality is the ability to measure, evaluate and rank software systems. In this presentation we will introduce a novel methodology to use source code metrics to evaluate and rank software systems against a benchmark. Thresholds are derived from a benchmark and used in a two-stage process to aggregate metrics, first to risk profiles and afterwards to ratings. A rating summarizes a metric at system-level, allowing it to compare and evaluate a software. Thresholds also allow to drill down from ratings to measurements, enabling root-cause analysis. We explain the methodologies to derive thresholds from benchmark data and their role in the SIG quality model. Finally, using two space-domain software systems, we show how the whole process enables meaningful analysis and evaluation of software systems.
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino) - see the HASLab blog
Lightning Talk 2 (5 min.): Where do algorithms "come from"? (JNO)
6th of July, 2011
(Semi-) Automatic Fault Diagnosis
Rui Maranhão (FEUP/HASLab)
Automatic fault localization techniques aid developers/testers to pinpoint the root cause of software faults, thereby reducing the debugging effort. Depending on the amount of knowledge that is required about the system’s internal component structure and behavior, current, predominant approaches to automatic software fault localization can be classified as (1) statistics-based approaches, and (2) reasoning approaches. Statistics-based fault localization techniques such as SFL use program spectra to find a statistical relationship with observed failures. While modeling costs and computational complexity are minimal, SFL’s diagnostic accuracy is inherently limited as no reasoning is used. In contrast to SFL, model-based reasoning approaches use prior knowledge of the system, such as component interconnection and statement semantics, to build a model of the correct behavior of the system. While delivering higher diagnostic accuracy, they suffer from high computation complexity. In this talk, we present a novel, low-cost, Bayesian reasoning approach to spectrum-based multiple fault localization, coined Barinel. A central feature of our contribution is the use of a generic, intermittent component failure model. Whereas previous approaches have used approximations instead, in Barinel component intermittency rate is computed as part of the posterior candidate probability computation, using a maximum likelihood estimation procedure. This procedure optimally exploits all information contained by the program spectra. Our synthetic and real software experiments (not only including well-known benchmark programs, but also experiments on the Philips TV software) show that Barinel outperforms other state-of-the-art approaches.
Slides: tba
29th of June, 2011
Worldwide Consensus - Best paper award
Francisco Maia (HASLab)
Consensus is an abstraction of a variety of important challenges in dependable distributed systems. Thus a large body of theoretical knowledge is focused on modeling and solving consensus within different system assumptions. However, moving from theory to practice imposes compromises and design decisions that may impact the elegance, trade-offs and correctness of theoretical appealing consensus protocols. In this paper we present the implementation and detailed analysis, in a real environment with a large number of nodes, of mutable consensus, a theoretical appealing protocol able to offer a wide range of trade-offs (called mutations) between decision latency and message complexity. The analysis sheds light on the fundamental behavior of the mutations, and leads to the identification of problems related to the real environment. Such problems are addressed without ever affecting the correctness of the theoretical proposal.
Slides: tba
22nd of June, 2011
Reasoning about Alloy Specifications using Pointfree Relational Calculus
Nuno Macedo (HASLab)
As a lightweight formal modeling language, Alloy focusses on quick and automatic verification of specifications, at the expense of the size of the scope of analysis. However, when modeling safety-critical systems, the need for unbounded proofs arises. Since in Alloy everything is a relation, the calculus of relations is a natural candidate to represent its specifications. As such, we propose a possible translation of Alloy models into a pointfree relational calculus, whose resulting expressions are still simple and easy to manipulate.
Slides: (pdf) ; see also a paper in preparation on this subject
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)
15th of June, 2011
Formalizing and Implementing a Type System for a Cryptographic Language
Paulo Silva (HASLab)
Cryptographic software development is a challenging field not only by the inherent mathematical issues but also by the need of correctness and the lack of supporting tools. CAO is a DSL designed to aid the development of cryptographic software. The language incorporates a series of syntactic and semantic features that facilitate the development of correct and optimised cryptographic software. One of the central key features of CAO is its original type system, introducing native types such as pre-defined sized vectors and matrices as well as integer and polynomial moduli types. This paper presents the formalisation and the implementation of this rich CAO type system. We also show, resorting to practical examples, how this type system enforces strong typing rules and how these rules detect several common run-time errors in cryptographic algorithms.
Slides: tba
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)
8th of June, 2011
Test case generation from mutated task models
José Creissac Campos (HASLab)
This talk describes an approach to the model-based testing of graphical user interfaces from task models. Starting from a task model of the system under test, oracles are generated whose behaviour is compared with the execution of the running system. The use of task models means that the effort of producing the test oracles is reduced. It does also mean, however, that the oracles are confined to the set of expected user behaviours for the system. The talk focuses on solving this problem. It shows how task mutations can be generated automatically, enabling a broader range of user behaviours to be considered. The is the rehearsal of a talk to be given at EICS 2011 the following week.
Slides: tba
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)
1st of June, 2011
Do the middle letters of "OLAP" stand for Linear Algebra (LA)?
H. Macedo and J.N. Oliveira (HASLab)
Inspired by work on pointfree relational data processing, we investigate how the generation of cross tabulations (pivot tables) and data cubes essential to on-line analytical processing (OLAP) and data mining can be expressed in terms of matrix multiplication, transposition and the Khatri-Rao matrix product, a variant of the Kronecker product. This offers much potential for parallel OLAP, as such matrix operations have a well-defined parallelization theory. We propose a simple roadmap for parallel OLAP based on a separation of concerns: rather than depending on SQL-querying and heavy machinery, one encodes the data in matrix format and relies solely on LA operations to perform OLAP operations; then such LA scripts run on a parallel machine, trusting on the efficiency of well-established, parallel LA kernels which have become available in areas such as eg. DSP and computer graphics.
Lightning Talk 1 (5 min.): 5 min of Alloy (Alcino)
25th of May, 2011
Distributed Systems Cloud Platform
Francisco Maia (HASLab)
Regardless all the theoretical results and research in the field, Distributed Systems remain considered to be a topic somehow difficult and mastered by a small group of people. However, designing and implementing Distributed Systems is essential to achieve highly resilient and robust systems. Moreover, there is still a gap between the design of distributed protocols and their implementation and deployment processes. There are a number of systems aimed at solving these problems. These systems try to provide a programming paradigm that eases the development of Distributed Systems from design to deployment. However, a unifying solution is still lacking. Recently Declarative Networking (Hellerstein et al) appeared solving some of these problems. Namely, focusing on a data-centric approach to application design. However, providing consistency guarantees in such programming model seems to require a posteriori verification of the code and, in some cases, requires the developer to rewrite the code. Building on all these observations it becomes clear that there is room for a new Distributed Systems Cloud Platform.
Time series motif discovery is the task of extracting previously unknown recurrent patterns from time series data. It is an important problem within applications that range from finance to health. Many algorithms have been proposed for the task of efficiently finding motifs. Surprisingly, most of these proposals do not focus on how to evaluate the discovered motifs. They are typically evaluated by human experts. This is unfeasible even for moderately sized datasets, since the number of discovered motifs tends to be prohibitively large. Statistical significance tests are widely used in bioinformatics and association rules mining communities to evaluate the extracted patterns. In this work we present an approach to calculate time series motifs statistical significance. Our proposal leverages work from the bioinformatics community by using a symbolic definition of time series motifs to derive each motif's p-value. We estimate the expected frequency of a motif by using Markov Chain models. The p-value is then assessed by comparing the actual frequency to the estimated one using statistical hypothesis tests. Our contribution gives means to the application of a powerful technique - statistical tests - to a time series setting. This provides researchers and practitioners with an important tool to evaluate automatically the degree of relevance of each extracted motif.
Formal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive low-level optimisations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. We apply state-of-the art deductive verification tools to check security-relevant properties of cryptographic software, including safety, absence of error propagation, and correctness with respect to reference implementations.
Requirements management in the CESAR project: Boilerplates and Ontologies together
J.M. Faria (Critical Software)
Presentation of tools and methodologies for semi-automation of requirement analysis in requirements engineering. Prospect of enriching such methodologies with formal methods support.
Calculating (Haskell) programs from Galois connections
J.N. Oliveira (HASLab); joint work with Shin-Cheng Mu (IIS, Academia Sinica, Taiwan)
Problem statements (and software requirements) resorting to superlatives such as in eg. "... the smallest such number", "... the best approximation", "... the longest such list" lead to specifications made of two parts: one defining a broad class of solutions (the "easy" part) and the other requesting one particular such solution, which is optimal in some sense (the "hard" part). I will talk about a binary relational combinator which mirrors this linguistic structure and exploit (using pointfree relational algebra) its potential for calculating programs by optimization. This applies to handling Galois connections in which one of the adjoints delivers the optimal solution. The framework is also shown to encompass, as special cases, thinning strategies already known for refining non-deterministic, inductive specifications (vulg. "relational (un)folds"). This includes the elegant re-factoring of two results by Bird-de Moor (the two Greedy Theorems and the Dynamic Programming Theorem) dispensing with powersets and the power transpose.
The APEX framework: prototyping of ubiquitous environments based on Petri nets
José Luís Silva (HASLab)
The user experience of ubiquitous environments is a determining factor in their success. The characteristics of such systems must be explored as early as possible to anticipate potential user problems, and to reduce the cost of redesign. However, the development of early prototypes to be evaluated in the target environment can be disruptive to the ongoing system and therefore unacceptable. This talk reports on an ongoing effort to explore how model-based rapid prototyping of ubiquitous environments might be used to avoid actual deployment while still enabling users to interact with a representation of the system. The paper describes APEX, a framework that brings together an existing 3D Application Server with CPN Tools. APEX-based prototypes enable users to navigate a virtual world simulation of the envisaged ubiquitous environment. The APEX architecture and the proposed CPN-based modelling approach are described. An example illustrates their use.
Fastest: a Model-Based Testing Tool for the Z Notation
Maximiliano Cristiá (Universidad Nacional de Rosario, Argentina)
Fastest is a model-based testing tool for the Z formal notation providing an almost automatic implementation of the Test Template Framework. Z is one of the first and most studied industrial-strength formal methods to formally specify software systems. In this talk I will show how to use Fastest to automatically derive abstract test cases from a Z specification.
Matrices as Arrows! A Biproduct Approach to Typed Linear Algebra
Hugo Macedo (MAPi PhD student)
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of programming. The derivation of fusion, cancellation and abide laws from the biproduct equations makes it easy to calculate algorithms implementing matrix multiplication, the kernel operation of matrix algebra, ranging from its divide-and-conquer version to the conventional, iterative one. From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.
Lenses are one the most popular approaches to define bidirectional transformations between data models. A bidirectional transformation with "view-update", denoted a "lens", encompasses the definition of a forward transformation projecting "concrete models" into "abstract views", together with a backward transformation instructing how to translate an abstract view to an update over concrete models. In this presentation we show that most of the standard point-free combinators can be lifted to lenses with suitable backward semantics, allowing us to use the point-free style to define powerful bidirectional transformations by composition. We also demonstrate how to define generic lenses over arbitrary inductive data types by lifting standard recursion patterns, like folds or unfolds. To exemplify the power of this approach, we "lensify" some standard functions over naturals and lists, which are tricky to define directly "by-hand" using explicit recursion.
The GUISurfer tool: towards a language independent approach to reverse engineering GUI code
J. Carlos Silva (MAPi PhD student)
Graphical user interfaces (GUIs) are critical components of today's software. Developers are dedicating a larger portion of code to implementing them. Given their increased importance, correctness of GUIs code is becoming essential. This talk describes the latest results in the development of GUISurfer, a tool to reverse engineer the GUI layer of interactive computing systems. The ultimate goal of the tool is to enable analysis of interactive system from source code.
Can we teach computers to generate fast OLAP code?
Hugo Macedo (MAPi PhD student) and J.N. Oliveira
Inspired by previous pointfree relational approaches to data processing, we investigate how the generation of pivot tables in data mining (such as those produced by Microsoft Excel) can be expressed using matrix multiplication and transposition. This generalizes relational projections and provides a linear algebra approach to FD detection and the drill-down/roll-up operations typical of OLAP. In this context, the prospect of using SPIRAL to generate fast code for OLAP is envisaged.
Slides: there is a technical note (version of July-10th) about this talk
Formal analysis of user interfaces: state of the art and future prospects
Michael Harrison (Newcastle University)
This talk will give a (biased) survey of the use of mathematically based tools in the analysis of aspects of the user interface. It will discuss the role that these tools can play in improving interface design, how they complement more conventional HCI techniques and why their integration with existing techniques remains a future prospect. The talk will discuss future challenges and opportunities. Amongst these, scale and genericity, the prospects for tools that are accessible to HCI experts and the need for a common language will be a particular focus.
Free theorems establish interesting properties of parametrically polymorphic functions, solely from their types, and serve as a nice proof tool. For pure and lazy functional programming languages, they can be used with very few preconditions. Unfortunately, in the presence of selective strictness, as provided in languages like Haskell, their original strength is reduced. In this paper we present an approach for restrengthening them. By a refined type system which tracks the use of strict evaluation, we rule out unnecessary restrictions that otherwise emerge from the general suspicion that strict evaluation may be used at any point. Additionally, we provide an implemented algorithm determining all refined types for a given term.
Alberto Pardo, InCo, Universidad de La República, Uruguai
We show the main aspects of a compiler, written in Haskell, which preserves the property of noninterference between a simple imperative language and structured machine code with loop and branch primitives. The compiler is based on the use of typed abstract syntax (represented in terms of GADTs and type families) both for the source and target language. In this case typed abstract syntax is used to model the type system for noninterference of each language where types correspond to security types. That way it is possible, on the one hand, to use Haskell's type checker to verify that programs enforce security restrictions, and on the other hand, verify that the compiler is correct (in the sense that preserves security restrictions) by construction. Joint work with Cecilia Manzino.
Program Repair as Sound Optimization of Broken Programs
Tarmo Uustalu, Institute of Cybernetics, Tallinn University of Technology
We present a new, semantics-based approach to mechanical program repair where the intended meaning of broken programs (i.e., programs that may abort under a given, error-admitting language semantics) can be defined by a special, error-compensating semantics. Program repair can then become a compile-time, mechanical program transformation based on a program analysis. It turns a given program into one whose evaluations under the error-admitting semantics agree with those of the given program under the error-compensating semantics. We present the analysis and transformation as a type system with a transformation component, following the type-systematic approach to program optimization from our earlier work. The type-systematic method allows for simple soundness proofs of the repairs, based on a relational interpretation of the type system, as well as mechanical transformability of program correctness proofs between the Hoare logics for the error-compensating and error-admitting semantics. We first demonstrate our approach on the repair of file-handling programs with missing or superfluous open and close statements. Our framework shows that this repair is strikingly similar to partial redundancy elimination optimization commonly used by compilers. In a second example, we demonstrate the repair of programs operating a queue that can over- and underflow, including mechanical transformation of program correctness proofs. (Joint work with Bernd Fischer, Ando Saabas.)
TR-HASLab:01:2014 - Jácome Cunha, João Paulo Fernandes, Jorge Mendes, João Saraiva. Embedding, Evolution, and Validation of Model-Driven Spreadsheets. April. 2014.
TR-HASLab:02:2014 - João Saraiva et al., !SSaaPP: SpreadSheets as a Programming Paradigm. August. 2014.
TR-HASLab:03:2014 - Victor Miraldo, Object Oriented Programming with Monadic Mealy Machines (PDF). QAIS Project, October 2014.
TR-HASLab:04:2014 - Jorge Mendes, Model-driven Spreadsheets on Google Drive. December, 2014.
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).
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).
Technical Reports LaTeX style file: haslab report.sty 2011 TR HASLab:01:2011 L. S. Barbosa and Dimitrios Settas (eds). Pre Proceedings of the Fifth International ...
Languages And Tools for Critical Real time Systems The goal of this project is to contribute to a change to the current paradigm of secure ITC infrastructure, according ...
This page has been moved to the new HASLab web site at http://haslab.uminho.pt/calendar HASLab Seminar Series The HASLab Seminar Series is a scientific colloquium ...
Welcome to HASLab Our Motto "Improving Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting ...
Imprensa Universidade do Minho desenvolve aplicação que evita erros no Excel http://www.tvi.iol.pt/videos/13893309 UMinho recebe polo do INESC TEC http://www.cienciahoje ...
Working at HASLab HASLab is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of ...
Recent Publications Journal Papers J.N. Oliveira, M.A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering ...
Lemma "Improve Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting computers' behaviour. HASLab ...
Ph.D. MAP/I Doctoral Programme in Computer Science. See eg. units such as PSVC. M.Sc. Master courses in Computer science at Minho University are built upon the ...
TWiki.DI/FMHAS Web Preferences The following settings are web preferences of the TWiki.DI/FMHAS web. These preferences overwrite the site level preferences ...
Forthcoming Events GTTSE'11 4th Summer School on Generative and Transformational Techniques in Software Engineering, 2011. Past Events 2010 7th Int ...
GTTSE'11 4th Summer School on Generative and Transformational Techniques in Software Engineering, 2011 2010 7th Int. Conference on Formal Aspects of Component ...
Dependable Distributed Systems The goal is to advance the state of the art in dependable distributed data management and dependable distributed systems, in particular ...
(Under revision) 2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled ...
This is a subscription service to be automatically notified by e mail when topics change in this DI/FMHAS web. This is a convenient service, so you do not have to ...
Software technology is pre-scientific in its lack of an effective basis for predicting computers' behaviour. HASLab research aims at improving scientific standards in software design through rigorous methods and mathematical techniques.
HASLab researchers have a long tradition of linking their research to national and international industry partners, 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 (Ph.D and M.Sc) students.
The HASLab "Tripod"
Formal methods
Dependable Distributed Systems
Cryptography & Information security
Research Topics
High-assurance Model-driven Software Engineering
Foundations for architectural design (service certification, dynamic reconfiguration and self-adaptability)
Formal verification of real-time Systems
Secure embedded systems (static ckecking of embedded systems against safety policies)
Theoretical Cryptography / Provable Security
Implementation, Verification, and Analysis of Cryptographic Software
Dependability of interactive systems (model checking-based analysis of interactive systems)
Languages And Tools for Critical Real time Systems The goal of this project is to contribute to a change to the current paradigm of secure ITC infrastructure, according ...
Ph.D. MAP/I Doctoral Programme in Computer Science. See eg. units such as PSVC. M.Sc. Master courses in Computer science at Minho University are built upon the ...
Forthcoming Events GTTSE'11 4th Summer School on Generative and Transformational Techniques in Software Engineering, 2011. Past Events 2010 7th Int ...
GTTSE'11 4th Summer School on Generative and Transformational Techniques in Software Engineering, 2011 2010 7th Int. Conference on Formal Aspects of Component ...
Imprensa Universidade do Minho desenvolve aplicação que evita erros no Excel http://www.tvi.iol.pt/videos/13893309 UMinho recebe polo do INESC TEC http://www.cienciahoje ...
Working at HASLab HASLab is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of ...
Lemma "Improve Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting computers' behaviour. HASLab ...
Dependable Distributed Systems The goal is to advance the state of the art in dependable distributed data management and dependable distributed systems, in particular ...
Recent Publications Journal Papers J.N. Oliveira, M.A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering ...
This page has been moved to the new HASLab web site at http://haslab.uminho.pt/calendar HASLab Seminar Series The HASLab Seminar Series is a scientific colloquium ...
Technical Reports LaTeX style file: haslab report.sty 2011 TR HASLab:01:2011 L. S. Barbosa and Dimitrios Settas (eds). Pre Proceedings of the Fifth International ...
(Under revision) 2LT A two level data transformation system. 2LT is a deliverable of the PURe project. Examples of application include XML schema evolution coupled ...
Welcome to HASLab Our Motto "Improving Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting ...
This is a subscription service to be automatically notified by e mail when topics change in this DI/FMHAS web. This is a convenient service, so you do not have to ...
TWiki.DI/FMHAS Web Preferences The following settings are web preferences of the TWiki.DI/FMHAS web. These preferences overwrite the site level preferences ...
This is a subscription service to be automatically notified by e-mail when topics change in this DI/FMHAS 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/FMHAS 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 = HASLab
Set NATWEBLOGO = HASLab
Set WEBLOGOALT = High-Assurance Software Laboratory
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/FMHAS.Topic links.
Set SITEMAPLIST = on
Set SITEMAPWHAT = High-Assurance Software Laboratory
Set SITEMAPUSETO = High-Assurance Software Laboratory
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 #D0D0D0 .
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 #D0D0D0
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.
HASLab web
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS
The DI/FMHAS 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/FMHAS
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS
/twiki/pub/Main/LocalLogos/um_eengP.jpgTechnicalReports
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/TechnicalReports
Technical Reports LaTeX style file: haslab report.sty 2011 TR HASLab:01:2011 L. S. Barbosa and Dimitrios Settas (eds). Pre Proceedings of the Fifth International ... (last changed by JoseNunoOliveira)2020-06-19T09:48:28ZJoseNunoOliveiraBestCaseRL8
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/BestCaseRL8
Languages And Tools for Critical Real time Systems The goal of this project is to contribute to a change to the current paradigm of secure ITC infrastructure, according ... (last changed by JoseCampos)2015-11-02T00:12:05ZJoseCamposSeminar
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Seminar
This page has been moved to the new HASLab web site at http://haslab.uminho.pt/calendar HASLab Seminar Series The HASLab Seminar Series is a scientific colloquium ... (last changed by JoseNunoOliveira)2015-04-04T20:32:47ZJoseNunoOliveiraNewsHeadlines
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/NewsHeadlines
New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709 #8211;728, WSP Company. DOI: 10.1142/S0129054113400145 ... (last changed by TWikiGuest)2013-12-30T11:29:41ZguestNews
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/News
News New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709 #8211;728, WSP Company. DOI: 10.1142/S0129054113400145 ... (last changed by JoseNunoOliveira)2013-12-30T11:29:41ZJoseNunoOliveiraPeople
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/People
(All email addresses are AT di.uminho.pt) Staff Maranhão Abreu email: rui computer org http://portal.acm.org/author page.cfm?id 81321488948 ACM repositoriUM ... (last changed by PauloSilva)2013-11-25T20:31:40ZPauloSilvaWebHome
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/WebHome
Welcome to HASLab Our Motto "Improving Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting ... (last changed by JoseNunoOliveira)2013-10-25T12:27:50ZJoseNunoOliveiraPastProjects
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/PastProjects
Past Projects Research Projects (FP7) (FCT) Evolve (ADI) MathIS (FCT) (FCT) (FCT) AudioBrowser (FCT) KARMA (ADI) ... (last changed by JoseNunoOliveira)2013-10-23T09:33:56ZJoseNunoOliveiraHASLabPress
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/HASLabPress
Imprensa Universidade do Minho desenvolve aplicação que evita erros no Excel http://www.tvi.iol.pt/videos/13893309 UMinho recebe polo do INESC TEC http://www.cienciahoje ... (last changed by JacomeCunha)2013-06-14T13:26:39ZJacomeCunhaProjects
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Projects
#ResearchProjects Research Projects SmartGrids (ON.2, 2013 2015) Network Sensing for Critical Systems Monitoring (ON.2, 2013 2015) Cooperation and ... (last changed by JoseCampos)2013-06-07T23:01:04ZJoseCamposOpportunities
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Opportunities
Working at HASLab HASLab is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of ... (last changed by AlcinoCunha)2013-05-31T13:31:23ZAlcinoCunhaWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/WebSideBar
Overview Home People Selected Publications Technical Reports BookShelf Projects Seminar Blog Press ... (last changed by JoseNunoOliveira)2013-05-06T16:29:07ZJoseNunoOliveiraSelectedPublications
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/SelectedPublications
Recent Publications Journal Papers J.N. Oliveira, M.A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering ... (last changed by JoseNunoOliveira)2013-04-10T14:13:28ZJoseNunoOliveiraPastPeople
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/PastPeople
#FormerStudents Former Researchers and Ph.D Students Post Doc Visser (2003 2007) Uustalu (2000 2002) Pons (2000 2001) Barthe (1998 1999) Ph ... (last changed by JoseNunoOliveira)2013-04-10T14:09:10ZJoseNunoOliveiraLinks
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Links
#OldWebPages Sites: File System GC (VFS @ Minho) Old webpages: FAST (CCTC) and Formal Methods (DIUM) and Formal Methods Group 2361 (INESC ... (last changed by JorgeSousaPinto)2012-10-12T10:47:54ZJorgeSousaPintoResearch
http://wiki.di.uminho.pt/twiki/bin/view/DI/FMHAS/Research
Lemma "Improve Practice Through Theory" Overview Software technology is pre scientific in its lack of an effective basis for predicting computers' behaviour. HASLab ... (last changed by JorgeSousaPinto)2012-10-09T14:27:31ZJorgeSousaPinto
New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709–728, WSP Company. DOI: 10.1142/S0129054113400145
New Paper: H.D. Macedo and J.N. Oliveira. Typing Linear Algebra: a Biproduct-oriented Approach. SCP 78:11, pp.2160-2191 (DOI 10.1016/j.scico.2012.07.012)
New Paper: J.C. Campos and J. Machado, A Specification Patterns System for Discrete Event Systems Analysis, Int. J. Adv. Robotic Systems, vol. 10, 2013, doi:110.5772/56412
Job Opportunities: We are opening five post-doctoral positions. Details here
New Paper: José N. Oliveira, Miguel A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15
New Paper: J.N. Oliveira. Weighted automata as coalgebras in categories of matrices. IJFCS Vol. 24, No. 6 (2013) 709–728, WSP Company. DOI: 10.1142/S0129054113400145
New Paper: H.D. Macedo and J.N. Oliveira. Typing Linear Algebra: a Biproduct-oriented Approach. SCP 78:11, pp.2160-2191 (DOI 10.1016/j.scico.2012.07.012)
New Paper: J.C. Campos and J. Machado, A Specification Patterns System for Discrete Event Systems Analysis, Int. J. Adv. Robotic Systems, vol. 10, 2013, doi:110.5772/56412
Job Opportunities: We are opening five post-doctoral positions. Details here
New Paper: José N. Oliveira, Miguel A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study," IEEE Transactions on Software Engineering, vol. 39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15
Details here
(All email addresses are AT di.uminho.pt)
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.