Percorrer por autor "Spilere Nandi, Giann"
A mostrar 1 - 5 de 5
Resultados por página
Opções de ordenação
- Reducing the gap between theory and practice in real-time systems with MARSPublication . 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 opportunity for new platform-specific research directions to emerge. In this work we discuss the use and development of an open-source tool named MARS capable of porting various scheduling tests and algorithms to hardware platforms used in distributed real-time dependable systems.
- Security in Wireless Sensor Networks: A formal verification of protocolsPublication . 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 together with safe and secure transmissions. Notably, in what concerns security aspects, several cryptographic protocols have been proposed. Since the design of these protocols is usually error-prone, security breaches can still be exposed and MALICIOUSly exploited unless they are rigorously analyzed and verified. In this paper we formally verify, using ProVerif, three cryptographic protocols used in WSN, regarding the security properties of secrecy and authenticity. The security analysis performed in this paper is more robust than the ones performed in related work. Our contributions involve analyzing protocols that were modeled considering an unbounded number of participants and actions, and also the use of a hierarchical system to classify the authenticity results. Our verification shows that the three analyzed protocols guarantee secrecy, but can only provide authenticity in specific scenarios.
- Towards the safe deployment of runtime monitors in mode-change supported Cyber- Physical SystemsPublication . 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 framework capable of analyzing the schedulability of a set of mode-change supporting Cyber-Physical Systems in the presence of coupled runtime monitors.
- Verification of multiple models of a safetycritical motor controller in railway systemsPublication . 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. This paper describes our work in the context of the European VALU3S project to integrate the analysis of such systems with the Uppaal model checker during the development cycle, involving both developers from Alstom and academic partners. We use special Excel tables to configure the underlying Uppaal models and requirements, bridging these two stakeholders. We follow Software Product Line Engineering principles, e.g., allowing features to be turned on and off and periodicities to be changed, and verify different properties for each of such configuration. We automate the instantiation and verification in Uppaal of a set of selected configurations via an open-source prototype tool named Uppex.
- Work-In-Progress: a DSL for the safe deployment of Runtime Monitors in Cyber-Physical SystemsPublication . 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 combines the formal specification of properties to be validated and monitors that perform these validations during runtime. Although helpful, runtime verification solutions introduce an inevitable overhead in the system, which can disrupt its correct functioning if not safely employed. We propose the creation of a Domain Specific Language (DSL) that, given a generic CPS, 1) verifies if its real- time scheduling is guaranteed, even in the presence of coupled monitors, and 2) implements several verification conditions for the correct-by-construction generation of monitoring architectures. To achieve it, we plan to perform statical verifications, derived from the available literature on schedulability analysis, and powered by a set of semi-automatic formal verification tools.