Automated quantitative software verification
<p>Many software systems exhibit probabilistic behaviour, either added explicitly, to improve performance or to break symmetry, or implicitly, through interaction with unreliable networks or faulty hardware. When employed in safety-critical applications, it is important to rigorously analyse t...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2010
|
| Subjects: |
| _version_ | 1797072006224543744 |
|---|---|
| author | Kattenbelt, M |
| author2 | Kwiatkowska, M |
| author_facet | Kwiatkowska, M Kattenbelt, M |
| author_sort | Kattenbelt, M |
| collection | OXFORD |
| description | <p>Many software systems exhibit probabilistic behaviour, either added explicitly, to improve performance or to break symmetry, or implicitly, through interaction with unreliable networks or faulty hardware. When employed in safety-critical applications, it is important to rigorously analyse the behaviour of these systems. This can be done with a formal verification technique called <em>model checking</em>, which establishes <em>properties</em> of systems by algorithmically considering all execution scenarios. In the presence of probabilistic behaviour, we consider quantitative properties such as <em>"the worst-case probability that the airbag fails to deploy within 10ms"</em>, instead of qualitative properties such as <em>"the airbag eventually deploys"</em>. Although many model checking techniques exist to verify <em>qualitative</em> properties of software, <em>quantitative</em> model checking techniques typically focus on manually derived models of systems and cannot directly verify software.</p> <p>In this thesis, we present two quantitative model checking techniques for probabilistic software. The first is a quantitative adaptation of a successful model checking technique called <em>counter-example guided abstraction refinement</em> which uses <em>stochastic two-player games</em> as abstractions of probabilistic software. We show how to achieve abstraction and refinement in a probabilistic setting and investigate theoretical extensions of stochastic two-player game abstractions. Our second technique <em>instruments</em> probabilistic software in such a way that existing, non-probabilistic software verification methods can be used to compute bounds on quantitative properties of the original, uninstrumented software.</p> <p>Our techniques are the first to target real, compilable software in a probabilistic setting. We present an experimental evaluation of both approaches on a large range of case studies and evaluate several extensions and heuristics. We demonstrate that, with our methods, we can successfully compute quantitative properties of real network clients comprising approximately 1,000 lines of complex ANSI-C code — the verification of such software is far beyond the capabilities of existing quantitative model checking techniques.</p> |
| first_indexed | 2024-03-06T23:01:24Z |
| format | Thesis |
| id | oxford-uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T23:01:24Z |
| publishDate | 2010 |
| record_format | dspace |
| spelling | oxford-uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f52022-03-26T18:05:03ZAutomated quantitative software verificationThesishttp://purl.org/coar/resource_type/c_db06uuid:62430df4-7fdf-4c4f-b3cd-97ba8912c9f5Theory and automated verificationEnglishOxford University Research Archive - Valet2010Kattenbelt, MKwiatkowska, M<p>Many software systems exhibit probabilistic behaviour, either added explicitly, to improve performance or to break symmetry, or implicitly, through interaction with unreliable networks or faulty hardware. When employed in safety-critical applications, it is important to rigorously analyse the behaviour of these systems. This can be done with a formal verification technique called <em>model checking</em>, which establishes <em>properties</em> of systems by algorithmically considering all execution scenarios. In the presence of probabilistic behaviour, we consider quantitative properties such as <em>"the worst-case probability that the airbag fails to deploy within 10ms"</em>, instead of qualitative properties such as <em>"the airbag eventually deploys"</em>. Although many model checking techniques exist to verify <em>qualitative</em> properties of software, <em>quantitative</em> model checking techniques typically focus on manually derived models of systems and cannot directly verify software.</p> <p>In this thesis, we present two quantitative model checking techniques for probabilistic software. The first is a quantitative adaptation of a successful model checking technique called <em>counter-example guided abstraction refinement</em> which uses <em>stochastic two-player games</em> as abstractions of probabilistic software. We show how to achieve abstraction and refinement in a probabilistic setting and investigate theoretical extensions of stochastic two-player game abstractions. Our second technique <em>instruments</em> probabilistic software in such a way that existing, non-probabilistic software verification methods can be used to compute bounds on quantitative properties of the original, uninstrumented software.</p> <p>Our techniques are the first to target real, compilable software in a probabilistic setting. We present an experimental evaluation of both approaches on a large range of case studies and evaluate several extensions and heuristics. We demonstrate that, with our methods, we can successfully compute quantitative properties of real network clients comprising approximately 1,000 lines of complex ANSI-C code — the verification of such software is far beyond the capabilities of existing quantitative model checking techniques.</p> |
| spellingShingle | Theory and automated verification Kattenbelt, M Automated quantitative software verification |
| title | Automated quantitative software verification |
| title_full | Automated quantitative software verification |
| title_fullStr | Automated quantitative software verification |
| title_full_unstemmed | Automated quantitative software verification |
| title_short | Automated quantitative software verification |
| title_sort | automated quantitative software verification |
| topic | Theory and automated verification |
| work_keys_str_mv | AT kattenbeltm automatedquantitativesoftwareverification |