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

Thumbnail Image

Files

isbn9789526413877.pdf (540.53 KB)

URL

Journal Title

Journal ISSN

Volume Title

School of Science | Doctoral thesis (article-based) | Defence date: 2023-08-30
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.

Authors

Date

2023

Department

Tietotekniikan laitos
Department of Computer Science

Major/Subject

Mcode

Degree programme

Language

en

Pages

56 + app. 126

Series

Aalto University publication series DOCTORAL THESES, 126/2023

Abstract

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).

Description

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

Keywords

formal methods, learning, requirements formalization, monitor generation, reachability analysis

Other note

Parts

  • [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

Citation

Permanent link to this item

https://urn.fi/URN:ISBN:978-952-64-1387-7

Collections

[diss] Perustieteiden korkeakoulu / SCI