enter search term and/or author name
Detecting Software Cache Coherence Violations in MPSoC Using Traces Captured on Virtual Platforms
Marcos Aurélio Pinto Cunha, Omayma Matoussi, Frédéric Pétrot
Article No.: 30
Software cache coherence schemes tend to be the solution of choice in dedicated multi/many core systems on chip, as they make the hardware much simpler and predictable. However, despite the developers’ effort, it is hard to make sure that...
Dynamic Data-Cache Locking for Minimizing the WCET of a Single Task
Wenguang Zheng, Hui Wu
Article No.: 31
Caches have been widely used in modern embedded processors to bridge the increasing speed gap between processors and off-chip memory. In real-time embedded systems, computing the Worst-Case Execution Time (WCET) of a task is essential for the task...
Compiler-Directed Soft Error Detection and Recovery to Avoid DUE and SDC via Tail-DMR
Qingrui Liu, Changhee Jung, Dongyoon Lee, Devesh Tiwari
Article No.: 32
This article presents Clover, a compiler-directed soft error detection and recovery scheme for lightweight soft error resilience. The compiler carefully generates soft-error-tolerant code based on idempotent processing without explicit...
There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system...
Eager Synching: A Selective Logging Strategy for Fast fsync() on Flash-Based Android Devices
Li-Pin Chang, Po-Han Sung, Po-Tsang Chen, Po-Hung Chen
Article No.: 34
Flash storage has been a standard component in Android devices. Recent research has reported that application data management in Android involves frequent fsync() operations. The current fsync() implementations, including those of ext4 and F2FS,...
Global Optimization of Fixed-Priority Real-Time Systems by RTOS-Aware Control-Flow Analysis
Christian Dietrich, Martin Hoffmann, Daniel Lohmann
Article No.: 35
Cyber--physical systems typically target a dedicated purpose; their embedded real-time control system, such as an automotive control unit, is designed with a well-defined set of functionalities. On the software side, this results in a large amount...
Cost savings are very critical in modern heterogeneous computing systems, especially in embedded systems. Task scheduling plays an important role in cost savings. In this article, we tackle the problem of scheduling tasks on heterogeneous...
From a Formalized Parallel Action Language to Its Efficient Code Generation
Ivan Llopard, Christian Fabre, Albert Cohen
Article No.: 37
Modeling languages propose convenient abstractions and transformations to handle the complexity of today’s embedded systems. Based on the formalism of the Hierarchical State Machine, they enable the expression of hierarchical control...
Stanislav Manilov, Björn Franke, Anthony Magrath, Cedric Andrieu
Article No.: 38
Section: Special Issue on LCETES
Message from the Guest Editors
Stefan Haar, Roland Meyer
Article No.: 40
Testing Preorders for dMTS: Deadlock- and the New Deadlock-/DivergenceTesting
Ferenc Bujtor, Lev Sorokin, Walter Vogler
Article No.: 41
Testing preorders on component specifications ensure that replacing a specification by a refined one does not introduce unwanted behavior in an overall system. Considering deadlocks as unwanted, the preorder can be characterized by a failure...
Multi-valued Simulation and Abstraction Using Lattice Operations
Stefan Vijzelaar, Wan Fokkink
Article No.: 42
Abstractions can cause spurious results, which need to be verified in the concrete system to gain conclusive results. Verification based on a multi-valued logic can distinguish between conclusive and inconclusive results, provides increased...
Preserving Partial-Order Runs in Parametric Time Petri Nets
Étienne André, Thomas Chatain, César Rodríguez
Article No.: 43
Parameter synthesis for timed systems aims at deriving parameter valuations satisfying a given property. In this article, we target concurrent systems. We use partial-order semantics for parametric time Petri nets as a way to both cope with the...
Non-interference (NI) is a property of systems stating that confidential actions should not cause effects observable by unauthorized users. Several variants of NI have been studied for many types of models but rarely for true concurrency or...
Minimizing Test Suites with Unfoldings of Multithreaded Programs
Olli Saarikivi, Hernán Ponce-De-León, Kari Kähkönen, Keijo Heljanko, Javier Esparza
Article No.: 45
This article focuses on computing minimal test suites for multithreaded programs. Based on previous work on test case generation for multithreaded programs using unfoldings, this article shows how this unfolding can be used to generate minimal...
This publication discusses how automatic verification of concurrent systems can be made more efficient by focusing on always may-terminating systems. First, making a system always may-terminating is a method for meeting a modelling need...
Incremental Inductive Verification of Parameterized Timed Systems
Article No.: 47
We propose and extend an approach for the verification of safety properties for parameterized timed systems modeled as networks of timed automata. For this task, we introduce an incremental workflow that is based on our algorithm IC3 with...
When Do We Not Need Complex Assume-Guarantee Rules?
Antti Siirtola, Stavros Tripakis, Keijo Heljanko
Article No.: 48
We study the need for complex circular assume-guarantee (AG) rules in formalisms that already provide the simple precongruence rule. We first investigate the question for two popular formalisms: Labeled Transition Systems (LTSs) with weak...
Section: Special Issue on LCETES
While the increasing digitalization of our society and amalgamation of embedded devices into the ever-increasing facets of our daily life (e.g., in smart and intelligent vehicles, smart cities and smart nations, and critical infrastructure...
DLSeF: A Dynamic Key-Length-Based Efficient Real-Time Security Verification Model for Big Data Stream
Deepak Puthal, Surya Nepal, Rajiv Ranjan, Jinjun Chen
Article No.: 51
Applications in risk-critical domains such as emergency management and industrial control systems need near-real-time stream data processing in large-scale sensing networks. The key problem is how to ensure online end-to-end security (e.g.,...
Ensuring the security and privacy of vehicular ad hoc networks (VANETs) and related services such as secure payment has been the focus of recent research efforts. Existing secure payment solutions generally require stable and reliable network...
Efficient Elliptic Curve Cryptography for Embedded Devices
Zhe Liu, Jian Weng, Zhi Hu, Hwajeong Seo
Article No.: 53
Many resource-constrained embedded devices, such as wireless sensor nodes, require public key encryption or a digital signature, which has induced plenty of research on efficient and secure implementation of elliptic curve cryptography (ECC) on...
Differential Fault Attack (DFA) is a powerful cryptanalytic technique to retrieve secret keys by exploiting the faulty ciphertexts generated during encryption procedure. This article proposes a novel DFA attack that is effective on ITUbee,...
Reduction in the Number of Fault Injections for Blind Fault Attack on SPN Block Ciphers
Yang Li, Mengting Chen, Zhe Liu, Jian Wang
Article No.: 55
In 2014, a new fault analysis called blind fault attack (BFA) was proposed, in which attackers can only obtain the number of different faulty outputs without knowing the public data. The original BFA requires 480,000 fault injections to...
On-Board Format-Independent Security of Functional Magnetic Resonance Images
Arcangelo Castiglione, Raffaele Pizzolante, Francesco Palmieri, Barbara Masucci, Bruno Carpentieri, Alfredo De Santis, Aniello Castiglione
Article No.: 56
Functional magnetic resonance imaging (fMRI) provides an effective and noninvasive tool for researchers to understand cerebral functions and correlate them with brain activities. In addition, with the ever-increasing diffusion of the Internet,...
Electronic healthcare (eHealth) systems have replaced traditional paper-based medical systems due to attractive features such as universal accessibility, high accuracy, and low cost. As a major constituent part of eHealth systems, mobile...
When competing in eBay bidding, online games, or e-exams in embedded computing environments, people naturally face asynchronous starts from different computing devices, which is treated as a security risk of online contests. The security risks of...
Fault Detection Architectures for Post-Quantum Cryptographic Stateless Hash-Based Secure Signatures Benchmarked on ASIC
Mehran Mozaffari-Kermani, Reza Azarderakhsh, Anita Aghaie
Article No.: 59
Symmetric-key cryptography can resist the potential post-quantum attacks expected with the not-so-faraway advent of quantum computing power. Hash-based, code-based, lattice-based, and multivariate-quadratic equations are all other potential...
The expected advanced network explorations and the growing demand for mobile data sharing and transferring have driven numerous novel applications in Cyber-Physical Systems (CPSs), such as Intelligent Transportation Systems (ITSs)....
Smart mobile devices are becoming the main vessel of personal privacy information. While they carry valuable information, data erasure is somehow much more vulnerable than was predicted. The security mechanisms provided by the Android system are...