h1

h2

h3

h4

h5
h6

MISSION

Models in Space Systems: Integration, Operation, and Networking

Grant period2021-10-01 - 2025-09-30
Funding bodyEuropean Union
Call numberH2020-MSCA-RISE-2020
Grant number101008233
IdentifierG:(EU-Grant)101008233

Note: Spacecraft must work robustly in the presence of uncertainties such as random hardware faults, operator mistakes, space debris, and radiation. Classic space missions address uncertainty via large safety margins and bult-in redundancy, leading to a spiral of increasing cost and complexity. A recent trend is the small-business commercialisation of space using commercial-off-the-shelf components for networked constellations of small satellites. This "New Space" approach reduces component weight, size, price, and lead time, and makes innovation increasingly driven by software. This pertains especially to resource management and data handling, while simpler components and new interactions increase uncertainty, and come with less reliable parts. Thus, overall mission connectivity, efficiency, dependability and safety in the New Space needs to be achieved on a system level - for which there is no systematic approach yet. This is partly rooted in the empirical focus of many teams, and partly in a lack of easy-to-use methods to model, analyse, and guarantee system-level dependability. This interdisciplinary project sets out to solve this space engineering problem by exploiting highly advanced techniques from the forefront of computing science research, especially model-based algorithmics. We strive for sound and efficient software tools for the development of dependable, networked, and resource-aware New Space missions. For this, the MISSION project will develop an integrated model-based technology to establish and maintain system-level properties of critical space mission parameters. A strong consortium of excellent academic and industrial partners in Europe, Argentina, and China has agreed on a joint research and knowledge sharing agenda that will foster a shared culture of research and innovation, to finally deliver an ecosystem of easy-to-use methods and software tools to the New Space industry.
   

Recent Publications

All known publications ...
Download: BibTeX | EndNote XML,  Text | RIS | 

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Software  ;  ;
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Artifact Evaluation)
Zenodo () [10.5281/ZENODO.18188200]  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Dissertation / PhD Thesis  ;  ;
Analysis of probabilistic programs using generating functions
Aachen : RWTH Aachen University 1 Online-Ressource : Illustrationen () [10.18154/RWTH-2025-07571] = Dissertation, RWTH Aachen University, 2025  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book  ;  ;  ;
J-P: MDP. FP. PP: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs
Principles of verification: cycling the probabilistic landscape, Part 1 / Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk, editors Cham : Springer, Lecture notes in computer science 15260, 255-302 () [10.1007/978-3-031-75783-9_11]  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book  ;  ;  ;
Symbolic Quantitative Information Flow for Probabilistic Programs
Principles of verification: cycling the probabilistic landscape, Part 1 / Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk, editors Cham : Springer, Lecture notes in computer science 15260, 128-154 () [10.1007/978-3-031-75783-9_6]  GO  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article/Contribution to a conference proceedings  ;  ;  ;  ;
Stochastic games with lexicographic objectives
Conference on Computer-Aided Verification, CAV 2020, onlineonline, 21 Jul 2020 - 24 Jul 20202020-07-212020-07-24
Conference on Computer-Aided Verification, CAV 2021, onlineonline, 20 Jul 2021 - 23 Jul 20212021-07-202021-07-23 Formal methods in system design 63(1/3), 40-80 () [10.1007/s10703-023-00411-4] special issue: "Special issue on 'CAV 2020 - 2021'"  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article  ;  ;  ;  ;
Encoding inductive invariants as barrier certificates : Synthesis via difference-of-convex programming
Information and computation 289(A), 104965 () [10.1016/j.ic.2022.104965]  GO  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

All known publications ...
Download: BibTeX | EndNote XML,  Text | RIS | 

 Record created 2021-10-10, last modified 2023-02-11
Similar records



Rate this document:

Rate this document:
1
2
3
4
5
 
(Not yet reviewed)