Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
| Autor: | Peter Lammich, Julian Brunner |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Model checking
Correctness Computer science HOL 02 engineering and technology computer.software_genre Artificial Intelligence 0502 economics and business 0202 electrical engineering electronic engineering information engineering formal verification partial order reduction Formal verification computer.programming_language Programming language 05 social sciences Proof assistant computer.file_format model checking Partial order reduction Computational Theory and Mathematics Promela TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 050211 marketing 020201 artificial intelligence & image processing Executable Algorithm computer Software |
| Zdroj: | Brunner, J & Lammich, P 2018, ' Formal Verification of an Executable LTL Model Checker with Partial Order Reduction ', Journal of Automated Reasoning, vol. 60, no. 1, pp. 3-21 . https://doi.org/10.1007/s10817-017-9418-4 |
| ISSN: | 1573-0670 0168-7433 |
| Popis: | We present a formally verified and executable on-the-fly LTL model checker that uses ample set partial order reduction. The verification is done using the proof assistant Isabelle/HOL and covers everything from the abstract correctness proof down to the generated SML code. Building on Doron Peled’s paper “Combining Partial Order Reductions with On-the-Fly Model-Checking”, we formally prove abstract correctness of ample set partial order reduction. This theorem is independent of the actual reduction algorithm. We then verify a reduction algorithm for a simple but expressive fragment of Promela. We use static partial order reduction, which allows separating the partial order reduction and the model checking algorithms regarding both the correctness proof and the implementation. Thus, the Cava model checker that we verified in previous work can be used as a back end with only minimal changes. Finally, we generate executable SML code using a stepwise refinement approach. We test our model checker on some examples, observing the effectiveness of the partial order reduction algorithm. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink