Automated Logical Verification based on Trace Abstractions

Forfattere

  • Nils Klarlund
  • Mogens Nielsen
  • Kim Sunesen

DOI:

https://doi.org/10.7146/brics.v2i53.19954

Resumé

We propose a new and practical framework for integrating the behavioral
reasoning about distributed systems with model-checking methods.
Our proof methods are based on trace abstractions, which relate the
behaviors of the program and the specification. We show that for finite-state
systems such symbolic abstractions can be specified conveniently in
Monadic Second-Order Logic (M2L). Model-checking is then made possible
by the reduction of non-determinism implied by the trace abstraction.
Our method has been applied to a recent verification problem by Broy
and Lamport. We have transcribed their behavioral description of a distributed
program into temporal logic and verified it against another distributed
system without constructing the global program state space. The
reasoning is expressed entirely within M2L and is carried out by a decision
procedure. Thus M2L is a practical vehicle for handling complex temporal
logic specifications, where formulas decided by a push of a button are as
long as 10-15 pages.

Downloads

Publiceret

1995-11-23

Citation/Eksport

Klarlund, N., Nielsen, M., & Sunesen, K. (1995). Automated Logical Verification based on Trace Abstractions. BRICS Report Series, 2(53). https://doi.org/10.7146/brics.v2i53.19954

Nummer

Nr. 53 (1995): RS-53 Automated Logical Verification based on Trace Abstractions

Sektion

Artikler

Licens

Authors who publish with this journal agree to the following terms:

    1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.

    1. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.

  1. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).