FocusE: A semantic extension of FocusST
Maria Spichkova
TL;DR
This paper presents Focus$^{E}$ as a semantic extension of Focus$^{ST}$ to model event-based streams for interactive systems. It explains the differences between time-based and causality-based streams, including the notion of causality intervals and an operator to access the i-th interval, and situates Focus$^{E}$ as compatible with the existing Focus$^{ST}$ framework. The approach aims to improve readability and verifiability of formal specifications while preserving the component-based, assumption-guarantee methodology and enabling formal proofs in Isabelle. The practical impact lies in providing a rigorous, readable, and verifiable formalism for event-driven interactive systems, useful for safety/security analysis and verification beyond point-wise testing.
Abstract
To analyse and verify the safety and security properties of interactive systems, a formal specification might be necessary. There are many types of formal languages and frameworks. The decision regarding what type of formal specification should be applied in each particular case depends on many factors. One of the approaches to specify interactive systems formally is to present them as a composition of components processing data and control streams. In this short paper, we present FocusE, a formal approach for modelling event-based streams. The proposed approach is based on a formal language FocusST, and can be seen as its semantic extension.