Issue
Leibniz Transactions on Embedded Systems, Volume 10, Issue 1
LITES, Volume 10, Issue 1
-
Part of:
Volume:
LITES, Volume 10
Journal: Leibniz Transactions on Embedded Systems (LITES)
Publication Details
- published at: 2025-04-16
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Issue
LITES, Volume 10, Issue 1, Complete Issue
Abstract
LITES, Volume 10, Issue 1, Complete Issue
Cite as
LITES, Volume 10, Issue 1, pp. 1-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{LITES.10.1,
title = {{LITES, Volume 10, Issue 1, Complete Issue}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {1--122},
ISSN = {2199-2002},
year = {2025},
volume = {10},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1},
URN = {urn:nbn:de:0030-drops-252678},
doi = {10.4230/LITES.10.1},
annote = {Keywords: LITES, Volume 10, Issue 1, Complete Issue}
}
Document
Front Matter
Front Matter, Table of Contents
Abstract
Front Matter, Table of Contents
Cite as
LITES, Volume 10, Issue 1, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{LITES.10.1.0,
title = {{Front Matter, Table of Contents}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {0:1--0:8},
ISSN = {2199-2002},
year = {2025},
volume = {10},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.0},
URN = {urn:nbn:de:0030-drops-230179},
doi = {10.4230/LITES.10.1.0},
annote = {Keywords: Front Matter, Table of Contents}
}
Document
GDBMiner: Mining Precise Input Grammars on (Almost) Any System
Abstract
If one knows the input language of the system to be tested, one can generate inputs in a very efficient manner. Grammar-based fuzzers, for instance, produce inputs that are syntactically valid by construction. They are thus much more likely to be accepted by the program under test and to reach code beyond the input parser.
Grammar-based fuzzers, however, need a grammar in the first place. Grammar miners are set to extract such grammars from programs. However, current grammar mining tools place huge demands on the source code they are applied on, or are too imprecise, both preventing adoption in industrial practice.
We present GDBMiner, a tool to mine input grammars for binaries and executables in any (compiled) programming language, on any operating system, using any processor architecture, even without source code. GDBMiner leverages the GNU debugger (GDB) to step through the program and determine which code locations access which input bytes, generalizing bytes accessed by the same location into grammar elements.
GDBMiner is slow, but versatile - and precise: In our evaluation, GDBMiner produces grammars as precise as the (more demanding) Cmimid tool, while producing more precise grammars than the (less demanding) Arvada black-box approach. GDBMiner can be applied on any recursive descent parser that can be debugged via GDB and is available as open source.
Cite as
Max Eisele, Johannes Hägele, Christopher Huth, and Andreas Zeller. GDBMiner: Mining Precise Input Grammars on (Almost) Any System. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 1:1-1:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{eisele_et_al:LITES.10.1.1,
author = {Eisele, Max and H\"{a}gele, Johannes and Huth, Christopher and Zeller, Andreas},
title = {{GDBMiner: Mining Precise Input Grammars on (Almost) Any System}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {1:1--1:26},
ISSN = {2199-2002},
year = {2025},
volume = {10},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.1},
URN = {urn:nbn:de:0030-drops-230134},
doi = {10.4230/LITES.10.1.1},
annote = {Keywords: program analysis, testing, input grammar, fuzzing, grammar mining}
}
Document
Towards a Coq-verified Chain of Esterel Semantics
Abstract
This article focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel’s circuit semantics used by compilers to generate software code and hardware designs. The article also comes with formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics, except for the loop construct of Esterel.
Cite as
Lionel Rieg and Gérard Berry. Towards a Coq-verified Chain of Esterel Semantics. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 2:1-2:54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{rieg_et_al:LITES.10.1.2,
author = {Rieg, Lionel and Berry, G\'{e}rard},
title = {{Towards a Coq-verified Chain of Esterel Semantics}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {2:1--2:54},
ISSN = {2199-2002},
year = {2025},
volume = {10},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.2},
URN = {urn:nbn:de:0030-drops-230144},
doi = {10.4230/LITES.10.1.2},
annote = {Keywords: Esterel programming language, formal verification, Coq proof assistant}
}
Document
Limited-Preemption EDF Scheduling for Multi-Phase Secure Tasks
Abstract
Safety-critical embedded systems such as autonomous vehicles typically have only very limited computational capabilities on board that must be carefully managed to provide required enhanced functionalities. As these systems become more complex and inter-connected, some parts may need to be secured to prevent unauthorized access, or isolated to ensure correctness.
We propose the multi-phase secure (MPS) task model as a natural extension of the widely used sporadic task model for modeling both the timing and the security (and isolation) requirements for such systems. Under MPS, task phases reflect execution using different security mechanisms which each have associated execution time costs for startup and teardown. We develop corresponding limited-preemption EDF scheduling algorithms and associated pseudo-polynomial schedulability tests for constrained-deadline MPS tasks. In doing so, we provide a correction to a long-standing schedulability condition for EDF under limited-preemption. Evaluation shows that the proposed tests are efficient to compute for bounded utilizations. We empirically demonstrate that the MPS model successfully schedules more task sets compared to non-preemptive approaches.
Cite as
Benjamin Standaert, Fatima Raadia, Marion Sudvarg, Sanjoy Baruah, Thidapat Chantem, Nathan Fisher, and Christopher Gill. Limited-Preemption EDF Scheduling for Multi-Phase Secure Tasks. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 3:1-3:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{standaert_et_al:LITES.10.1.3,
author = {Standaert, Benjamin and Raadia, Fatima and Sudvarg, Marion and Baruah, Sanjoy and Chantem, Thidapat and Fisher, Nathan and Gill, Christopher},
title = {{Limited-Preemption EDF Scheduling for Multi-Phase Secure Tasks}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {3:1--3:27},
ISSN = {2199-2002},
year = {2025},
volume = {10},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.3},
URN = {urn:nbn:de:0030-drops-230799},
doi = {10.4230/LITES.10.1.3},
annote = {Keywords: real-time systems, limited-preemption scheduling, trusted execution environments}
}
Document
Revisiting Slot-Shifting’s Offline Acceptance Test for Sporadic Tasks: A Technical Note
Abstract
The Slot-Shifting algorithm presents a solution to combine the benefits of offline and online scheduling in time-triggered systems. It dynamically adjusts the allocation of time slots to tasks in the scheduling tables to accommodate aperiodic tasks at runtime. In this note, we revisit an extension to Slot-Shifting that enables it to handle sporadic task sets. In particular, we clarify the assumptions required for the correct application of its offline acceptance test, identify sources of pessimism within it, and address its schedulability analysis interval.
Cite as
Mohammad Ibrahim Alkoudsi, Damir Isovic, and Gerhard Fohler. Revisiting Slot-Shifting’s Offline Acceptance Test for Sporadic Tasks: A Technical Note. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{alkoudsi_et_al:LITES.10.1.4,
author = {Alkoudsi, Mohammad Ibrahim and Isovic, Damir and Fohler, Gerhard},
title = {{Revisiting Slot-Shifting’s Offline Acceptance Test for Sporadic Tasks: A Technical Note}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {4:1--4:6},
ISSN = {2199-2002},
year = {2025},
volume = {10},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.4},
URN = {urn:nbn:de:0030-drops-252354},
doi = {10.4230/LITES.10.1.4},
annote = {Keywords: real-time systems scheduling, time-triggered systems, offline acceptance test of sporadic tasks}
}