Entry Juan:1998:CVC from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Juan:1998:CVC,
  author =       "Eric Y. T. Juan and Jeffrey J. P. Tsai and Tadao
                 Murata",
  title =        "Compositional Verification of Concurrent Systems Using
                 {Petri}-Net-Based Condensation Rules",
  journal =      j-TOPLAS,
  volume =       "20",
  number =       "5",
  pages =        "917--979",
  month =        sep,
  year =         "1998",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Mon Mar 1 10:04:11 MST 1999",
  bibsource =    "http://www.acm.org/pubs/toc/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org:80/pubs/citations/journals/toplas/1998-20-5/p917-juan/",
  abstract =     "The state-explosion problem of formal verification has
                 obstructed its application to large-scale software
                 systems. In this article, we introduce a set of new
                 condensation theories: IOT-failure equivalence,
                 IOT-state equivalence, and firing-dependence theory to
                 cope with this problem. Our condensation theories are
                 much weaker than current theories used for the
                 compositional verification of Petri nets. More
                 significantly, our new condensation theories can
                 eliminate the interleaved behaviors caused by
                 asynchronously sending actions. Therefore, our
                 technique provides a much more powerful means for the
                 compositional verification of asynchronous processes.
                 Our technique can efficiently analyze several
                 state-based properties: boundedness, reachable
                 markings, reachable submarkings, and deadlock states.
                 Based on the notion of our new theories, we develop a
                 set of condensation rules for efficient verification of
                 large-scale software systems. The experimental results
                 show a significant improvement in the analysis
                 large-scale concurrent systems.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  keywords =     "algorithms; experimentation; reliability; theory;
                 verification",
  subject =      "{\bf D.2.4} Software, SOFTWARE ENGINEERING,
                 Software/Program Verification, Programming by contract.
                 {\bf F.3.1} Theory of Computation, LOGICS AND MEANINGS
                 OF PROGRAMS, Specifying and Verifying and Reasoning
                 about Programs, Mechanical verification.",
}

Related entries