Browsing by Author "Nandi, Giann"
Now showing 1 - 3 of 3
Results Per Page
Sort Options
- 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.
- 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.
- Towards the design of a DSL to enable the secure Runtime Monitoring and Verification of Safety-Critical CPSPublication . Nandi, GiannSafety-critical systems commonly face unpredictable and hostile environments, with emergent behaviors and with a growing number of external, malicious attackers. These are risk factors that should be taken into account during these systems design phases, but that is not always possible due to the overall complexity of the interaction between the systems and its external operational environment. Cyber-Physical Systems (CPS) are notable examples of practical implementations of safety-critical systems. Being able to guarantee that safetycritical CPS do not fail upon operation can easily become a huge challenge, depending on how complex the system is. Among the most promising approaches to reduce the complexity of designing safety-critical CPS are Runtime Monitoring (RM) (Watterson and Heffernan 2017) and Runtime Verification (RV) (Bartocci Et al. 2018), where monitors are generated and orchestrated in a software architecture that can be coupled to the target system, observe it during its execution, and identify aspects that were not foreseen during design phase, or that could not be proved to be absent via static verification methods. Monitors can be used to verify the correct functioning of a system by analyzing direct (and/or indirect) aspects of it. This can be especially useful when considering a security-oriented point of view, where monitors can identify possible security attacks to a system when exposed to the events taking place or the patterns of data being processed.