Καλησπέρα σας,
στα πλαίσια του μαθήματος "Space Software", την Τρίτη 9/12 θα έχουμε τη χαρά να υποδεχθούμε 2 προσκεκλημένες ομιλίες. Οι τίτλοι και τα abstracts ακολουθούν - οι ομιλίες θα είναι στα ελληνικά, στην αίθουσα Β214 και θα ξεκινήσουν στις 13:15.
Advancing Space Software Development: An Introduction to the F' Framework for Satellite Systems
Christoforos Vasilakis - Section of Electronic Physics and Systems, Physics Dept. University of Athens
This presentation provides a comprehensive overview of the architectural and development considerations for satellite on-board software (OBSW). Beginning with an introduction to satellite subsystems and the core responsibilities of the on-board computer (OBC), the discussion highlights the critical role of microcontrollers in executing software tasks essential to satellite operations. The focus then shifts to F', an open-source framework developed by NASA's Jet Propulsion Laboratory (JPL), designed to streamline the development and deployment of flight software. By leveraging its modular and reusable components, the Fprime enables efficient implementation of satellite functionalities, including the telemetry, the command handling, the event logging, and the file management. The session concludes with the exploration of a flight software architecture using the Fprime framework, demonstrating how its structured approach facilitates the development of reliable and scalable OBSW.
Specification of Internet of Things (IoT) and edge systems with Linear Temporal Logic (LTL)
Angeliki Pantiora - Space Software Group, University of Athens
IoT and edge systems induce complex, heterogeneous, and distributed environments where interconnected physical devices and localized computing resources exhibit intricate behaviors. Specifying behavioral requirements in such contexts is inherently challenging yet essential, since formal specifications provide a critical foundation for tasks such as verification or synthesis. This presentation opens by detailing the suitability of LTL in specifying behavioral requirements for IoT and edge systems, along with its limitations. This is followed by a comprehensive, tool-supported quantitative analysis of LTL requirement-formula pairs drawn from the academic literature of the past decade (2015–2024). Specifically, this analysis aims to reveal: (i) adoption trends for temporal logic, particularly LTL, in the specification of edge and IoT systems, (ii) insights regarding the engineering complexity of LTL formulae and its correlation with the natural language formulation of corresponding requirements, and (iii) the frequency each temporal, logical, and comparison operator is utilized in LTL property specifications, and how these frequencies relate to the defining characteristic of edge and IoT systems.