Contract Based Program Models for Software Model Checking
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916652621234176 |
|---|---|
| author | Amilon, Jesper Gurov, Dilian |
| author_facet | Amilon, Jesper Gurov, Dilian |
| contents | Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating suitable abstractions is another difficult problem. We argue that such abstract models can be obtained with little effort, when the state transformation properties of the software components have already been deductively verified. As a concrete, language-independent representation of such abstractions we propose the use of \emph{flow graphs}, a formalism previously developed for the purposes of compositional model checking. In this paper, we describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written in~C. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_11236 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Contract Based Program Models for Software Model Checking Amilon, Jesper Gurov, Dilian Formal Languages and Automata Theory Software Engineering Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating suitable abstractions is another difficult problem. We argue that such abstract models can be obtained with little effort, when the state transformation properties of the software components have already been deductively verified. As a concrete, language-independent representation of such abstractions we propose the use of \emph{flow graphs}, a formalism previously developed for the purposes of compositional model checking. In this paper, we describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written in~C. |
| title | Contract Based Program Models for Software Model Checking |
| topic | Formal Languages and Automata Theory Software Engineering |
| url | https://arxiv.org/abs/2503.11236 |