46 documents found, page 1 of 5
MARS: Safely instrumenting runtime monitors in real-time resource-constrained d...
Nandi, Giann; Pereira, David; Proenca, José; Tovar, EduardoAdvancements in the energy efficiency and computational power of embedded devices allow developers to equip resource-constrained systems with a greater number of features and more complex behavior. As complexity of a system grows, so does the difficulty in demonstrating its overall correctness. Formal methods have been successfully applied in a variety of verification and validation scenarios, but their wide ad...
Reducing the gap between theory and practice in real-time systems with MARS
Spilere Nandi, Giann; Pereira, David; Proença, José; Tovar, Eduardo; Nogueira, LuísA significant number of dependable systems rely on scheduling algorithms to achieve temporal correctness. Despite their relevance in real-world applications, only a narrow subset of the works in the literature of real-time systems are readily available to be reproduced in real-world hardware platforms. This lack of support not only hinders the reproducibility of research results, but also reduces the opportunit...
Verification of multiple models of a safetycritical motor controller in railway...
Proenca, José; Borrami, Sina; Nova, Jorge Sanchez de; Pereira, David; Spilere Nandi, GiannMotor controllers, such as the ones used in signalling systems, include critical embedded software. Alstom is a company that produces such embedded systems, which must follow complex certification processes that require formal modelling and analysis. The formal analysis of these real-time systems have to balance between including enough details to be useful and abstracting away enough details to be verifiable. ...
MARS: a toolset for the safe and secure deployment of heterogeneous distributed...
Nandi, Giann; Pereira, David; Proenca, José; Santos, José; Rodrigues, Lourenço A.; Lourenço, André; Tovar, EduardoThis work discusses the ongoing development of a toolset named MARS aimed to ease the process of safely deploying runtime verification monitors into distributed micro-ROS and ROS2 nodes. The work is motivated by a use case in the health and automotive domains and covers safety/security concerns around the manipulation of sensitive biometric data.
Towards the safe deployment of runtime monitors in mode-change supported Cyber-...
Spilere Nandi, Giann; Pereira, David; Proenca, José; Tovar, EduardoComplex safety-critical Cyber-Physical Systems require modern approaches that can provide evidence of their correct functioning. Among the many state-of-the-art approaches is runtime verification, which constantly verifies if a system’s behavior complies with its specification. However, the coupling of monitors causes an inevitable overhead that could compromise the system’s safety. We present the concept of a ...
Sound production in the Meagre, Argyrosomus regius (Asso, 1801): intraspecific ...
Pereira, David; Vieira, Manuel; Pousão-Ferreira, Pedro; Candeias-Mendes, Ana; Barata, Marisa; Fonseca, Paulo; Amorim, Maria Clara PessoaMany fish taxa produce sound in voluntary and in disturbance contexts but information on the full acoustic repertoire is lacking for most species. Yet, this knowledge is critical to enable monitoring fish populations in nature through acoustic monitoring.
Work-In-Progress: a DSL for the safe deployment of Runtime Monitors in Cyber-Ph...
Spilere Nandi, Giann; Pereira, David; Proenca, José; Tovar, EduardoGuaranteeing that safety-critical Cyber-Physical Systems (CPS) do not fail upon deployment is becoming an even more complicated task with the increased use of complex software solutions. To aid in this matter, formal methods (rigorous mathematical and logical techniques) can be used to obtain proofs about the correctness of CPS. In such a context, Runtime Verification has emerged as a promising solution that co...
Real-time MTL with durations as SMT with applications to schedulability analysis
Matos, Andre de; Leucker, Martin; Pereira, David; Pinto, Jorge SousaThis paper introduces a synthesis procedure for the satisfiability problem of RMTL- ∫ formulas as SAT solving modulo theories. RMTL- ∫ is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and ...
Real-time MTL with durations as SMT with applications to schedulability analysis
Pedro, André de Matos; Leucker, Martin; Pereira, David; Pinto, Jorge SousaThis paper introduces a synthesis procedure for the satisfiability problem of RMTL-D formulas as SAT solving modulo theories. RMTL-D is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and ma...
Security in Wireless Sensor Networks: A formal verification of protocols
Spilere Nandi, Giann; Pereira, David; Vigil, Martín; Moraes, Ricardo; Schiaffino Morales, Analúcia; Araújo, GustavoThe increase of the digitalization taking place in various industrial domains is leading developers towards the design and implementation of more and more complex networked control systems (NCS) supported by Wireless Sensor Networks (WSN). This naturally raises new challenges for the current WSN technology, namely in what concerns improved guarantees of technical aspects such as real-time communications togethe...