Publications

Publications by HumanISE

2016

Editorial

Authors
Pinho, LM;

Publication
Ada User Journal

Abstract

2016

Towards Certified Compilation of RTFM-core Applications

Authors
Lindgren, P; Lindner, M; Pereira, D; Pinho, LM;

Publication
2016 IEEE 21ST INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA)

Abstract
Concurrent programming is dominated by thread based solutions with lock based critical sections. Careful attention has to be paid to avoid race and deadlock conditions. Real-Time for The Masses (RTFM) takes an alternative language approach, introducing tasks and named critical sections (via resources) natively in the RTFM-core language. RTFM-core programs can be compiled to native C-code, and efficiently executed onto single-core platforms under the Stack Resource Policy (SRP) by the RTFM-kernel. In this paper we formally define the well-formedness criteria for SRP based resource management, and develop a certified (formally proven) implementation of the corresponding compilation from nested critical sections of the input RTFM-core program to a resulting flat sequence of primitive operations and scheduling primitives. Moreover we formalise the properties for resource ceilings under SRP and develop a certified algorithm for their computation. The feasibility of the described approach is shown through the adoption of the Why3 platform, which allows the necessary verification conditions to be automatically generated and discharged through a variety of automatic external SMT-solvers and interactive theorem provers. Moreover, Why3 supports the extraction of certified Ocaml code for proven implementations in WhyML. As a proof of concept the certified extracted development is demonstrated on an example system.

CloseRead Abstract

2016

Editorial

Authors
Pinho, LM;

Publication
Ada User Journal

Abstract

2016

Message from the program chairs

Authors
Faucou, S; Pinho, LM;

Publication
ACM International Conference Proceeding Series

Abstract

2016

Editorial

Authors
Pinho, LM;

Publication
Ada User Journal

Abstract

2016

Requirements for the use of virtual worlds in corporate training : perspectives from the post-mortem of a corporate e-learning provider approach of Second Life and OpenSimulator

Authors
Morgado, Leonel; Paredes, Hugo; Fonseca, Benjamim; Martins, Paulo; Antunes, Ricardo; Moreira, Lúcia; Carvalho, Fausto de; Peixinho, Filipe; Santos, Arnaldo;

Publication
iLRN 2016: Immersive Learning Research Network Conference. Workshop, Short Paper and Poster Proceedings from the Second Immersive Learning Research Network Conference

Abstract
Between 2009 and 2011, a joint academia-industry effort took place to integrate Second Life and OpenSimulator platforms into a corporate elearning provider’s learning management platform. The process involved managers and lead developers at the provider and an academic engineering research team. We performed content analysis on the documents produced in this process, seeking data on the corporate perspective of requirements for virtual world platforms to be usable in everyday practice. In this paper, we present the requirements found in the documents, and detail how they emerged and evolved throughout the process.

CloseRead Abstract