Kovalov, Andrii and Lobe, Elisabeth and Gerndt, Andreas and Lüdtke, Daniel (2017) Task-Node Mapping in an Arbitrary Computer Network Using SMT Solver. In: Integrated Formal Methods Lecture Notes in Computer Science, 10510. Springer, Cham. doi: 10.1007/978-3-319-66845-1_12. ISBN 978-3-319-66845-1. ISSN 1611-3349.
|
PDF
400kB |
Official URL: http://dx.doi.org/10.1007/978-3-319-66845-1_12
Abstract
The problem of mapping (assigning) application tasks to processing nodes in a distributed computer system for spacecraft is investigated in this paper. The network architecture is developed in the project ‘Scalable On-Board Computing for Space Avionics’ (ScOSA) at the German Aerospace Center (DLR). In ScOSA system the processing nodes are connected to a network with an arbitrary topology. The applications are structured as directed graphs of periodic and aperiodic tasks that exchange messages. In this paper a formal definition of the mapping problem is given. We demonstrate several ways to formulate it as a satisfiability modulo theories (SMT) problem and then use Z3, a state-of-the-art SMT solver, to produce the mapping. The approach is evaluated on a mapping problem for an optical navigation application as well as on a set of randomly generated task graphs.
| Item URL in elib: | https://elib.dlr.de/114452/ | ||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Document Type: | Book Section | ||||||||||||||||||||
| Title: | Task-Node Mapping in an Arbitrary Computer Network Using SMT Solver | ||||||||||||||||||||
| Authors: |
| ||||||||||||||||||||
| Date: | September 2017 | ||||||||||||||||||||
| Journal or Publication Title: | Integrated Formal Methods | ||||||||||||||||||||
| Refereed publication: | Yes | ||||||||||||||||||||
| Open Access: | Yes | ||||||||||||||||||||
| Gold Open Access: | No | ||||||||||||||||||||
| In SCOPUS: | No | ||||||||||||||||||||
| In ISI Web of Science: | No | ||||||||||||||||||||
| Volume: | 10510 | ||||||||||||||||||||
| DOI: | 10.1007/978-3-319-66845-1_12 | ||||||||||||||||||||
| Editors: |
| ||||||||||||||||||||
| Publisher: | Springer, Cham | ||||||||||||||||||||
| Series Name: | Lecture Notes in Computer Science | ||||||||||||||||||||
| ISSN: | 1611-3349 | ||||||||||||||||||||
| ISBN: | 978-3-319-66845-1 | ||||||||||||||||||||
| Status: | Published | ||||||||||||||||||||
| Keywords: | task-node mapping, SMT | ||||||||||||||||||||
| HGF - Research field: | Aeronautics, Space and Transport | ||||||||||||||||||||
| HGF - Program: | Space | ||||||||||||||||||||
| HGF - Program Themes: | Space System Technology | ||||||||||||||||||||
| DLR - Research area: | Raumfahrt | ||||||||||||||||||||
| DLR - Program: | R SY - Space System Technology | ||||||||||||||||||||
| DLR - Research theme (Project): | R - Scosa Onboard Computing (old) | ||||||||||||||||||||
| Location: | Braunschweig | ||||||||||||||||||||
| Institutes and Institutions: | Institut of Simulation and Software Technology > Software for Space Systems and Interactive Visualisation | ||||||||||||||||||||
| Deposited By: | Kovalov, Andrii | ||||||||||||||||||||
| Deposited On: | 29 Sep 2017 10:24 | ||||||||||||||||||||
| Last Modified: | 31 Jul 2019 20:11 |
Repository Staff Only: item control page