<p>Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the state-space explosion problem and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole state-space and (ii) providing a robustness measure instead of yes/no answers. In this paper, we consider real-time systems where executions and specifications are modelled as timed signals and Signal Temporal Logic (STL) formulae, respectively. We propose a new temporal robustness measure <InlineEquation ID="IEq1"> <EquationSource Format="MATHML"><math> <mi>δ</mi> </math></EquationSource> <EquationSource Format="TEX">$\delta $</EquationSource> </InlineEquation> for STL, based on a new distance that we define over timed signals. In contrast with existing measures, <InlineEquation ID="IEq2"> <EquationSource Format="MATHML"><math> <mi>δ</mi> </math></EquationSource> <EquationSource Format="TEX">$\delta $</EquationSource> </InlineEquation> provides a precise quantification of distances between the monitored signal and the boundary separating faulty and non-faulty executions w.r.t. an STL property. Thus, <InlineEquation ID="IEq3"> <EquationSource Format="MATHML"><math> <mi>δ</mi> </math></EquationSource> <EquationSource Format="TEX">$\delta $</EquationSource> </InlineEquation> is suitable for a wide range of real-life perturbations, such as those affecting exclusively a particular time window within a signal. Though we prove that computing <InlineEquation ID="IEq4"> <EquationSource Format="MATHML"><math> <mi>δ</mi> </math></EquationSource> <EquationSource Format="TEX">$\delta $</EquationSource> </InlineEquation> is NP-hard in general, we provide efficient algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response. This paper is an extension of&#xa0;(Rino et&#xa0;al. in Joint International Conference on Quantitative Evaluation of SysTems &amp; International Conference on Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), <CitationRef CitationID="CR1">2024</CitationRef>), published at QEST+FORMATS 2024. The extension includes implementation of algorithms to compute <InlineEquation ID="IEq5"> <EquationSource Format="MATHML"><math> <mi>δ</mi> </math></EquationSource> <EquationSource Format="TEX">$\delta $</EquationSource> </InlineEquation> in a prototype tool, and an evaluation of our approach on a case study of quality assessment of insulin controllers for diabetic patients.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Efficiently computable temporal robustness for a practical STL fragment

  • Neha Rino,
  • Mohammed Foughali,
  • Florian Renkin,
  • Eugene Asarin

摘要

Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the state-space explosion problem and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole state-space and (ii) providing a robustness measure instead of yes/no answers. In this paper, we consider real-time systems where executions and specifications are modelled as timed signals and Signal Temporal Logic (STL) formulae, respectively. We propose a new temporal robustness measure δ $\delta $ for STL, based on a new distance that we define over timed signals. In contrast with existing measures, δ $\delta $ provides a precise quantification of distances between the monitored signal and the boundary separating faulty and non-faulty executions w.r.t. an STL property. Thus, δ $\delta $ is suitable for a wide range of real-life perturbations, such as those affecting exclusively a particular time window within a signal. Though we prove that computing δ $\delta $ is NP-hard in general, we provide efficient algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response. This paper is an extension of (Rino et al. in Joint International Conference on Quantitative Evaluation of SysTems & International Conference on Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), 2024), published at QEST+FORMATS 2024. The extension includes implementation of algorithms to compute δ $\delta $ in a prototype tool, and an evaluation of our approach on a case study of quality assessment of insulin controllers for diabetic patients.