1999 | OriginalPaper | Buchkapitel
Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes
verfasst von : Farn Wang
Erschienen in: FM’99 — Formal Methods
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Real-world concurrent software may be implemented with any number of processes which are linked together to form complex and dynamic network cofigurations. We formally model such concurrent software as processes running algorithms on data-structures with pointers. We show that the verification problem of such algorithms is undecidable. A new automatic approximation method is then proposed to safely verify such algorithms. The central idea is to construct a finite collective image set (CIS) which collapses reachable state representations for all implementations of all numbers of processes. Our collapsing scheme filters out unimportant information of system behaviors and results in CIS’s with manageable space requirements. Analysis shows our method can automatically generate a CIS of size 1619 to verify that a version of Mellor-Crummy & Scott’s algorithm preserves mutual exclusion for all numbers of processes.