2024-03-28T13:14:56Z
https://ojs.dagstuhl.de/index.php/lites/oai
oai:ojs.dagstuhl.de:article/36
2016-02-18T09:51:01Z
lites:ART
driver
nmb a2200000Iu 4500
"141114 2014 eng "
2199-2002
10.4230/LITES-v001-i002-a002
doi
dc
Computation Offloading for Frame-Based Real-Time Tasks under Given Server Response Time Guarantees
Toma, Anas S. M.
Institute for Process Control and Robotics, Department of Informatics, Karlsruhe Institute of Technology (KIT), Germany https://mta.ipr.kit.edu/staffs_atoma.php
Chen, Jian-Jia
Department of Informatics, TU Dortmund University, Germany http://ls12-www.cs.tu-dortmund.de/daes/en/daes/mitarbeiter/prof-dr-jian-jia-chen.html
Array
Computation offloading has been adopted to improve the performance of embedded systems by offloading the computation of some tasks, especially computation-intensive tasks, to servers or clouds. This paper explores computation offloading for real-time tasks in embedded systems, provided given response time guarantees from the servers, to decide which tasks should be offloaded to get the results in time. We consider frame-based real-time tasks with the same period and relative deadline. When the execution order of the tasks is given, the problem can be solved in linear time. However, when the execution order is not specified, we prove that the problem is NP-complete. We develop a pseudo-polynomial-time algorithm for deriving feasible schedules, if they exist. An approximation scheme is also developed to trade the error made from the algorithm and the complexity. Our algorithms are extended to minimize the period/relative deadline of the tasks for performance maximization. The algorithms are evaluated with a case study for a surveillance system and synthesized benchmarks.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2014-09-12 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v001-i002-a002
Leibniz Transactions on Embedded Systems; Vol. 1 No. 2 (2014)
eng
Copyright (c) 2014 Anas S. M. Toma, Jian-Jia Chen
oai:ojs.dagstuhl.de:article/37
2016-02-18T09:50:54Z
lites:ART
driver
nmb a2200000Iu 4500
"140425 2014 eng "
2199-2002
10.4230/LITES-v001-i001-a002
doi
dc
TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox
Helmstetter, Claude
Verimag - CNRS
2 Avenue de Vignate, 38610 Gières, France
Array
SystemC/TLM models, which are C++ programs, allow the simulation of embedded software before hardware low-level descriptions are available and are used as golden models for hardware verification. The verification of the SystemC/TLM models is an important issue since an error in the model can mislead the system designers or reveal an error in the specifications. An open-source simulator for SystemC/TLM is provided but there are no tools for formal verification.
In order to apply model checking to a SystemC/TLM model, a semantics for standard C++ code and for specific SystemC/TLM features must be provided. The usual approach relies on the translation of the SystemC/TLM code into a formal language for which a model checker is available.
We propose another approach that suppresses the error-prone translation effort. Given a SystemC/TLM program, the transitions are obtained by executing the original code using g++ and an extended SystemC library, and we ask the user to provide additional functions to store the current model state. These additional functions generally represent less than 20% of the size of the original model, and allow it to apply all CADP verification tools to the SystemC/TLM model itself.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2014-04-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v001-i001-a002
Leibniz Transactions on Embedded Systems; Vol. 1 No. 1 (2014)
eng
Copyright (c) 2014 Claude Helmstetter
oai:ojs.dagstuhl.de:article/40
2016-02-18T09:50:53Z
lites:ART
driver
nmb a2200000Iu 4500
"140414 2014 eng "
2199-2002
10.4230/LITES-v001-i001-a001
doi
dc
A Comparison between Fixed Priority and EDF Scheduling accounting for Cache Related Pre-emption Delays
Lunniss, Will
University of York http://www-users.cs.york.ac.uk/~wlunniss/
Altmeyer, Sebastian
University of Amsterdam
Davis, Robert I.
University of York
Array
In multitasking real-time systems, the choice of scheduling algorithm is an important factor to ensure that response time requirements are met while maximising limited system resources. Two popular scheduling algorithms include fixed priority (FP) and earliest deadline first (EDF). While they have been studied in great detail before, they have not been compared when taking into account cache related pre-emption delays (CRPD). Memory and cache are split into a number of blocks containing instructions and data. During a pre-emption, cache blocks from the pre-empting task can evict those of the pre-empted task. When the pre-empted task is resumed, if it then has to re-load the evicted blocks, CRPD are introduced which then affect the schedulability of the task.
In this paper we compare FP and EDF scheduling algorithms in the presence of CRPD using the state-of-the-art CRPD analysis. We find that when CRPD is accounted for, the performance gains offered by EDF over FP, while still notable, are diminished. Furthermore, we find that under scenarios that cause relatively high CRPD, task layout optimisation techniques can be applied to allow FP to schedule tasksets at a similar processor utilisation to EDF. Thus making the choice of the task layout in memory as important as the choice of scheduling algorithm. This is very relevant for industry, as it is much cheaper and simpler to adjust the task layout through the linker than it is to switch the scheduling algorithm.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2014-04-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v001-i001-a001
Leibniz Transactions on Embedded Systems; Vol. 1 No. 1 (2014)
eng
Copyright (c) 2014 Will Lunniss, Sebastian Altmeyer, Robert I. Davis
oai:ojs.dagstuhl.de:article/41
2016-02-18T09:51:00Z
lites:ART
driver
nmb a2200000Iu 4500
"140912 2014 eng "
2199-2002
10.4230/LITES-v001-i002-a001
doi
dc
Blocking Optimality in Distributed Real-Time Locking Protocols
Brandenburg, Björn Bernhard
Max Planck Institute for Software Systems (MPI-SWS) http://www.mpi-sws.org/~bbb
Array
Lower and upper bounds on the maximum priority inversion blocking (pi-blocking) that is generally unavoidable in distributed multiprocessor real-time locking protocols (where resources may be accessed only from specific synchronization processors) are established. Prior work on suspension-based shared-memory multiprocessor locking protocols (which require resources to be accessible from all processors) has established asymptotically tight bounds of Ω(m) and Ω(n) maximum pi-blocking under suspension-oblivious and suspension-aware analysis, respectively, where m denotes the total number of processors and n denotes the number of tasks. In this paper, it is shown that, in the case of distributed semaphore protocols, there exist two different task allocation scenarios that give rise to distinct lower bounds. In the case of co-hosted task allocation, where application tasks may also be assigned to synchronization processors (i.e., processors hosting critical sections), Ω(Φ · n) maximum pi-blocking is unavoidable for some tasks under any locking protocol under both suspension-aware and suspension-oblivious schedulability analysis, where Φ denotes the ratio of the maximum response time to the shortest period. In contrast, in the case of disjoint task allocation (i.e., if application tasks may not be assigned to synchronization processors), only Ω(m) and Ω(n) maximum pi-blocking is fundamentally unavoidable under suspension-oblivious and suspension-aware analysis, respectively, as in the shared-memory case. These bounds are shown to be asymptotically tight with the construction of two new distributed real-time locking protocols that ensure O(m) and O(n) maximum pi-blocking under suspension-oblivious and suspension-aware analysis, respectively.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2014-09-12 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v001-i002-a001
Leibniz Transactions on Embedded Systems; Vol. 1 No. 2 (2014)
eng
Copyright (c) 2014 Björn Bernhard Brandenburg
oai:ojs.dagstuhl.de:article/43
2018-01-08T10:43:32Z
lites:ART
driver
nmb a2200000Iu 4500
"151130 2015 eng "
2199-2002
10.4230/LITES-v002-i002-a001
doi
dc
From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation
Carle, Thomas
Brown University
247 Browen Street, Providence, Rhode Island 02906 http://orcid.org/0000-0002-1411-1030
Potop-Butucaru, Dumitru
INRIA Paris-Rocquencourt
Domaine de Voluceau, Rocquencourt - B.P. 105, 78153 Le Chesnay http://orcid.org/0000-0003-3672-6156
Sorel, Yves
INRIA Paris-Rocquencourt
Domaine de Voluceau, Rocquencourt - B.P. 105, 78153 Le Chesnay
Lesens, David
Airbus Defence & Space
Route de Verneuil, 78133 Les Mureaux, France http://orcid.org/0000-0002-3452-9960
Array
Our objective is to facilitate the development of complex time-triggered systems by automating the allocation and scheduling steps. We show that full automation is possible while taking into account the elements of complexity needed by a complex embedded control system. More precisely, we consider deterministic functional specifications provided (as often in an industrial setting) by means of synchronous data-flow models with multiple modes and multiple relative periods. We first extend this functional model with an original real-time characterization that takes advantage of our time-triggered framework to provide a simpler representation of complex end-to-end flow requirements. We also extend our specifications with additional non-functional properties specifying partitioning, allocation, and preemptability constraints. Then, we provide novel algorithms for the off-line scheduling of these extended specifications onto partitioned time-triggered architectures à la ARINC 653. The main originality of our work is that it takes into account at the same time multiple complexity elements: various types of non-functional properties (real-time, partitioning, allocation, preemptability) and functional specifications with conditional execution and multiple modes. Allocation of time slots/windows to partitions can be fully or partially provided, or synthesized by our tool. Our algorithms allow the automatic allocation and scheduling onto multi-processor (distributed) systems with a global time base, taking into account communication costs. We demonstrate our technique on a model of space flight software system with strong real-time determinism requirements.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2015-11-30 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v002-i002-a001
Leibniz Transactions on Embedded Systems; Vol. 2 No. 2 (2015)
eng
Copyright (c) 2015 Thomas Carle, Dumitru Potop-Butucaru, Yves Sorel, and David Lesens
oai:ojs.dagstuhl.de:article/45
2016-02-18T09:50:58Z
lites:ART
driver
nmb a2200000Iu 4500
"140610 2014 eng "
2199-2002
10.4230/LITES-v001-i001-a003
doi
dc
Randomized Caches Considered Harmful in Hard Real-Time Systems
Reineke, Jan
Saarland University http://embedded.cs.uni-saarland.de/reineke.php http://orcid.org/0000-0002-3459-2214
Array
We investigate the suitability of caches with randomized placement and replacement in the context of hard real-time systems. Such caches have been claimed to drastically reduce the amount of information required by static worst-case execution time (WCET) analysis, and to be an enabler for measurement-based probabilistic timing analysis. We refute these claims and conclude that with prevailing static and measurement-based analysis techniques caches with deterministic placement and least-recently-used replacement are preferable over randomized ones.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2014-04-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v001-i001-a003
Leibniz Transactions on Embedded Systems; Vol. 1 No. 1 (2014)
eng
Copyright (c) 2014 Jan Reineke
oai:ojs.dagstuhl.de:article/49
2016-02-18T09:51:03Z
lites:ART
driver
nmb a2200000Iu 4500
"141117 2014 eng "
2199-2002
10.4230/LITES-v001-i002-a003
doi
dc
Implementing Mixed-criticality Systems Upon a Preemptive Varying-speed Processor
Guo, Zhishan
University of North Carolina, Chapel Hill, NC, USA
Baruah, Sanjoy K.
University of North Carolina, Chapel Hill, NC, USA
Array
A mixed criticality (MC) workload consists of components of varying degrees of importance (or "criticalities"); the more critical components typically need to have their correctness validated to greater levels of assurance than the less critical ones. The problem of executing such a MC workload upon a preemptive processor whose effective speed may vary during run-time, in a manner that is not completely known prior to run-time, is considered.
Such a processor is modeled as being characterized by several execution speeds: a normal speed and several levels of degraded speed. Under normal circumstances it will execute at or above its normal speed; conditions during run-time may cause it to execute slower. It is desired that all components of the MC workload execute correctly under normal circumstances. If the processor speed degrades, it should nevertheless remain the case that the more critical components execute correctly (although the less critical ones need not do so).
In this work, we derive an optimal algorithm for scheduling MC workloads upon such platforms; achieving optimality does not require that the processor be able to monitor its own run-time speed. For the sub-case of the general problem where there are only two criticality levels defined, we additionally provide an implementation that is asymptotically optimal in terms of run-time efficiency.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2014-09-12 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v001-i002-a003
Leibniz Transactions on Embedded Systems; Vol. 1 No. 2 (2014)
eng
Copyright (c) 2014 Zhishan Guo, Sanjoy K. Baruah
oai:ojs.dagstuhl.de:article/50
2016-02-18T09:50:56Z
lites:FOR
driver
nmb a2200000Iu 4500
"140610 2014 eng "
2199-2002
10.4230/LITES-v001-i001-a000
doi
dc
Foreword
Burns, Alan
University of York
I would like to welcome all readers to the first issue of this new not-for-profit open access journal: the Leibniz Transactions on Embedded Systems (LITES). Unless you have come across this journal by accident then you will already understand the key role that embedded systems have in modern life. One can hardly think of a single human activity that is not underpinned by such systems; transport, entertainment, supply lines for supermarkets, health care and drug production, energy production and transmission, robotic manufacturing, control systems and communication media of all kinds are now dependent on the fusion of embedded hardware and software. For researchers in this domain this provides great opportunities but also responsibilities. We need to make sure that society can justifiable rely on technology that is increasing beyond the understanding of most ordinary people. Computer-based technologies have been described as modern magic; it follows that we are therefore magicians. But the spells we cast must be based on sound principles, solid theory and demonstrable performance.
One of the influences that embedded and other IT technology has had in the last decade is in publishing itself. Online services are now the norm. And early and open access to publicly funded research is now rightly demanded by Government bodies and related funding councils. This new journal has been created to meet this challenge. All papers are open access, with copyright being retained by the authors. Moreover, only a small fee is charged to authors due to low operational overheads and the support of Google and the Klaus Tschira Stiftung. But the lack of a physical page limit in an online-only journal does not mean that quality is undermined. All papers are thoroughly reviewed, with only the best work, in terms of originality and rigour, being accepted. Our aim is to evolve an excellent and effective venue for publish scholarly articles. To help achieve this aim LITES benefits greatly from having the name and reputation of Schloss Dagstuhl behind it.
The volume of research material produced world-wide relating to embedded systems has lead to the spawning of many conferences and workshops, special issues and focused publications. In LITES we intend to cater for the broadest collection of relevant topics. We currently have subject editors to cover: the design, implementation, verification, and testing of embedded hardware and software systems; the theoretical foundations; single-core, multi-processor and networked architectures and their energy consumption and predictability properties; reliability and fault tolerance; security properties; applications in the avionics, automotive, telecommunication, medical and production domains; cyber-physical systems; high performance and real-time embedded systems; and hybrid systems. This is an impressive list, but it is not exhaustive. New areas will emerge and new editors will be appointed.
LITES obtains its governance from EDAA (European Design and Automation Association) and EMSIG (Embedded Systems Special Interest Group) as a joint endeavour with Schloss Dagstuhl. EDAA/EMSIG appoint the Editor-in-Chief (EiC) and the subject area editors. The terms for editors is four years, renewable once. All editorial work is done voluntarily.
The first few issues of the journal will contain standard papers that have been through the review process. Later, comments on previously published papers will be allowed and commentaries included that will help the reader trace forward the influence of each paper. Comments will be reviewed; commentaries will just need to be passed by the EiC.
I hope that as a reader you will find the papers in this journal of interest and often inspirational. As a researcher I hope you will consider it as a worthy place to entrust your work. All the editorial team will work towards building up the reputation of the journal. I hope the community at large will be part of that journey.
I am proud to be the founding EiC of this journal, but I promise not to include editorials in future issues. The papers are quite capable of introducing themselves.
Alan Burns
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2014-04-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v001-i001-a000
Leibniz Transactions on Embedded Systems; Vol. 1 No. 1 (2014)
eng
Copyright (c) 2014 Alan Burns
oai:ojs.dagstuhl.de:article/51
2018-01-08T10:43:59Z
lites:ART
driver
nmb a2200000Iu 4500
"150323 2015 eng "
2199-2002
10.4230/LITES-v002-i001-a001
doi
dc
Randomized Caches Can Be Pretty Useful to Hard Real-Time Systems
Mezzetti, Enrico
University of Padova
Ziccardi, Marco
University of Padova
Vardanega, Tullio
University of Padova http://orcid.org/0000-0002-0089-0889
Abella, Jaume
Barcelona Supercomputing Center (BSC-CNS)
Quiñones, Eduardo
Barcelona Supercomputing Center (BSC-CNS)
Cazorla, Francisco J.
Barcelona Supercomputing Center (BSC-CNS) and Spanish National Research Council (IIIA-CSIC)
Array
Cache randomization per se, and its viability for probabilistic timing analysis (PTA) of critical real-time systems, are receiving increasingly close attention from the scientific community and the industrial practitioners. In fact, the very notion of introducing randomness and probabilities in time-critical systems has caused strenuous debates owing to the apparent clash that this idea has with the strictly deterministic view traditionally held for those systems. A paper recently appeared in LITES (Reineke, J. (2014). Randomized Caches Considered Harmful in Hard Real-Time Systems. LITES, 1(1), 03:1-03:13.) provides a critical analysis of the weaknesses and risks entailed in using randomized caches in hard real-time systems. In order to provide the interested reader with a fuller, balanced appreciation of the subject matter, a critical analysis of the benefits brought about by that innovation should be provided also. This short paper addresses that need by revisiting the array of issues addressed in the cited work, in the light of the latest advances to the relevant state of the art. Accordingly, we show that the potential benefits of randomized caches do offset their limitations, causing them to be - when used in conjunction with PTA - a serious competitor to conventional designs.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2015-06-01 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v002-i001-a001
Leibniz Transactions on Embedded Systems; Vol. 2 No. 1 (2015)
eng
Copyright (c) 2015 Enrico Mezzetti, Marco Ziccardi, Tullio Vardanega, Jaume Abella, Eduardo Qui\~{n}ones, Francisco J. Cazorla
oai:ojs.dagstuhl.de:article/53
2018-01-08T10:43:59Z
lites:LITES-SCOPES
driver
nmb a2200000Iu 4500
"150602 2015 eng "
2199-2002
10.4230/LITES-v002-i001-a002
doi
dc
More General Optimal Offset Assignment
Mallach, Sven
Universität zu Köln
Albertus-Magnus-Platz, 50923 Köln, Germany
Array
This manuscript presents exact approaches to the general offset assignment problem arising in the address code generation phase of compilers for application-specific processors. First, integer programming models for architecture-dependent and theoretically motivated special cases of the problem are established. Then, these models are extended to provide the first widely applicable formulations for the most general problem setting, supporting processors with several address registers and complex addressing capabilities. Existing heuristics are similarly extended and practical applicability of the proposed methods is demonstrated by experimental evaluation using an established and large benchmark set. The experiments allow us to study the impact of exploiting more complex memory addressing capabilities on the address computation costs of real-world programs. We also show how to integrate operand reordering techniques for commutative instructions into existing solution approaches.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2015-06-01 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v002-i001-a002
Leibniz Transactions on Embedded Systems; Vol. 2 No. 1 (2015)
eng
Copyright (c) 2015 Sven Mallach
oai:ojs.dagstuhl.de:article/60
2016-06-29T13:57:54Z
lites:ART
driver
nmb a2200000Iu 4500
"160629 2016 eng "
2199-2002
10.4230/LITES-v003-i001-a005
doi
dc
A Survey on Static Cache Analysis for Real-Time Systems
Lv, Mingsong
Northeastern University, China
Guan, Nan
Northeastern University, China
Reineke, Jan
Saarland University http://orcid.org/0000-0002-3459-2214
Wilhelm, Reinhard
Saarland University http://orcid.org/0000-0002-5599-7560
Yi, Wang
Uppsala University
Array
Real-time systems are reactive computer systems that must produce their reaction to a stimulus within given time bounds. A vital verification requirement is to estimate the Worst-Case Execution Time (WCET) of programs. These estimates are then used to predict the timing behavior of the overall system. The execution time of a program heavily depends on the underlying hardware, among which cache has the biggest influence. Analyzing cache behavior is very challenging due to the versatile cache features and complex execution environment. This article provides a survey on static cache analysis for real-time systems. We first present the challenges and static analysis techniques for independent programs with respect to different cache features. Then, the discussion is extended to cache analysis in complex execution environment, followed by a survey of existing tools based on static techniques for cache analysis. An outlook for future research is provided at last.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2016-06-10 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v003-i001-a005
Leibniz Transactions on Embedded Systems; Vol. 3 No. 1 (2016)
eng
Copyright (c) 2016 Mingsong Lv, Nan Guan, Jan Reineke, Reinhard Wilhelm, and Wang Yi
oai:ojs.dagstuhl.de:article/61
2016-06-29T13:57:54Z
lites:ART
driver
nmb a2200000Iu 4500
"160610 2016 eng "
2199-2002
10.4230/LITES-v003-i001-a001
doi
dc
Programming Language Constructs Supporting Fault Tolerance
Houben, Christina
Rheinische Friedrich-Wilhelms-Universität
Chemical Institutes, Bonn
Houben, Sebastian
Ruhr-Universität Bochum
Institute for Neural Computation, Bochum http://orcid.org/0000-0002-2036-419X
Array
In order to render software viable for highly safety-critical applications, we describe how to incorporate fault tolerance mechanisms into the real-time programming language PEARL. Therefore, we present, classify, evaluate and illustrate known fault tolerance methods for software. We link them together with the requirements of the international standard IEC 61508-3 for functional safety. We contribute PEARL-2020 programming language constructs for fault tolerance methods that need to be implemented by operating systems, and code-snippets as well as libraries for those independent from runtime systems.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2016-06-10 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v003-i001-a001
Leibniz Transactions on Embedded Systems; Vol. 3 No. 1 (2016)
eng
Copyright (c) 2016 Christina Houben and Sebastian Houben
oai:ojs.dagstuhl.de:article/62
2016-06-29T13:57:54Z
lites:ART
driver
nmb a2200000Iu 4500
"160629 2016 eng "
2199-2002
10.4230/LITES-v003-i001-a004
doi
dc
Optimal Scheduling of Periodic Gang Tasks
Goossens, Joël
Université Libre de Bruxelles (ULB)
50 av. F.D. Roosevelt 1050 Brussels, Belgium http://parts.ulb.ac.be/jgoossens
Richard, Pascal
LIAS/Isae-Ensma-Université de Poitiers
1 av. Clément Ader, BP 40109, 86961 Chasseneuil du Poitou, France
Array
The gang scheduling of parallel implicit-deadline periodic task systems upon identical multiprocessor platforms is considered. In this scheduling problem, parallel tasks use several processors simultaneously. We propose two DPFAIR (deadline partitioning) algorithms that schedule all jobs in every interval of time delimited by two subsequent deadlines. These algorithms define a static schedule pattern that is stretched at run-time in every interval of the DPFAIR schedule. The first algorithm is based on linear programming and is the first one to be proved optimal for the considered gang scheduling problem. Furthermore, it runs in polynomial time for a fixed number m of processors and an efficient implementation is fully detailed. The second algorithm is an approximation algorithm based on a fixed-priority rule that is competitive under resource augmentation analysis in order to compute an optimal schedule pattern. Precisely, its speedup factor is bounded by (2-1/m). Both algorithms are also evaluated through intensive numerical experiments.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2016-06-10 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v003-i001-a004
Leibniz Transactions on Embedded Systems; Vol. 3 No. 1 (2016)
eng
Copyright (c) 2016 Joël Goossens and Pascal Richard
oai:ojs.dagstuhl.de:article/63
2016-06-29T13:57:54Z
lites:ART
driver
nmb a2200000Iu 4500
"160629 2016 eng "
2199-2002
10.4230/LITES-v003-i001-a003
doi
dc
Modeling Power Consumption and Temperature in TLM Models
Moy, Matthieu
Univ. Grenoble Alpes, VERIMAG, F-38000 Grenoble, France
CNRS, VERIMAG, F-38000 Grenoble, France http://www-verimag.imag.fr/~moy/ http://orcid.org/0000-0002-6054-8882
Helmstetter, Claude
Univ. Grenoble Alpes, VERIMAG, F-38000 Grenoble, France
CNRS, VERIMAG, F-38000 Grenoble, France http://orcid.org/0000-0002-2323-6919
Bouhadiba, Tayeb
Univ. Grenoble Alpes, VERIMAG, F-38000 Grenoble, France
CNRS, VERIMAG, F-38000 Grenoble, France http://orcid.org/0000-0003-1694-6709
Maraninchi, Florence
Univ. Grenoble Alpes, VERIMAG, F-38000 Grenoble, France
CNRS, VERIMAG, F-38000 Grenoble, France http://orcid.org/0000-0003-0783-9178
Array
Many techniques and tools exist to estimate the power consumption and the temperature map of a chip. These tools help the hardware designers develop power efficient chips in the presence of temperature constraints. For this task, the application can be ignored or at least abstracted by some high level scenarios; at this stage, the actual embedded software is generally not available yet.
However, after the hardware is defined, the embedded software can still have a significant influence on the power consumption; i.e., two implementations of the same application can consume more or less power. Moreover, the actual software power manager ensuring the temperature constraints, usually by acting dynamically on the voltage and frequency, must itself be validated. Validating such power management policy requires a model of both actuators and sensors, hence a closed-loop simulation of the functional model with a non-functional one.
In this paper, we present and compare several tools to simulate the power and thermal behavior of a chip together with its functionality. We explore several levels of abstraction and study the impact on the precision of the analysis.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2016-06-10 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v003-i001-a003
Leibniz Transactions on Embedded Systems; Vol. 3 No. 1 (2016)
eng
Copyright (c) 2016 Matthieu Moy, Claude Helmstetter, Tayeb Bouhadiba, and Florence Maraninchi
oai:ojs.dagstuhl.de:article/64
2018-11-19T15:56:24Z
lites:ART
driver
nmb a2200000Iu 4500
"180530 2018 eng "
2199-2002
10.4230/LITES-v005-i001-a002
doi
dc
Errata for Three Papers (2004-05) on Fixed-Priority Scheduling with Self-Suspensions
Bletsas, Konstantinos
CISTER/INESC-TEC, ISEP, Polytechnic Institute of Porto http://orcid.org/0000-0002-3640-0239
Audsley, Neil C.
University of York http://orcid.org/0000-0003-3739-6590
Huang, Wen-Hung
TU Dortmund http://orcid.org/0000-0001-9446-4719
Chen, Jian-Jia
TU Dortmund http://orcid.org/0000-0001-8114-9760
Nelissen, Geoffrey
CISTER/INESC-TEC, ISEP, Polytechnic Institute of Porto http://orcid.org/0000-0003-4141-6718
Array
The purpose of this article is to (i) highlight the flaws in three previously published works [Audsley, 2004a; Audsley, 2004b; Bletsas, 2005] on the worst-case response time analysis for tasks with self-suspensions and (ii) provide straightforward fixes for those flaws, hence rendering the analysis safe.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2018-05-30 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v005-i001-a002
Leibniz Transactions on Embedded Systems; Vol. 5 No. 1 (2018)
eng
Copyright (c) 2018 Konstantinos Bletsas, Neil C. Audsley, Wen-Hung Huang, Jian-Jia Chen, Geoffrey Nelissen
oai:ojs.dagstuhl.de:article/65
2016-06-29T13:57:54Z
lites:ART
driver
nmb a2200000Iu 4500
"160610 2016 eng "
2199-2002
10.4230/LITES-v003-i001-a002
doi
dc
Real-Time Scheduling on Uni- and Multiprocessors based on Priority Promotions
Pathan, Risat Mahmud
Chalmers University of Technology
412 96, Göteborg http://www.cse.chalmers.se/~risat/ http://orcid.org/0000-0002-9902-7558
Array
This paper addresses the problem of real-time scheduling of a set of sporadic tasks on uni- and multiprocessor platform based on priority promotion. A new preemptive scheduling algorithm, called Fixed-Priority with Priority Promotion (FPP), is proposed. In FPP scheduling, tasks are executed similar to traditional fixed-priority (FP) scheduling but the priority of some tasks are promoted at fixed time interval (called, promotion point) relative to the release time of each job. A policy called Increase Priority at Deadline Difference (IPDD) to compute the promotion points and promoted priorities for each task is proposed. FPP scheduling prioritizes jobs according to Earliest-Deadline-First (EDF) priority when all tasks' priorities follow IPDD policy.
It is known that managing (i.e., inserting and removing) jobs in the ready queue of traditional EDF scheduler is more complex than that of FP scheduler. To avoid such problem in FPP scheduling, a simple data structure and efficient operations to manage jobs in the ready queue are proposed. In addition, techniques for implementing priority promotions with and without the use of a hardware timer are proposed.
Finally, an effective scheme to reduce the average number of priority promotions is proposed: if a task set is not schedulable using traditional FP scheduling, then promotion points are assigned only to those tasks that need them to meet the deadlines; otherwise, tasks are assigned traditional fixed priorities without any priority promotion. Empirical investigation shows the effectiveness of the proposed scheme in reducing overhead on uniprocessor and in accepting larger number of task sets in comparison to that of using state-of-the-art global schedulability tests for multiprocessors.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2016-06-10 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v003-i001-a002
Leibniz Transactions on Embedded Systems; Vol. 3 No. 1 (2016)
eng
Copyright (c) 2016 Risat Mahmud Pathan
oai:ojs.dagstuhl.de:article/68
2017-02-28T07:13:57Z
lites:ART
driver
nmb a2200000Iu 4500
"170228 2017 eng "
2199-2002
10.4230/LITES-v004-i001-a001
doi
dc
A Note on the Period Enforcer Algorithm for Self-Suspending Tasks
Chen, Jian-Jia
TU Dortmund University
Dortmund, Germany
Brandenburg, Björn B.
Max Planck Institute for Software Systems (MPI-SWS)
Kaiserslautern, Germany http://www.mpi-sws.org/~bbb http://orcid.org/0000-0001-8254-3815
Array
The period enforcer algorithm for self-suspending real-time tasks is a technique for suppressing the "back-to-back" scheduling penalty associated with deferred execution. Originally proposed in 1991, the algorithm has attracted renewed interest in recent years. This note revisits the algorithm in the light of recent developments in the analysis of self-suspending tasks, carefully re-examines and explains its underlying assumptions and limitations, and points out three observations that have not been made in the literature to date: (i) period enforcement is not strictly superior (compared to the base case without enforcement) as it can cause deadline misses in self-suspending task sets that are schedulable without enforcement; (ii) to match the assumptions underlying the analysis of the period enforcer, a schedulability analysis of self-suspending tasks subject to period enforcement requires a task set transformation for which no solution is known in the general case, and which is subject to exponential time complexity (with current techniques) in the limited case of a single self-suspending task; and (iii) the period enforcer algorithm is incompatible with all existing analyses of suspension-based locking protocols, and can in fact cause ever-increasing suspension times until a deadline is missed.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2017-02-28 08:09:27
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v004-i001-a001
Leibniz Transactions on Embedded Systems; Vol. 4 No. 1 (2017)
eng
Copyright (c) 2016 Jian-Jia Chen and Björn B. Brandenburg
oai:ojs.dagstuhl.de:article/69
2017-02-28T07:13:57Z
lites:LITES-QEST
driver
nmb a2200000Iu 4500
"170228 2017 eng "
2199-2002
10.4230/LITES-v004-i001-a003
doi
dc
Quantitative Analysis of Consistency in NoSQL Key-Value Stores
Liu, Si
Department of Computer Science
University of Illinois at Urbana-Champaign, IL, USA
Ganhotra, Jatin
Department of Computer Science
University of Illinois at Urbana-Champaign, IL, USA
Rahman, Muntasir Raihan
Microsoft, Redmond, WA, USA
Nguyen, Son
Addepar Inc., Sunnyvale, CA, USA
Gupta, Indranil
Department of Computer Science
University of Illinois at Urbana-Champaign, IL, USA
Meseguer, José
Department of Computer Science
University of Illinois at Urbana-Champaign, IL, USA
Array
The promise of high scalability and availability has prompted many companies to replace traditional relational database management systems (RDBMS) with NoSQL key-value stores. This comes at the cost of relaxed consistency guarantees: key-value stores only guarantee eventual consistency in principle. In practice, however, many key-value stores seem to offer stronger consistency. Quantifying how well consistency properties are met is a non-trivial problem. We address this problem by formally modeling key-value stores as probabilistic systems and quantitatively analyzing their consistency properties by both statistical model checking and implementation evaluation. We present for the first time a formal probabilistic model of Apache Cassandra, a popular NoSQL key-value store, and quantify how much Cassandra achieves various consistency guarantees under various conditions. To validate our model, we evaluate multiple consistency properties using two methods and compare them against each other. The two methods are: (1) an implementation-based evaluation of the source code; and (2) a statistical model checking analysis of our probabilistic model.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2017-02-28 08:09:27
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v004-i001-a003
Leibniz Transactions on Embedded Systems; Vol. 4 No. 1 (2017)
eng
Copyright (c) 2016 Si Liu, Jatin Ganhotra, Muntasir Raihan Rahman, Son Nguyen, Indranil Gupta, José Meseguer
oai:ojs.dagstuhl.de:article/70
2017-02-28T07:13:57Z
lites:LITES-QEST
driver
nmb a2200000Iu 4500
"170228 2017 eng "
2199-2002
10.4230/LITES-v004-i001-a004
doi
dc
How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty
Hermanns, Holger
Saarland University, Saarland Informatics Campus, Saarbrücken http://orcid.org/0000-0002-2766-9615
Krčál, Jan
Saarland University, Saarland Informatics Campus, Saarbrücken http://orcid.org/0000-0002-3799-039X
Nies, Gilles
Saarland University, Saarland Informatics Campus, Saarbrücken http://orcid.org/0000-0002-2535-1590
Array
The kinetic battery model is a popular model of the dynamic behaviour of a conventional battery, useful to predict or optimize the time until battery depletion. The model however lacks certain obvious aspects of batteries in-the-wild, especially with respect to the effects of random influences and the behaviour when charging up to capacity limits.
This paper considers the kinetic battery model with limited capacity in the context of piecewise constant yet random charging and discharging. We provide exact representations of the battery behaviour wherever possible, and otherwise develop safe approximations that bound the probability distribution of the battery state from above and below. The resulting model enables the time-dependent evaluation of the risk of battery depletion. This is demonstrated in an extensive dependability study of a nano satellite currently orbiting the earth.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2017-02-28 08:09:27
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v004-i001-a004
Leibniz Transactions on Embedded Systems; Vol. 4 No. 1 (2017)
eng
Copyright (c) 2016 Holger Hermanns, Jan Krčál, Gilles Nies
oai:ojs.dagstuhl.de:article/74
2017-02-28T07:13:57Z
lites:LITES-QEST
driver
nmb a2200000Iu 4500
"170228 2017 eng "
2199-2002
10.4230/LITES-v004-i001-a005
doi
dc
Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains
Rozier, Eric W. D.
Department of Computer Science, Iowa State University, Ames, IA, USA http://dataengineering.org
Rozier, Kristin Y.
Department of Aerospace Engineering, Iowa State University, Ames, IA, USA
Bayram, Ulya
Department of Electrical Engineering and Computing Systems, University of Cincinnati, Cincinnati, OH, USA http://orcid.org/0000-0002-8150-4053
Array
As data centers attempt to cope with the exponential growth of data, new techniques for intelligent, software-defined data centers (SDDC) are being developed to confront the scale and pace of changing resources and requirements. For cost-constrained environments, like those increasingly present in scientific research labs, SDDCs also may provide better reliability and performability with no additional hardware through the use of dynamic syndrome allocation. To do so, the middleware layers of SDDCs must be able to calculate and account for complex dependence relationships to determine an optimal data layout. This challenge is exacerbated by the growth of constraints on the dependence problem when available resources are both large (due to a higher number of syndromes that can be stored) and small (due to the lack of available space for syndrome allocation). We present a quantitative method for characterizing these challenges using an analysis of attack domains for high-dimension variants of the $n$-queens problem that enables performable solutions via the SMT solver Z3. We demonstrate correctness of our technique, and provide experimental evidence of its efficacy; our implementation is publicly available.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2017-02-28 08:09:27
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v004-i001-a005
Leibniz Transactions on Embedded Systems; Vol. 4 No. 1 (2017)
eng
Copyright (c) 2017 Eric W. D. Rozier, Kristin Y. Rozier, and Ulya Bayram
oai:ojs.dagstuhl.de:article/76
2017-02-28T07:13:57Z
lites:ART
driver
nmb a2200000Iu 4500
"170228 2017 eng "
2199-2002
10.4230/LITES-v004-i001-a002
doi
dc
Utility-Based Scheduling of (m,k)-firm Real-Time Tasks - New Empirical Results
Kluge, Florian
Department of Computer Science
University of Augsburg
Array
The concept of a firm real-time task implies the notion of a firm deadline that should not be missed by the jobs of this task. If a deadline miss occurs, the concerned job yields no value to the system. For some applications domains, this restrictive notion can be relaxed. For example, robust control systems can tolerate that single executions of a control loop miss their deadlines, and still yield an acceptable behaviour. Thus, systems can be developed under more optimistic assumptions, e.g. by allowing overloads. However, care must be taken that deadline misses do not accumulate. This restriction can be expressed by the model of (m,k)-firm real-time tasks that require that from any k consecutive jobs at least m are executed successfully. In this article, we extend our prior work on the MKU scheduling heuristic. MKU uses history-cognisant utility functions as means for making decisions in overload situations. We present new theoretical results on MKU and on other schedulers for (m,k)-firm real-time tasks. Based on extensive simulations, we assess the performance of these
schedulers. The results allow us to identify task set characteristics that can be used as guidelines for choosing a scheduler for a concrete use case.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2017-02-28 08:09:27
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v004-i001-a002
Leibniz Transactions on Embedded Systems; Vol. 4 No. 1 (2017)
eng
Copyright (c) 2016 Florian Kluge
oai:ojs.dagstuhl.de:article/78
2018-11-19T15:56:24Z
lites:ART
driver
nmb a2200000Iu 4500
"180530 2018 eng "
2199-2002
10.4230/LITES-v005-i001-a001
doi
dc
Risk-Aware Scheduling of Dual Criticality Job Systems Using Demand Distributions
Alahmad, Bader Naim
The University of British Columbia
2366 Main Mall, Vancouver, BC, Canada V6T 1Z4 http://blogs.ubc.ca/bader http://orcid.org/0000-0002-6409-1277
Gopalakrishnan, Sathish
The University of British Columbia
2332 Main Mall, Vancouver, BC, Canada V6T 1Z4 https://www.ece.ubc.ca/faculty/sathish-gopalakrishnan
Array
We pose the problem of scheduling Mixed Criticality (MC) job systems when there are only two criticality levels, Lo and Hi -referred to as Dual Criticality job systems- on a single processing platform, when job demands are probabilistic and their distributions are known. The current MC models require that the scheduling policy allocate as little execution time as possible to Lo-criticality jobs if the scenario of execution is of Hi criticality, and drop Lo-criticality jobs entirely as soon as the execution scenario's criticality level can be inferred and is Hi. The work incurred by "incorrectly" scheduling Lo-criticality jobs in cases of Hi realized scenarios might affect the feasibility of Hi criticality jobs; we quantify this work and call it Work Threatening Feasibility (WTF). Our objective is to construct online scheduling policies that minimize the expected WTF for the given instance, and under which the instance is feasible in a probabilistic sense that is consistent with the traditional deterministic definition of MC feasibility.
We develop a probabilistic framework for MC scheduling, where feasibility is defined in terms of (chance) constraints on the probabilities that Lo and Hi jobs meet their deadlines. The probabilities are computed over the set of sample paths, or trajectories, induced by executing the policy, and those paths are dependent upon the set of execution scenarios and the given demand distributions. Our goal is to exploit the information provided by job distributions to compute the minimum expected WTF below which the given instance is not feasible in probability, and to compute a (randomized) "efficiently implementable" scheduling policy that realizes the latter quantity. We model the problem as a Constrained Markov Decision Process (CMDP) over a suitable state space and a finite planning horizon, and show that an optimal (non-stationary) Markov randomized scheduling policy exists. We derive an optimal policy by solving a Linear Program (LP). We also carry out quantitative evaluations on select probabilistic MC instances to demonstrate that our approach potentially outperforms current MC scheduling policies.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2018-05-30 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v005-i001-a001
Leibniz Transactions on Embedded Systems; Vol. 5 No. 1 (2018)
eng
Copyright (c) 2018 Bader Naim Alahmad and Sathish Gopalakrishnan
oai:ojs.dagstuhl.de:article/79
2018-01-08T10:46:08Z
lites:ART
driver
nmb a2200000Iu 4500
"170707 2017 eng "
2199-2002
10.4230/LITES-v004-i002-a001
doi
dc
Dynamic and Static Task Allocation for Hard Real-Time Video Stream Decoding on NoCs
Mendis, Hashan R.
University of York
Audsley, Neil C.
University of York
Indrusiak, Leandro Soares
University of York http://orcid.org/0000-0002-9938-2920
Array
Hard real-time (HRT) video systems require admission control decisions that rely on two factors. Firstly, schedulability analysis of the data-dependent, communicating tasks within the application need to be carried out in order to guarantee timing and predictability. Secondly, the allocation of the tasks to multi-core processing elements would generate different results in the schedulability analysis. Due to the conservative nature of the state-of-the-art schedulability analysis of tasks and message flows, and the unpredictability in the application, the system resources are often under-utilised. In this paper we propose two blocking-aware dynamic task allocation techniques that exploit application and platform characteristics, in order to increase the number of simultaneous, fully schedulable, video streams handled by the system. A novel, worst-case response time aware, search-based, static hard real-time task mapper is introduced to act as an upper-baseline to the proposed techniques. Further evaluations are carried out against existing heuristic-based dynamic mappers. Improvements to the admission rates and the system utilisation under a range of different workloads and platform sizes are explored.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2017-07-07 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v004-i002-a001
Leibniz Transactions on Embedded Systems; Vol. 4 No. 2 (2017)
eng
Copyright (c) 2017 Hashan R. Mendis, Neil C. Audsley, and Leandro Soares Indrusiak
oai:ojs.dagstuhl.de:article/81
2018-01-08T10:46:08Z
lites:ART
driver
nmb a2200000Iu 4500
"170707 2017 eng "
2199-2002
10.4230/LITES-v004-i002-a002
doi
dc
EMSBench: Benchmark and Testbed for Reactive Real-Time Systems
Kluge, Florian
University of Augsburg
Rochange, Christine
IRIT, Université de Toulouse, CNRS http://orcid.org/0000-0001-7257-7114
Ungerer, Theo
University of Augsburg
Array
Benchmark suites for real-time embedded systems (RTES) usually contain only pure computations that are often used in this domain. They allow to evaluate computing performance, but do not reproduce the complexity and behaviour that is typical for such systems. Actual RTES have to interact with the physical environment, which is often reflected by code that is executed concurrently. In this article, we present the software package EMSBench that mimics such complex behaviour, and highlight some of its use cases. The benchmark code ems of EMSBench is based on the open-source engine management system (EMS) FreeEMS. Additionally, EMSBench contains a trace generator (tg) that provides input signals for ems and enables to execute ems close to reality. We provide detailed descriptions of the ems's execution behaviour and of trace generation. EMSBench can be used as test or benchmark program to compare different hardware platforms, e.g. in terms of schedulability. Also, we use EMSBench as a benchmark for static worst-case execution time (WCET) analysis and compare these results to measurements performed on existing hardware. Our results based on the OTAWA WCET estimation tool show WCET overestimations by the static analysis from 11.9% to 41.1% depending on the complexity of the analysed functions.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2017-07-07 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v004-i002-a002
Leibniz Transactions on Embedded Systems; Vol. 4 No. 2 (2017)
eng
Copyright (c) 2017 Florian Kluge, Christine Rochange, and Theo Ungerer
oai:ojs.dagstuhl.de:article/85
2018-11-19T15:56:24Z
lites:ART
driver
nmb a2200000Iu 4500
"181015 2018 eng "
2199-2002
10.4230/LITES-v005-i001-a004
doi
dc
A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits
Burlyaev, Dmitry
Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble https://team.inria.fr/spades/dmitry-burlyaev/ https://orcid.org/0000-0001-8685-6923
Fradet, Pascal
Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble, France https://orcid.org/0000-0003-4961-9923
Girault, Alain
Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble, France https://orcid.org/0000-0001-7500-1655
Array
We present a formal approach to minimize the number of voters in triple-modular redundant (TMR) sequential circuits. Our technique actually works on a single copy of the TMR circuit and considers a large class of fault mo dels of the form “at most 1 Single-Event Upset (SEU) or Single-Event Transient (SET) every k clock cycles”. Verification-based voter minimization guarantees that the resulting TMR circuit (i) is fault tolerant to the soft-errors defined by the fault model and (ii) is functionally equivalent to the initial TMR circuit. Our approach operates at the logic level and takes into account the input and output interface specifications of the circuit. Its implementation makes use of graph traversal algorithms, fixed-point iterations, and binary decision diagrams (BDD). Experimental results on the ITC’99 benchmark suite indicate that our method significantly decreases the number of inserted voters, yielding a hardware reduction of up to 55% and a clock frequency increase of up to 35% compared to full TMR. As our experiments show, if the SEU fault-model is replaced with the stricter fault-model of SET, it has a minor impact on the number of removed voters. On the other hand, BDD-based modelling of SET effects represents a more complex task than the modelling of an SEU as a bit-flip. We propose solutions for this task and explain the nature of encountered problems. We address scalability issues arising from formal verification with approximations and assess their efficiency and precision.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2018-05-30 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v005-i001-a004
Leibniz Transactions on Embedded Systems; Vol. 5 No. 1 (2018)
eng
Copyright (c) 2018 Dmitry Burlyaev, Pascal Fradet, and Alain Girault
oai:ojs.dagstuhl.de:article/88
2018-01-08T10:46:08Z
lites:ART
driver
nmb a2200000Iu 4500
"180108 2018 eng "
2199-2002
10.4230/LITES-v004-i002-a003
doi
dc
Per Processor Spin-Based Protocols for Multiprocessor Real-Time Systems
Afshar, Sara
Mälardalen University
Behnam, Moris
Mälardalen University
Bril, Reinder J.
Technische Universiteit Eindhoven
Nolte, Thomas
Mälardalen University
Array
This paper investigates preemptive spin-based global resource sharing protocols for resource-constrained real-time embedded multi-core systems based on partitioned fixed-priority preemptive scheduling. We present preemptive spin-based protocols that feature (i) an increased schedulability ratio of task sets and reduced response jitter of tasks compared to the classical non-preemptive spin-based protocol, (ii) similar memory requirements for the administration of waiting tasks as for the non-preemptive protocol whilst only causing (iii) a minimal increase of the minimal number of required stacks per core from one to at most two, and (iv) strong progress guarantees to tasks. We complement these protocols with a unified worst-case response time analysis that specializes to the classical analysis for the non-preemptive protocol. The paper includes a comparative evaluation of the preemptive protocols and the non-preemptive protocol based on synthetic data.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2017-07-07 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v004-i002-a003
Leibniz Transactions on Embedded Systems; Vol. 4 No. 2 (2017)
eng
Copyright (c) 2017 Sara Afshar, Moris Behnam, Reinder J. Bril, and Thomas Nolte
oai:ojs.dagstuhl.de:article/96
2021-07-16T13:55:00Z
lites:ART
driver
nmb a2200000Iu 4500
"190218 2019 eng "
2199-2002
10.4230/LITES-v006-i001-a001
doi
dc
Local Planning Semantics: A Semantics for Distributed Real-Time Systems
Dellabani, Mahieddine
University Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, 38000 Grenoble, France https://orcid.org/0000-0002-7437-2822
Combaz, Jacques
University Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, 38000 Grenoble, France https://orcid.org/0000-0002-3968-3879
Bensalem, Saddek
University Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, 38000 Grenoble, France https://orcid.org/0000-0002-5753-2126
Bozga, Marius
University Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, 38000 Grenoble, France https://orcid.org/0000-0003-4412-5684
Array
Design, implementation and verification of distributed real-time systems are acknowledged to be very hard tasks. Such systems are prone to different kinds of delay, such as execution time of actions or communication delays implied by distributed platforms. The latter increase considerably the complexity of coordinating the parallel activities of running components. Scheduling such systems must cope with those delays by proposing execution strategies ensuring global consistency while satisfying the imposed timing constraints. In this paper, we investigate a formal model for such systems as compositions of timed automata subject to multiparty interactions, and propose a semantics aiming to overcome the communication delays problem through anticipating the execution of interactions. To be effective in a distributed context, scheduling an interaction should rely on (as much as possible) local information only, namely the state of its participating components. However, as shown in this paper these information is not always sufficient and does not guarantee a safe execution of the system as it may introduce deadlocks. Moreover, delays may also affect the satisfaction of timing constraints, which also corresponds to deadlocks in the former model. Thus, we also explore methods for analyzing such deadlock situations and for computing deadlock-free scheduling strategies when possible.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2019-05-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v006-i001-a001
Leibniz Transactions on Embedded Systems; Vol. 6 No. 1 (2019)
eng
Copyright (c) 2019 Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga
oai:ojs.dagstuhl.de:article/97
2018-11-19T15:56:24Z
lites:ART
driver
nmb a2200000Iu 4500
"180802 2018 eng "
2199-2002
10.4230/LITES-v005-i001-a003
doi
dc
The Semantic Foundations and a Landscape of Cache-Persistence Analyses
Reineke, Jan
Saarland University
Saarland Informatics Campus Saarbrücken http://orcid.org/0000-0002-3459-2214
Array
We clarify the notion of cache persistence and contribute to the understanding of persistence analysis for caches with least-recently-used replacement.
To this end, we provide the first formal definition of persistence as a property of a trace semantics. Based on this trace semantics we introduce a semantics-based, i.e., abstract-interpretation-based persistence analysis framework.
We identify four basic persistence analyses and prove their correctness as instances of this analysis framework.
Combining these basic persistence analyses via two generic cooperation mechanisms yields a lattice of ten persistence analyses.
Notably, this lattice contains all persistence analyses previously described in the literature. As a consequence, we obtain uniform correctness proofs for all prior analyses and a precise understanding of how and why these analyses work, as well as how they relate to each other in terms of precision.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2018-05-30 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v005-i001-a003
Leibniz Transactions on Embedded Systems; Vol. 5 No. 1 (2018)
eng
Copyright (c) 2018 Jan Reineke
oai:ojs.dagstuhl.de:article/98
2021-07-16T08:51:20Z
lites:ART
driver
nmb a2200000Iu 4500
"190218 2019 eng "
2199-2002
10.4230/LITES-v006-i001-a002
doi
dc
Improving WCET Evaluation using Linear Relation Analysis
Raymond, Pascal
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, Grenoble, France http://www-verimag.imag.fr/~raymond/ https://orcid.org/0000-0003-3876-9125
Maiza, Claire
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, Grenoble, France https://orcid.org/0000-0002-5977-6685
Parent-Vigouroux, Catherine
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, Grenoble, France https://orcid.org/0000-0003-0594-8274
Jahier, Erwan
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, Grenoble, France https://orcid.org/0000-0002-3042-1565
Halbwachs, Nicolas
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, Grenoble, France https://orcid.org/0000-0002-1426-7967
Carrier, Fabienne
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, Grenoble, France
Asavoae, Mihail
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, Grenoble, France
Boutonnet, Rémy
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes),
VERIMAG, Grenoble, France https://orcid.org/0000-0003-4761-5566
Array
The precision of a worst case execution time (WCET) evaluation tool on a given program is highly dependent on how the tool is able to detect and discard semantically infeasible executions of the program. In this paper, we propose to use the classical abstract interpretation-based method of linear relation analysis to discover and exploit relations between execution paths. For this purpose, we add auxiliary variables (counters) to the program to trace its execution paths. The results are easily incorporated in the classical workflow of a WCET evaluator, when the evaluator is based on the popular implicit path enumeration technique. We use existing tools - a WCET evaluator and a linear relation analyzer - to build and experiment a prototype implementation of this idea.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2019-05-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v006-i001-a002
Leibniz Transactions on Embedded Systems; Vol. 6 No. 1 (2019)
eng
Copyright (c) 2018 Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet
oai:ojs.dagstuhl.de:article/99
2021-07-16T08:51:20Z
lites:ART
driver
nmb a2200000Iu 4500
"190514 2019 eng "
2199-2002
10.4230/LITES-v006-i001-a003
doi
dc
A Survey of Probabilistic Timing Analysis Techniques for Real-Time Systems
Davis, Robert I.
University of York, UK and Inria, France http://www-users.cs.york.ac.uk/~robdavis/ http://orcid.org/0000-0002-5772-0928
Cucu-Grosjean, Liliana
Inria, France https://who.rocq.inria.fr/Liliana.Cucu/Welcome.html
Array
This survey covers probabilistic timing analysis techniques for real-time systems. It reviews and critiques the key results in the field from its origins in 2000 to the latest research published up to the end of August 2018. The survey provides a taxonomy of the different methods used, and a classification of existing research. A detailed review is provided covering the main subject areas: static probabilistic timing analysis, measurement-based probabilistic timing analysis, and hybrid methods. In addition, research on supporting mechanisms and techniques, case studies, and evaluations is also reviewed. The survey concludes by identifying open issues, key challenges and possible directions for future research.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2019-05-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v006-i001-a003
Leibniz Transactions on Embedded Systems; Vol. 6 No. 1 (2019)
eng
Copyright (c) 2019 Robert I. Davis and Liliana Cucu-Grosjean
oai:ojs.dagstuhl.de:article/100
2021-07-16T08:51:20Z
lites:ART
driver
nmb a2200000Iu 4500
"190514 2019 eng "
2199-2002
10.4230/LITES-v006-i001-a004
doi
dc
A Survey of Probabilistic Schedulability Analysis Techniques for Real-Time Systems
Davis, Robert I.
University of York, UK; Inria, France http://www-users.cs.york.ac.uk/~robdavis/ http://orcid.org/0000-0002-5772-0928
Cucu-Grosjean, Liliana
Inria, France https://who.rocq.inria.fr/Liliana.Cucu/Welcome.html
Array
This survey covers schedulability analysis techniques for probabilistic real-time systems. It reviews the key results in the field from its origins in the late 1980s to the latest research published up to the end of August 2018. The survey outlines
fundamental concepts and highlights key issues. It provides a taxonomy of the different methods used, and a classification of existing research. A detailed review is provided covering the main subject areas as well as research on supporting techniques. The survey concludes by identifying open issues, key challenges and possible directions for future research.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2019-05-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v006-i001-a004
Leibniz Transactions on Embedded Systems; Vol. 6 No. 1 (2019)
eng
Copyright (c) 2019 Robert I. Davis and Liliana Cucu-Grosjean
oai:ojs.dagstuhl.de:article/102
2021-07-16T08:51:20Z
lites:ART
driver
nmb a2200000Iu 4500
"190514 2019 eng "
2199-2002
10.4230/LITES-v006-i001-a005
doi
dc
Elastic Scheduling for Parallel Real-Time Systems
Orr, James
{Washington University in St. Louis, 1 Brookings Dr, St. Louis, MO 63130, USA https://orcid.org/0000-0002-2835-2417
Gill, Chris
Washington University in St. Louis, 1 Brookings Dr, St. Louis, MO 63130, USA https://orcid.org/0000-0003-0366-8586
Agrawal, Kunal
Washington University in St. Louis, 1 Brookings Dr, St. Louis, MO 63130, USA https://orcid.org/0000-0001-5882-6647
Li, Jing
New Jersey Institute of Technology, University Heights, Newark, NJ 07102, USA https://orcid.org/0000-0002-6865-7290
Baruah, Sanjoy
Washington University in St. Louis, 1 Brookings Dr, St. Louis, MO 63130, USA https://orcid.org/0000-0002-4541-3445
Array
The elastic task model was introduced by Buttazzo et al.~in order to represent recurrent real-time workloads executing upon uniprocessor platforms that are somewhat flexible with regards to timing constraints. In this work, we propose an extension of this model and apply it to represent recurrent real-time workloads that exhibit internal parallelism and are executed on multiprocessor platforms. In our proposed extension, the elasticity coefficient - the quantitative measure of a task's elasticity that was introduced in the model proposed by Buttazzo et al. - is interpreted in the same manner as in the original (sequential) model. Hence, system developers who are familiar with the elastic task model in the uniprocessor context may use our more general model as they had previously done, now for real-time tasks whose computational demands require them to utilize more than one processor.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2019-05-14 00:00:00
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v006-i001-a005
Leibniz Transactions on Embedded Systems; Vol. 6 No. 1 (2019)
eng
Copyright (c) 2019 James Orr, Chris Gill, Kunal Agrawal, Jing Li, and Sanjoy Baruah
oai:ojs.dagstuhl.de:article/105
2021-08-12T07:00:26Z
lites:LITES-SECURITY
driver
nmb a2200000Iu 4500
"210812 2021 eng "
2199-2002
10.4230/LITES.7.1.2
doi
dc
We know what you're doing! Application detection using thermal data
Miedl, Philipp
Computer Engineering and Networks Laboratory, ETH Zurich, Gloriastrasse 35, Zurich, Switzerland https://www.linkedin.com/in/philippmiedl https://orcid.org/0000-0002-5828-8532
Ahmed, Rehan
Information Technology University of the Punjab, Arfa Software Technology Park, Ferozpur Road, Lahore, Pakistan https://orcid.org/0000-0002-1808-3954
Thiele, Lothar
Computer Engineering and Networks Laboratory, ETH Zurich, Gloriastrasse 35, Zurich, Switzerland https://people.ee.ethz.ch/~thiele/ https://orcid.org/0000-0001-6139-868X
Array
Modern mobile and embedded devices have high computing power which allows them to be used for multiple purposes. Therefore, applications with low security restrictions may execute on the same device as applications handling highly sensitive information. In such a setup, a security risk occurs if it is possible that an application uses system characteristics to gather information about another application on the same device.
In this work, we present a method to leak sensitive runtime information by just using temperature sensor readings of a mobile device. We employ a Convolutional-Neural-Network, Long Short-Term Memory units and subsequent label sequence processing to identify the sequence of executed applications over time. To test our hypothesis we collect data from two state-of-the-art smartphones and real user usage patterns. We show an extensive evaluation using laboratory data, where we achieve labelling accuracies up to 90% and negligible timing error. Based on our analysis we state that the thermal information can be used to compromise sensitive user data and increase the vulnerability of mobile devices. A study based on data collected outside of the laboratory opens up various future directions for research.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2021-08-12 08:36:56
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v007-i001-a002
Leibniz Transactions on Embedded Systems; Vol. 7 No. 1 (2021): Special Issue on Embedded System Security
eng
Copyright (c) 2021 Philipp Miedl, Rehan Ahmed, and Lothar Thiele
oai:ojs.dagstuhl.de:article/108
2021-08-12T07:00:26Z
lites:LITES-SECURITY
driver
nmb a2200000Iu 4500
"210812 2021 eng "
2199-2002
10.4230/LITES.7.1.1
doi
dc
Randomization as Mitigation of Directed Timing Inference Based Attacks on Time-Triggered Real-Time Systems with Task Replication
Krüger, Kristin
Department of Electrical and Computer Engineering, Technische Universität Kaiserslautern https://orcid.org/0000-0002-3201-5528
Vreman, Nils
Department of Automatic Control, Lund University https://orcid.org/0000-0002-6732-9500
Pates, Richard
Department of Automatic Control, Lund University https://orcid.org/0000-0001-6046-1878
Maggio, Martina
Department of Automatic Control, Lund University
Department of Computer Science, Saarland University https://orcid.org/0000-0002-1143-1127
Völp, Marcus
SnT - Université du Luxembourg https://orcid.org/0000-0002-8020-4446
Fohler, Gerhard
Department of Electrical and Computer Engineering, Technische Universität Kaiserslautern https://orcid.org/0000-0001-6162-2653
Array
Time-triggered real-time systems achieve deterministic behavior using schedules that are constructed offline, based on scheduling constraints. Their deterministic behavior makes time-triggered systems suitable for usage in safety-critical environments, like avionics. However, this determinism also allows attackers to fine-tune attacks that can be carried out after studying the behavior of the system through side channels, targeting safety-critical victim tasks. Replication -- i.e., the execution of task variants across different cores -- is inherently able to tolerate both accidental and malicious faults (i.e. attacks) as long as these faults are independent of one another. Yet, targeted attacks on the timing behavior of tasks which utilize information gained about the system behavior violate the fault independence assumption fault tolerance is based on. This violation may give attackers the opportunity to compromise all replicas simultaneously, in particular if they can mount the attack from already compromised components. In this paper, we analyze vulnerabilities of time-triggered systems, focusing on safety-certified multicore real-time systems. We introduce two runtime mitigation strategies to withstand directed timing inference based attacks: (i) schedule randomization at slot level, and (ii) randomization within a set of offline constructed schedules. We evaluate these mitigation strategies with synthetic experiments and a real case study to show their effectiveness and practicality.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2021-08-12 08:36:56
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v007-i001-a001
Leibniz Transactions on Embedded Systems; Vol. 7 No. 1 (2021): Special Issue on Embedded System Security
eng
Copyright (c) 2021 Kristin Krüger, Nils Vreman, Richard Pates, Martina Maggio, Marcus Völp, and Gerhard Fohler
oai:ojs.dagstuhl.de:article/110
2022-12-07T08:15:18Z
lites:LITES-HYBRID
driver
nmb a2200000Iu 4500
"221207 2022 eng "
2199-2002
10.4230/LITES.8.2.4
doi
dc
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems
Kamburjan, Eduard
Department of Informatics, University of Oslo, Norway; Department of Computer Science, Technische Universität Darmstadt, Germany https://orcid.org/0000-0002-0996-2543
Mitsch, Stefan
Computer Science Department, Carnegie Mellon University, USA https://orcid.org/0000-0002-3194-9759
Hähnle, Reiner
Department of Computer Science, Technische Universität Darmstadt, Germany https://orcid.org/0000-0001-8000-7613
Array
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-12-07 09:12:42
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a004
Leibniz Transactions on Embedded Systems; Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
eng
Copyright (c) 2022 Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle
oai:ojs.dagstuhl.de:article/112
2022-12-07T08:15:18Z
lites:LITES-HYBRID
driver
nmb a2200000Iu 4500
"221207 2022 eng "
2199-2002
10.4230/LITES.8.2.2
doi
dc
Swarms of Mobile Robots: Towards Versatility with Safety
Courtieu, Pierre
Conservatoire des arts et métiers, Cédric EA 4629, Paris, France https://orcid.org/0000-0001-8789-9781
Rieg, Lionel
VERIMAG, Grenoble INP - UGA, CNRS UMR 5104, Université Grenoble-Alpes, Saint Martin d'Hères, France
Tixeuil, Sébastien
Sorbonne University, CNRS, LIP6, Paris, France https://orcid.org/0000-0002-0948-7172
Urbain, Xavier
Université de Lyon, Université Claude Bernard Lyon 1, CNRS, INSA Lyon, LIRIS, UMR 5205, F-69622 Villeurbanne, France https://orcid.org/0000-0001-7442-2538
Array
We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-12-07 09:12:42
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a002
Leibniz Transactions on Embedded Systems; Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
eng
Copyright (c) 2022 Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain
oai:ojs.dagstuhl.de:article/114
2022-12-07T08:15:18Z
lites:LITES-HYBRID
driver
nmb a2200000Iu 4500
"221207 2022 eng "
2199-2002
10.4230/LITES.8.2.3
doi
dc
Higher-Dimensional Timed and Hybrid Automata
Fahrenberg, Uli
EPITA Research and Development Laboratory (LRDE), France https://orcid.org/0000-0001-9094-7625
Array
We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata.
The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-12-07 09:12:42
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a003
Leibniz Transactions on Embedded Systems; Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
eng
Copyright (c) 2022 Uli Fahrenberg
oai:ojs.dagstuhl.de:article/117
2022-12-07T08:15:18Z
lites:LITES-HYBRID
driver
nmb a2200000Iu 4500
"221207 2022 eng "
2199-2002
10.4230/LITES.8.2.1
doi
dc
Safety Verification of Networked Control Systems by Complex Zonotopes
Adimoolam, Arvind
Indian Institute of Technology Kanpur, Rajeev Motwani Building, Kalyanpur, Kanpur, India https://orcid.org/0000-0001-5991-2950
Dang, Thao
VERIMAG, CNRS/University Grenoble Alpes, Bâtiment IMAG, 700 Avenue Centrale, Grenoble, France
Array
Networked control systems (NCS) are widely used in real world applications because of their advantages, such as remote operability and reduced installation costs. However, they are prone to various inaccuracies in execution like delays, packet dropouts, inaccurate sensing and quantization errors. To ensure safety of NCS, their models have to be verified under the consideration of aforementioned uncertainties. In this paper, we tackle the problem of verifying safety of models of NCS under uncertain sampling time, inaccurate output measurement or estimation, and unknown disturbance input. Unbounded-time safety verification requires approximation of reachable sets by invariants, whose computation involves set operations. For uncertain linear dynamics, two important set operations for invariant computation are linear transformation and Minkowski sum operations. Zonotopes have the advantage that linear transformation and Minkowski sum operations can be efficiently approximated. However, they can not encode directions of convergence of trajectories along complex eigenvectors, which is closely related to encoding invariants. Therefore, we extend zonotopes to the complex valued domain by a representation called complex zonotope, which can capture contraction along complex eigenvectors for determining invariants. We prove a related mathematical result that in case of accurate feedback sampling, a complex zonotope will represent an invariant for a stable NCS. In addition, we propose an algorithm to verify the general case based on complex zonotopes, when there is uncertainty in sampling time and in input. We demonstrate the efficiency of our algorithm on benchmark examples and compare it with a state-of-the-art verification tool.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-12-07 09:12:42
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a001
Leibniz Transactions on Embedded Systems; Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
eng
Copyright (c) 2022 Arvind Adimoolam and Thao Dang
oai:ojs.dagstuhl.de:article/118
2022-12-07T08:15:18Z
lites:LITES-HYBRID
driver
nmb a2200000Iu 4500
"221207 2022 eng "
2199-2002
10.4230/LITES.8.2.6
doi
dc
From Dissipativity Theory to Compositional Construction of Control Barrier Certificates
Nejati, Ameneh
Department of Electrical Engineering, Technical University of Munich, Germany; Department of Computer Science, LMU Munich, Germany https://orcid.org/0000-0002-9065-1282
Zamani, Majid
Department of Computer Science, University of Colorado Boulder, USA; Department of Computer Science, LMU Munich, Germany https://orcid.org/0000-0001-6608-3708
Array
This paper proposes a compositional framework based on dissipativity approaches to construct control barrier certificates for networks of continuous-time stochastic hybrid systems. The proposed scheme leverages the structure of the interconnection topology and a notion of so-called control storage certificates to construct control barrier certificates compositionally. By utilizing those certificates, one can compositionally synthesize state-feedback controllers for interconnected systems enforcing safety specifications over a finite-time horizon. In particular, we leverage dissipativity-type compositionality conditions to construct control barrier certificates for interconnected systems based on corresponding control storage certificates computed for subsystems. Using those constructed control barrier certificates, one can quantify upper bounds on probabilities that interconnected systems reach certain unsafe regions in finite-time horizons. We employ a systematic technique based on the sum-of-squares optimization program to search for storage certificates of subsystems together with their corresponding safety controllers. We demonstrate our proposed results by applying them to a temperature regulation in a circular building containing 1000 rooms. To show the applicability of our approaches to dense networks, we also apply our proposed techniques to a fully-interconnected network.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-12-07 09:12:42
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a006
Leibniz Transactions on Embedded Systems; Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
eng
Copyright (c) 2022 Ameneh Nejati and Majid Zamani
oai:ojs.dagstuhl.de:article/119
2022-12-07T08:15:18Z
lites:LITES-HYBRID
driver
nmb a2200000Iu 4500
"221207 2022 eng "
2199-2002
10.4230/LITES.8.2.7
doi
dc
Real-Time Verification for Distributed Cyber-Physical Systems
Tran, Hoang-Dung
University of Nebraska-Lincoln, Lincoln, Nebraska, USA
Nguyen, Luan Viet
University of Dayton, Dayton, Ohio, USA
Musau, Patrick
Vanderbilt University, Nashville, Tennessee, USA
Xiang, Weiming
Augusta University, Nashville, Tennessee, USA
Johnson, Taylor T.
Vanderbilt University, Nashville, Tennessee, USA http://www.taylortjohnson.com/ https://orcid.org/0000-0001-8021-9923
Array
Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent transportation, where autonomous vehicles communicate and cooperate with each other via a high-speed communication network. Such systems require an ability to identify maneuvers in real-time that cause dangerous circumstances and ensure the implementation always meets safety-critical requirements. In this paper, we propose a real-time decentralized reachability approach for safety verification of a distributed multi-agent CPS with the underlying assumption that all agents are time-synchronized with a low degree of error. In the proposed approach, each agent periodically computes its local reachable set and exchanges this reachable set with the other agents with the goal of verifying the system safety. Our method, implemented in Java, takes advantages of the timing information and the reachable set information that are available in the exchanged messages to reason about the safety of the whole system in a decentralized manner. Any particular agent can also perform local safety verification tasks based on their local clocks by analyzing the messages it receives. We applied the proposed method to verify, in real-time, the safety properties of a group of quadcopters performing a distributed search mission.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-12-07 09:12:42
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a007
Leibniz Transactions on Embedded Systems; Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
eng
Copyright (c) 2022 Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson
oai:ojs.dagstuhl.de:article/121
2022-12-07T08:15:18Z
lites:LITES-HYBRID
driver
nmb a2200000Iu 4500
"221207 2022 eng "
2199-2002
10.4230/LITES.8.2.5
doi
dc
Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation
Kröger, Paul
Carl von Ossietzky Universität Oldenburg, 26111 Oldenburg, Germany https://orcid.org/0000-0002-0301-3611
Fränzle, Martin
Carl von Ossietzky Universität Oldenburg, 26111 Oldenburg, Germany https://orcid.org/0000-0002-9138-8340
Hybrid discrete-continuous system dynamics arises when discrete actions, e.g. by a decision algorithm, meet continuous behaviour, e.g. due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes.
Various flavours of hybrid automata have been suggested as a means to formally analyse CPS dynamics. In a previous article, we demonstrated that all these variants of hybrid automata provide inaccurate, in the sense of either overly pessimistic or overly optimistic, verdicts for engineered systems operating under imprecise observation of their environment due to, e.g., measurement error. We suggested a revised formal model, called Bayesian hybrid automata, that is able to represent state tracking and estimation in hybrid systems and thereby enhances precision of verdicts obtained from the model in comparison to traditional model variants.
In this article, we present an extended definition of Bayesian hybrid automata which incorporates a new class of guard and invariant functions that allow to evaluate traditional guards and invariants over probability distributions. The resulting framework allows to model observers with knowledge about the control strategy of an observed agent but with imprecise estimates of the data on which the control decisions are based.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-12-07 09:12:42
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a005
Leibniz Transactions on Embedded Systems; Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
eng
Copyright (c) 2022 Paul Kröger and Martin Fränzle
oai:ojs.dagstuhl.de:article/123
2022-11-16T07:32:50Z
lites:LITES-VISION
driver
nmb a2200000Iu 4500
"221116 2022 eng "
2199-2002
10.4230/LITES.8.1.3
doi
dc
HW-Flow: A Multi-Abstraction Level HW-CNN Codesign Pruning Methodology
Vemparala, Manoj-Rohit
BMW Autonomous Driving, Munich, Germany https://orcid.org/0000-0001-8186-8319
Fasfous, Nael
Technical University of Munich, Munich, Germany https://orcid.org/0000-0002-8081-7904
Frickenstein, Alexander
BMW Autonomous Driving, Munich, Germany
Valpreda, Emanuele
Politecnico di Torino, Turin, Italy https://orcid.org/0000-0002-1285-9360
Camalleri, Manfredi
BMW Autonomous Driving, Munich, Germany https://orcid.org/0000-0002-7050-8980
Zhao, Qi
BMW Autonomous Driving, Munich, Germany https://orcid.org/0000-0003-0944-8058
Unger, Christian
BMW Autonomous Driving, Munich, Germany
Nagaraja, Naveen-Shankar
BMW Autonomous Driving, Munich, Germany https://orcid.org/0000-0002-7608-1439
Martina, Maurizio
Politecnico di Torino, Turin, Italy https://orcid.org/0000-0002-3069-0319
Stechele, Walter
Technical University of Munich, Munich, Germany https://orcid.org/0000-0002-7455-8483
Convolutional neural networks (CNNs) have produced unprecedented accuracy for many computer vision problems in the recent past. In power and compute-constrained embedded platforms, deploying modern CNNs can present many challenges. Most CNN architectures do not run in real-time due to the high number of computational operations involved during the inference phase. This emphasizes the role of CNN optimization techniques in early design space exploration. To estimate their efficacy in satisfying the target constraints, existing techniques are either hardware (HW) agnostic, pseudo-HW-aware by considering parameter and operation counts, or HW-aware through inflexible hardware-in-the-loop (HIL) setups. In this work, we introduce HW-Flow, a framework for optimizing and exploring CNN models based on three levels of hardware abstraction: Coarse, Mid and Fine. Through these levels, CNN design and optimization can be iteratively refined towards efficient execution on the target hardware platform. We present HW-Flow in the context of CNN pruning by augmenting a reinforcement learning agent with key metrics to understand the influence of its pruning actions on the inference hardware. With 2× reduction in energy and latency, we prune ResNet56, ResNet50, and DeepLabv3 with minimal accuracy degradation on the CIFAR-10, ImageNet, and CityScapes datasets, respectively.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-11-16 08:31:03
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i001-a003
Leibniz Transactions on Embedded Systems; Vol. 8 No. 1 (2022): Special Issue on Embedded Systems for Computer Vision
eng
Copyright (c) 2022 Manoj-Rohit Vemparala, Nael Fasfous, Alexander Frickenstein, Emanuele Valpreda, Manfredi Camalleri, Qi Zhao, Christian Unger, Naveen-Shankar Nagaraja, Maurizio Martina, and Walter Stechele
oai:ojs.dagstuhl.de:article/127
2022-11-16T07:32:50Z
lites:LITES-VISION
driver
nmb a2200000Iu 4500
"221116 2022 eng "
2199-2002
10.4230/LITES.8.1.1
doi
dc
Susceptibility to Image Resolution in Face Recognition and Training Strategies to Enhance Robustness
Knoche, Martin
Technische Universität München, Arcisstrasse 21 80333 München, Deutschland https://orcid.org/0000-0002-0503-4600
Hörmann, Stefan
Technische Universität München, Arcisstrasse 21 80333 München, Deutschland
Rigoll, Gerhard
Technische Universität München, Arcisstrasse 21 80333 München, Deutschland https://orcid.org/0000-0003-1096-1596
Array
Many face recognition approaches expect the input images to have similar image resolution. However, in real-world applications, the image resolution varies due to different image capture mechanisms or sources, affecting the performance of face recognition systems. This work first analyzes the image resolution susceptibility of modern face recognition. Face verification on the very popular LFW dataset drops from 99.23% accuracy to almost 55% when image dimensions of both images are reduced to arguable very poor resolution. With cross-resolution image pairs (one HR and one LR image), face verification accuracy is even worse. This characteristic is investigated more in-depth by analyzing the feature distances utilized for face verification. To increase the robustness, we propose two training strategies applied to a state-of-the-art face recognition model: 1) Training with 50% low resolution images within each batch and 2) using the cosine distance loss between high and low resolution features in a siamese network structure. Both methods significantly boost face verification accuracy for matching training and testing image resolutions. Training a network with different resolutions simultaneously instead of adding only one specific low resolution showed improvements across all resolutions and made a single model applicable to unknown resolutions. However, models trained for one particular low resolution perform better when using the exact resolution for testing. We improve the face verification accuracy from 96.86% to 97.72% on the popular LFW database with uniformly distributed image dimensions between 112 × 112 px and 5 × 5 px. Our approaches improve face verification accuracy even more from 77.56% to 87.17% for distributions focusing on lower images resolutions. Lastly, we propose specific image dimension sets focusing on high, mid, and low resolution for five well-known datasets to benchmark face verification accuracy in cross-resolution scenarios.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-11-16 08:31:03
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i001-a001
Leibniz Transactions on Embedded Systems; Vol. 8 No. 1 (2022): Special Issue on Embedded Systems for Computer Vision
eng
Copyright (c) 2022 Martin Knoche
oai:ojs.dagstuhl.de:article/129
2022-11-16T07:32:50Z
lites:LITES-VISION
driver
nmb a2200000Iu 4500
"221116 2022 eng "
2199-2002
10.4230/LITES.8.1.2
doi
dc
Micro- and Macroscopic Road Traffic Analysis using Drone Image Data
Kruber, Friedrich
Technische Hochschule Ingolstadt, Esplanade 10, Ingolstadt, Germany https://orcid.org/0000-0002-7777-0033
Sánchez Morales, Eduardo
Technische Hochschule Ingolstadt, Esplanade 10, Ingolstadt, Germany https://orcid.org/0000-0001-8622-0757
Egolf, Robin
Technische Hochschule Ingolstadt, Esplanade 10, Ingolstadt, Germany https://orcid.org/0000-0001-6001-5827
Wurst, Jonas
Technische Hochschule Ingolstadt, Esplanade 10, Ingolstadt, Germany https://orcid.org/0000-0002-0399-3672
Chakraborty, Samarjit
University of North Carolina at Chapel Hill (UNC), Department of Computer Science, NC 27599, USA https://orcid.org/0000-0002-0503-6235
Botsch, Michael
Technische Hochschule Ingolstadt, Esplanade 10, Ingolstadt, Germany https://orcid.org/0000-0002-0900-1697
The current development in the drone technology, alongside with machine learning based image processing, open new possibilities for various applications. Thus, the market volume is expected to grow rapidly over the next years. The goal of this paper is to demonstrate the capabilities and limitations of drone based image data processing for the purpose of road traffic analysis.
In the first part a method for generating microscopic traffic data is proposed. More precisely, the state of vehicles and the resulting trajectories are estimated. The method is validated by conducting experiments with reference sensors and proofs to achieve precise vehicle state estimation results. It is also shown, how the computational effort can be reduced by incorporating the tracking information into a neural network. A discussion on current limitations supplements the findings. By collecting a large number of vehicle trajectories, macroscopic statistics, such as traffic flow and density can be obtained from the data. In the second part, a publicly available drone based data set is analyzed to evaluate the suitability for macroscopic traffic modeling. The results show that the method is well suited for gaining detailed information about macroscopic statistics, such as traffic flow dependent time headway or lane change occurrences. In conclusion, this paper presents methods to exploit the remarkable opportunities of drone based image processing for joint macro- and microscopic traffic analysis.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-11-16 08:31:03
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i001-a002
Leibniz Transactions on Embedded Systems; Vol. 8 No. 1 (2022): Special Issue on Embedded Systems for Computer Vision
eng
Copyright (c) 2022 Friedrich Kruber, Eduardo Sánchez Morales, Robin Egolf, Jonas Wurst, Samarjit Chakraborty, Michael Botsch
oai:ojs.dagstuhl.de:article/130
2021-08-12T07:00:26Z
lites:FOR
driver
nmb a2200000Iu 4500
"210812 2021 eng "
2199-2002
10.4230/LITES.7.1.0
doi
dc
Foreword
Burns, Alan
University of York, UK https://orcid.org/0000-0001-5621-8816
Goddard, Steve
University of Iowa, Iowa City, US
Array
Embedded systems are now an integral part of our lives. We have smart phones, smart meters, smart appliances, smart cars, smart grids, and smart houses--most relying on embedded systems with outdated security mechanisms, if they have any at all. A renewed emphasis on embedded systems security research is critical to our economies and our daily lives. This special issue on Embedded System Security attempts to contribute to this work by drawing attention to a number of key topics including Intrusion Detection and Tolerance, Confidence and Threat Modelling, Enhancing Dependability in Embedded Systems, and reducing Vulnerabilities in System Architectures for Embedded Systems.
Two papers are included in this initial instalment of the Special Issue. In the first paper ``"Randomization as Mitigation of Directed Timing Inference Based Attacks on Time-Triggered Real-Time Systems with Task Replication" by Kristin Krüger, Nils Vreman, Richard Pates, Martina Maggio, Marcus Völp and Gerhard Fohler, the vulnerabilities of time-triggered systems are investigated. They note that the assumption that faults are independent, which is often made for accidental faults, is not valid for malicious attacks. They go on to introduce two runtime mitigation strategies to withstand directed timing inference. Both involve the introduction of a level of randomization within the usual deterministic behaviour of time-triggered systems.
In the second paper ``"We know what you're doing! Application detection using thermal data", Philipp Miedl, Rehan Ahmed and Lothar Thiele consider how sensitive runtime information can be extracted from a system by just using temperature sensor readings from a mobile device. They employ a Convolutional-Neural-Network to identify the sequence of executed applications over time. They test their hypothesis via collected data from two state-of-the-art smartphones and real user usage patterns. The accuracy of their finding demonstrated that this is a clear vulnerability in mobile devices, including the potential to compromise sensitive user data.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2021-08-12 08:36:56
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/130
Leibniz Transactions on Embedded Systems; Vol. 7 No. 1 (2021): Special Issue on Embedded System Security
eng
Copyright (c) 2021 Alan Burns and Steve Goddard
oai:ojs.dagstuhl.de:article/133
2022-11-16T07:32:50Z
lites:LITES-VISION
driver
nmb a2200000Iu 4500
"221116 2022 eng "
2199-2002
10.4230/LITES.8.1.0
doi
dc
Introduction to the Special Issue on Embedded Systems for Computer Vision
Chakraborty, Samarjit
The University of North Carolina (UNC) at Chapel Hill, US https://cs.unc.edu/person/samarjit-chakraborty/ https://orcid.org/0000-0002-0503-6235
Rao, Qing
Momenta Europe GmbH, Stuttgart, Germany
Array
We provide a broad overview of some of the current research directions at the intersection of embedded systems and computer vision, in addition to introducing the papers appearing in this special issue. Work at this intersection is steadily growing in importance, especially in the context of autonomous and cyber-physical systems design. Vision-based perception is almost a mandatory component in any autonomous system, but also adds myriad challenges like, how to efficiently implement vision processing algorithms on resource-constrained embedded architectures, and how to verify the functional and timing correctness of these algorithms. Computer vision is also crucial in implementing various smart functionality like security, e.g., using facial recognition, or monitoring events or traffic patterns. Some of these applications are reviewed in this introductory article. The remaining articles featured in this special issue dive into more depth on a few of them.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-11-16 08:31:03
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i001-a000
Leibniz Transactions on Embedded Systems; Vol. 8 No. 1 (2022): Special Issue on Embedded Systems for Computer Vision
eng
Copyright (c) 2022 Samarjit Chakraborty, Qing Rao
oai:ojs.dagstuhl.de:article/136
2022-12-07T08:15:18Z
lites:LITES-HYBRID
driver
nmb a2200000Iu 4500
"221207 2022 eng "
2199-2002
10.4230/LITES.8.2.0
doi
dc
Introduction to the Special Issue on Distributed Hybrid Systems
Abate, Alessandro
University of Oxford, UK https://orcid.org/0000-0002-5627-9093
Fahrenberg, Uli
EPITA Research Laboratory (LRE), Paris, France https://orcid.org/0000-0001-9094-7625
Fränzle, Martin
Carl von Ossietzky Universität Oldenburg, Germany https://orcid.org/0000-0002-9138-8340
Array
This special issue contains seven papers within the broad subject of Distributed Hybrid Systems, that is, systems combining hybrid discrete-continuous state spaces with elements of concurrency and logical or spatial distribution. It follows up on several workshops on the same theme which were held between 2017 and 2019 and organized by the editors of this volume.
The first of these workshops was held in Aalborg, Denmark, in August 2017 and associated with the MFCS conference. It featured invited talks by Alessandro Abate, Martin Fränzle, Kim G. Larsen, Martin Raussen, and Rafael Wisniewski. The second workshop was held in Palaiseau, France, in July 2018, with invited talks by Luc Jaulin, Thao Dang, Lisbeth Fajstrup, Emmanuel Ledinot, and André Platzer. The third workshop was held in Amsterdam, The Netherlands, in August 2019, associated with the CONCUR conference. It featured a special theme on distributed robotics and had invited talks by Majid Zamani, Hervé de Forges, and Xavier Urbain.
The vision and purpose of the DHS workshops was to connect researchers working in real-time systems, hybrid systems, control theory, formal verification, distributed computing, and concurrency theory, in order to advance the subject of distributed hybrid systems. Such systems are abundant and often safety-critical, but ensuring their correct functioning can in general be challenging. The investigation of their dynamics by analysis tools from the aforementioned domains remains fragmentary, providing the rationale behind the workshops: it was conceived that convergence and interaction of theories, methods, and tools from these different areas was needed in order to advance the subject.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
2022-12-07 09:12:42
application/pdf
https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a000
Leibniz Transactions on Embedded Systems; Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
eng
Copyright (c) 2022 Alessandro Abate, Uli Fahrenberg, Martin Fränzle