Publications

Publications by Luis Miguel Pinho

2015

Editorial

Authors
Pinho L.M.;

Publication
Ada User Journal

Abstract

2015

Preface

Authors
Pinho L.; Karl W.; Cohen A.; Brinkschulte U.;

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract

2015

Editorial

Authors
Pinho, LM;

Publication
Ada User Journal

Abstract

2015

Editorial

Authors
Pinho, LM;

Publication
Ada User Journal

Abstract

2015

Abstract Timers and their Implementation onto the ARM Cortex-M family of MCUs

Authors
Lindgren, P; Fresk, E; Lindner, M; Lulea, AL; Pereira, D; Pinho, LM;

Publication
CEUR Workshop Proceedings

Abstract
Real-Time For the Masses (RTFM) is a set of languages and tools being developed to facilitate embedded software development and provide highly efficient implementations geared to static verification. The RTFM-kernel is an architecture designed to provide highly efficient and predicable Stack Resource Policy based scheduling, targeting bare metal (singlecore) platforms. We contribute beyond prior work by introducing a platform independent timer abstraction that relies on existing RTFM-kernel primitives. We develop two alternative implementations for the ARM Cortex-M family of MCUs: a generic implementation, using the ARM defined SysTick- /DWT hardware; and a target specific implementation, using the match compare/free running timers. While sacrificing generality, the latter is more exible and may reduce overall overhead. Invariants for correctness are presented, and methods to static and run-time verification are discussed. Overhead is bound and characterized. In both cases the critical section from release time to dispatch is less than 2us on a 100MHz MCU. Queue and timer mechanisms are directly implemented in the RTFM-core language and can be included in system-wide scheduling analysis.

CloseRead Abstract

2015

Editorial

Authors
Pinho, LM;

Publication
Ada User Journal

Abstract