Loading...
4 results
Search Results
Now showing 1 - 4 of 4
- 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.
- 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.
- MARS: Safely instrumenting runtime monitors in real-time resource-constrained distributed systemsPublication . 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 adoption in the industry and academia is still lackluster. Among the explanations listed in the literature for the low adoption of these techniques are the perceived difficulty of getting into formal practices and how formal tools are not usually aimed at practical use cases. Striving to address these issues, we present MARS, an open-source domain-specific language for the safe instrumentation of runtime verification monitors into real-time resource-constrained distributed systems. Our main objective with MARS is to ease the integration of runtime verification monitors in distributed applications while also providing developers with evidence of their correct instrumentation in the context of systems where dependability and temporal requirements need to be respected even under extreme resource constraints. We present the language syntax, the set of tools embedded into its compiler, its functionalities, and a use case to exemplify its use in a practical distributed application.
- MARS: a toolset for the safe and secure deployment of heterogeneous distributed systemsPublication . 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.