Carnegie Mellon University
Browse

A Case Study on the Lightweight Verification of a Multi-Threaded Task Server

Download (324.09 kB)
journal contribution
posted on 2013-12-01, 00:00 authored by Nestor Catano, Ijaz Ahmed, Radu I. Siminiceanu, Jonathan Aldrich

We present a case study on the verification of the design of a commercial multi-threaded task server (MTTS), developed by the Novabase company, used for massively parallelizing computational tasks. In a first stage, we employed the Plural tool, which is designed to perform lightweight verification of Java programs using a data-flow analysis (DFA) framework, to specify and verify the MTTS. We wrote the Plural specification for the MTTS based on the code developed by Novabase, its informal documentation, and our discussions with Novabase engineers, who validated our understanding of the MTTS application. The Plural specification language is based on typestates and access permissions. In a second stage, we developed the Pulse tool, which enhances the analysis performed by Plural, and used the tool on the MTTS specifications. Pulse translates Plural specifications into an abstract state-machine model that captures the semantics of all the possible concurrent programs implementing the given specifications, and uses the evmdd-smc symbolic model checker to verify the machine model. The experimental results on the MTTS specification show that the exhaustive model-checking approach scales reasonably well and is efficient at finding errors in specifications that were not previously detected with the data-flow analysis (DFA) capabilities of Plural.

History

Publisher Statement

This is the author’s version of a work that was accepted for publication. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version is available at http://dx.doi.org/10.1016/j.scico.2013.01.004

Date

2013-12-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC