Search

To stimulate the development and application of formal methods in industry, we need to promote research and development for the improvement of formal methods and tools for industrial applications, and we need to exchange experiences of the industrial usage of these methods and tools. This special issue of Software Tools for Technology Transfer presents various tools and experience reports that are targeting the use of formal methods in industry. The papers in this special issue are extended versions of selected conference papers from the proceedings of the 27th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2022). [ABSTRACT FROM AUTHOR]

This article is a follow-up contribution that extends the conference paper (Nxumalo, in: Laarman, Sokolova (eds)Model Checking Software - 27th International Symposium, 2021) which presented the spotlight abstraction method to enable an efficient model checking of schedulability properties of real-time operating systems. Our approach is based on iterative spotlight abstraction whereby the real-time task queue is divided into a so-called spotlight and a shade. Initially, an abstract state space model is generated from the spotlight, which contains a small number of tasks that appear at the front of the queue and the shade contains the remaining tasks. The schedulability of the spotlight tasks is model checked, whereas the behavior of the shade is summarized, and the result is saved for later re-use. If this result is still inconclusive, more tasks are iteratively brought from the shade into the spotlight, with which the model checker can proceed. These steps are repeated until a decisive schedulability result is obtained. In this article, we enrich the encoding of real-time systems into timed automata by separating operations over clock variables from operations based on other variables such as Boolean and integers. We enforce to maintain a reasonable size of the spotlight model by applying counter abstraction to the tasks that were previously confirmed schedulable in the previous iterations. We compare our approach against Timestool and RTLib, an Uppaal template, in the analysis of the schedulability of real-time tasks for the First-In-First-Out and Shortest-Deadline-First scheduling policies. Empirical results show that our approach can handle more tasks than Timestool and RTLib. [ABSTRACT FROM AUTHOR]

Parametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper continues our work exploring the relationship between specification techniques for parametric runtime verification. Here we consider the correspondence between trace-slicing automata-based approaches and rule systems. The main contribution is a translation from quantified automata to rule systems, which has been implemented in Scala. This then allows us to highlight the key differences in how the two formalisms handle data, an important step in our wider effort to understand the correspondence between different specification languages for parametric runtime verification. This paper extends a previous conference version of this paper with further examples, a proof of correctness, and an optimisation based on a notion of redundancy observed during the development of the translation. [ABSTRACT FROM AUTHOR]

In order to develop reliable software and systems, we depend on practical techniques for the construction and analysis of such software and systems. This special issue of Software Tools for Technology Transfer presents various tool-supported techniques that can help with the construction and analysis of such reliable software and systems. The papers in this special issue are extended versions of selected conference papers from the proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018). [ABSTRACT FROM AUTHOR]