Prof. Panagiotis Katsaros
Biography
Prof. Panagiotis Katsaros is an Associate Professor in the School of Informatics of the Aristotle University of Thessaloniki, the largest University of Greece. His research interests are in the field of model-driven software and system engineering and focus on rigorous design and formal verification techniques, but he has also conducted research on the safety and security of systems and software. He has authored 2 textbooks (in Greek), co-edited 2 books and co-authored 29 journal articles & 65 conference papers, most of which appear in top conferences and journals such as in Journal of Systems and Software, Information and Computation, Logical Methods in Computer Science, Reliability Engineering and System Safety, Computers & Security, NASA Formal Methods Symposium (NFM), Int. Conf. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Among his best known research are the contributions (with collaborators) on the Model Repair problem for Kripke structures and probabilistic models, as well as on the runtime model checking for the provisioning of cloud resources. More recently, Prof. Katsaros and collaborators presented new techniques for the early validation of system requirements and design with formal methods, as well as for the correct-by-construction design of real-time embedded software for multicores based on a novel model of computation. Prof. Katsaros has chaired the 21st edition of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018), which is the primary European forum for researchers working on topics related to Software Science, and co-chairs the 6th International Symposium on Model-Based Safety and Assessment (IMBSA) to be held in October 2019 in Thessaloniki. He has coordinated two international research projects on spacecraft on-board software design that were funded by the European Space Agency (ESA) and has participated in another two such projects, whereas he was PI in numerous other national and international projects. Prof. Katsaros has supervised 4 completed PhDs on the aforementioned topics and maintains an active research network of collaborators in Europe, US and more recently in China. Finally, Prof. Katsaros has given invited talks in European research institutions such as in the University of Oxford, the University of Groningen and elsewhere, whereas his works have been selected two times for the best paper award in international conferences.
Abstract
In the model-driven design of software and systems, approaches aiming to achieve correctness-by-construction are a natural alternative towards avoiding the well-known scalability limitations of model checking. Ensuring correctness by design rather than through verification is the main challenge of a few worthy research efforts during the last few years. We present two different perspectives of correctness-by-construction and the associated design frameworks developed in our recent research work.
The first perspective concerns with the early validation of requirements [1], in order to reduce the need for the high-cost validation testing and corrective measures at the late development stages. Here, we take into account that system designers usually try to address the requirements by (re-)using and combining existing solutions to design problems. We therefore propose an approach for requirements formalisation and rigorous design, which allows building complex designs by composing simpler reusable designs (patterns) that provably enforce given properties. Correctness-by-construction is based on a theory of property enforcement and property composability, while integrating the models. If some properties cannot be enforced nor verified, the model is refined or certain requirements are revised. At the end, a validated model of the system under design provides evidence of requirements' consistency and design correctness. Such an approach incurs extra cost to be paid for delivering early evidence that the requirement specifications are realisable; on the other hand, late-stage validation, relying on testing and requiring high-cost corrective measures, can be drastically reduced.
The second perspective of correctness-by-construction [2] shows how a system's implementation can be derived from a high-level formal model of computation encoding the application's execution semantics, through applying semantics preserving model transformations. Our model of computation combines streaming and reactive control behaviour with task parallelism for utilising multicore processing. The model is programmed independently from the execution platform and thus we avoid to program low-level real-time OS services (e.g., for task management), whereas applications are rendered provably correct in the sense that for any given test stimuli, a deterministic output response is expected (therefore, they become amenable to testing). Schedulability is established by static analysis of the high-level model. Our semantics preserving model transformation framework is then employed to generate code from the high-level model that is executable on the runtime environment of a formal modelling language, which has been ported on multi-core platforms.
Both design flows have been semi-automated through new and existing tools and their effectiveness has been evaluated on the control software of real satellite systems. More specifically: (i) in the first case, on a set of requirements for the control software of a nano-satellite and an extract of software requirements for a Low Earth Orbit observation satellite, and (ii) in the second case, on a guidance-navigation and control application of a satellite system that was ported onto a radiation hardened multi-core platform.
[1] Emmanouela Stachtiari, Anastasia Mavridou, Panagiotis Katsaros, Simon Bliudze, Joseph Sifakis, Early validation of system requirements and design through correctness-by-construction, Journal of Systems and Software, Vol. 145, pp. 52-78, Elsevier, 2018.
[2] Fotios Gioulekas, Petro Poplavko, Panagiotis Katsaros, Saddek Bensalem, Pedro Palomo, Correct-by-construction model-based design of reactive streaming software for multi-core embedded systems, International Journal on Software Tools for Technology Transfer, Springer, 2019.