A domain-specific language to design false data injection tests for air traffic control systems
The ADS-B—automatic dependent surveillance-broadcast—technology requires aircraft to broadcast their position and velocity periodically. As compared to legacy radar technologies, coupled with alarming cyber security issues (the ADS-B protocol ...
Bringing runtime verification home: a case study on the hierarchical monitoring of smart homes using decentralized specifications
We use runtime verification (RV) to check various specifications in a smart apartment. The specifications can be broken down into three types: behavioral correctness of the apartment sensors, detection of specific user activities (known as ...
Multi-level privacy analysis of business processes: the Pleak toolset
- Marlon Dumas,
- Luciano García-Bañuelos,
- Joosep Jääger,
- Peeter Laud,
- Raimundas Matulevičius,
- Alisa Pankova,
- Martin Pettai,
- Pille Pullonen-Raudvere,
- Aivo Toots,
- Reedik Tuuling,
- Maksym Yerokhin
Privacy regulations, such as GDPR, impose strict requirements to organizations that store and process private data. Privacy-enhancing technologies (PETs), such as secure multi-party computation and differential privacy, provide mechanisms to ...
SaBRe: load-time selective binary rewriting
- Paul-Antoine Arras,
- Anastasios Andronidis,
- Luís Pina,
- Karolis Mituzas,
- Qianyi Shu,
- Daniel Grumberg,
- Cristian Cadar
Binary rewriting consists in disassembling a program to modify its instructions. However, existing solutions suffer from shortcomings in terms of soundness and performance. We present SaBRe, a load-time system for selective binary rewriting. SaBRe ...
Interface control document modeling with Citrus (avionics systems interfaces)
Avionics systems integration based on interfaces control documents (ICDs) may be well handled when leveraging the strength of the model based-engineering. Indeed, avionics systems and their internal hardware and software components interfaces, ...
Supporting safe metamodel evolution with edelta
Metamodels play a crucial role in any model-based application. They underpin the definition of models and tools, and the development of model management operations, including model transformations and analysis. Like any software artifacts, ...
Software test results exploration and visualization with continuous integration and nightly testing
Software testing is key for quality assurance of embedded systems. However, with increased development pace, the amount of test results data risks growing to a level where exploration and visualization of the results are unmanageable. This paper ...
Parameterized verification of systems with component identities, using view abstraction
The parameterized verification problem seeks to verify all members of some collection of systems. We consider the parameterized verification problem applied to systems that are composed of an arbitrary number of component processes, together with ...