Percorrer por autor "Sousa Pinto, Jorge"
A mostrar 1 - 4 de 4
Resultados por página
Opções de ordenação
- Formal Contracts for Runtime Verification Support in the Ada Programming LanguagePublication . Matos Pedro, André; Pereira, David; Pinho, Luís Miguel; Sousa Pinto, JorgeStatic Verification is not sufficient to cope with many of the challenges of modern and future generation real-time embedded systems: • state-explosion problem of model-checking; • limited automation in deductive reasoning, even with recent advances in SAT and SMT solvers. • Most of the data important to certify a real-time embedded system is related to extra-functional properties: • Duration of tasks; • Energy consumption; • Temperature management; • Other cyber-physical properties. • Unfortunately, most of the extra functional data is only available and verifiable during execution time.
- Runtime verification of autopilot systems using a fragment of MTL- ∫Publication . Pedro, André de Matos; Sousa Pinto, Jorge; Pereira, David; Pinho, Luís MiguelCurrent real-time embedded systems development frameworks lack support for the verification of properties using explicit time where counting time (i.e., durations) may play an important role in the development process. Focusing on the real-time constraints inherent to these systems, we present a framework that addresses the specification of duration properties for runtime verification by employing a fragment of metric temporal logic with durations. We also provide an overview of the framework, the synthesis tools, and the library to support monitoring properties for real-time systems developed in C++11. The results obtained provide clear evidence of the feasibility and advantages of employing a duration-sensitive formalism to increase the dependability of avionic controller systems such as the PX4 and the Ardupilot flight stacks.
- Runtime verification of autopilot systems using a fragment of MTL-∫Publication . Pedro, André; Sousa Pinto, Jorge; Pereira, David; Pinho, Luis MiguelCurrent real-time embedded systems development frameworks lack support for the verification of properties using explicit time where counting time (i.e., durations) may play an important role in the development process. Focusing on the real-time constraints inherent to these systems, we present a framework that addresses the specification of duration properties for runtime verification by employing a fragment of metric temporal logic with durations. We also provide an overview of the framework, the synthesis tools, and the library to support monitoring properties for real-time systems developed in C++11. The results obtained provide clear evidence of the feasibility and advantages of employing a duration-sensitive formalism to increase the dependability of avionic controller systems such as the PX4 and the Ardupilot flight stacks.
- SMT-based Schedulability Analysis using RMTL- RPublication . Pedro, André; Pereira, David; Pinho, Luís Miguel; Sousa Pinto, JorgeSeveral methods have been proposed for performing schedulability analysis for both uni-processor and multi-processor real-time systems. Very few of these works use the power of formal logic to write unambiguous specifications and to allow the usage of theorem provers for building the proofs of interest with greater correctness guarantees. In this paper we address this challenge by: 1) defining a formal language that allows to specify periodic resource models; 2) describe a transformational approach to reasoning about timing properties of resource models by transforming the latter specifications into a SMT problem.