Accession Number:

ADA465305

Title:

Analysis of Agent-Based Systems Using Decision Procedures

Descriptive Note:

Research paper

Corporate Author:

NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)

Personal Author(s):

Report Date:

2001-07-01

Pagination or Media Count:

3.0

Abstract:

In recent years, model checking has emerged as a remarkably effective technique for the automated analysis of descriptions of hardware systems and communication protocols. To analyze software system descriptions, however, a direct application of model checking rarely succeeds, since these descriptions often have huge often infinite state spaces that are not amenable to the finite-state methods of model checking. More important, the computation of a fixpoint the hallmark of the model-checking approach is not always needed in practice for the verification of an interesting class of properties, viz, properties that are invariantly true in all reachable states or transitions of the system. To establish a property as an invariant, an induction proof, suitably augmented with automatically generated lemmas, often suffices.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE