High-Assurance Software Laboratory



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


DI » FMHAS » WebHome » Projects » BestCaseRL8
DI » FMHAS » Projects » 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 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 Info

Funding 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)
Start Date 1 January 2013
Duration 2.5 years
Coordinated by HASLab / INESC TEC at Departamento de Informįtica, Universidade do Minho
Principal Investigator José Creissac Campos (jose.campos@di.uminho.pt)
Telephone +351 253604447 (direct) or +351 253604430
Fax +351 253604471

Project Structure & Team

  • 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 Leader: J.S. Pinto (HASLab/INESC TEC & DI/UMinho)
    • 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


  • 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.

r10 - 02 Nov 2015 - 00:12:05 - JoseCampos
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
Syndicate this site RSSATOM