On Pragmatic System Design through Learning and Implementation-oriented Reachability Analysis

Thumbnail Image
Journal Title
Journal ISSN
Volume Title
School of Science | Doctoral thesis (article-based) | Defence date: 2023-08-30
Degree programme
56 + app. 126
Aalto University publication series DOCTORAL THESES, 126/2023
The need for formalization and verification in the design of complex systems is now more evident than ever. However, formal methods practices can sometimes be challenging to adopt in industrial environments. In particular, two broad categories of challenges can be identified: (a) The algorithmic challenge, which is about the ability of related tools and algorithms to scale to industrial size problems, and (b) the modeling challenge, which is about obtaining a formal system model as well as a formal specification of its behavior. To the end of easing integration of formal methods in industrial model based system engineering workflows, a solution is developed in this thesis aiming to help address the modeling challenge through contributions to four key areas of the process: (1) requirements formalization, (2) monitor generation, (3) model extraction from example behavior traces, and (4) reachability analysis for dynamical system implementations (C/C++ code).
Supervising professor
Brzuska, Chris, Assoc. Prof. Aalto University, Department of Computer Science, Finland
Thesis advisor
Tripakis, Stavros, Assoc. Prof., Northeastern University, USA
Basagiannis, Stylianos, Dr., Collins Aerospace, Ireland
formal methods, learning, requirements formalization, monitor generation, reachability analysis
Other note
  • [Publication 1]: Georgios Giantamidis, Georgios Papanikolaou, Marcelo Miranda, Gonzalo Salinas-Hernando, Juan Valverde-Alcalá, Suresh Veluru, Stylianos Basagiannis. ReForm: A Tool for Rapid Requirements Formalization. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., Vol 79, 2020.
    DOI: 10.14279/tuj.eceasst.79.1117 View at publisher
  • [Publication 2]: Georgios Giantamidis, Stylianos Basagiannis, Stavros Tripakis. Efficient Translation of Safety LTL to DFA Using Symbolic Automata Learning and Inductive Inference. In Computer Safety, Reliability, and Security, 2020.
    DOI: 10.1007/978-3-030-54549-9_8 View at publisher
  • [Publication 3]: Georgios Giantamidis, Stavros Tripakis, Stylianos Basagiannis. Learning Moore machines from input–output traces. International Journal on Software Tools for Technology Transfer, Vol 23, 1-29, 2021.
    DOI: 10.1007/s10009-019-00544-0 View at publisher
  • [Publication 4]: Georgios Giantamidis, Stavros Tripakis. Learning Moore Machines from Input-Output Traces. In FM 2016: Formal Methods, 2016.
    DOI: 10.1007/978-3-319-48989-6_18 View at publisher
  • [Publication 5]: Vassilios A. Tsachouridis, Georgios Giantamidis, Stylianos Basagiannis, Kostas Kouramas. Formal analysis of the Schulz matrix inversion algorithm: A paradigm towards computer aided verification of general matrix flow solvers. Numerical Algebra, Control & Optimization, Vol 10(2), 177-206, 2020.
    DOI: 10.3934/naco.2019047 View at publisher
  • [Publication 6]: Vassilios A. Tsachouridis, Georgios Giantamidis. Computer-aided verification of matrix Riccati algorithms. In 58th Conference on Decision and Control, 2019.
    DOI: 10.1109/CDC40024.2019.9030135 View at publisher