Entry Jonsson:1994:CSV 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{Jonsson:1994:CSV,
  author =       "Bengt Jonsson",
  title =        "Compositional Specification and Verification of
                 Distributed Systems",
  journal =      j-TOPLAS,
  volume =       "16",
  number =       "2",
  pages =        "259--303",
  month =        mar,
  year =         "1994",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Fri Jan 5 07:58:42 MST 1996",
  bibsource =    "Compiler/TOPLAS.bib;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org/pubs/toc/Abstracts/0164-0925/174665.html",
  abstract =     "We present a method for specification and verification
                 of distributed systems that communicate via
                 asynchronous message passing. The method handles both
                 safety and liveness properties. It is compositional,
                 i.e., a specification of a composite system can be
                 obtained from specifications of its components.
                 Specifications are given as labeled transition systems
                 with fairness properties, using a program-like notation
                 with guarded multiple assignments. Compositionality is
                 attained by partitioning the labels of a transition
                 system into input events, which intuitively denote
                 message receptions, and output events, which
                 intuitively denote message transmissions. A
                 specification denotes a set of allowed sequences of
                 message transmissions and receptions, in analogy with
                 the way finite automata are used as acceptors of finite
                 strings. A lower-level specification implements a
                 higher-level one. We present a verification technique
                 which reduces the problem of verifying the correctness
                 of an implementation to classical verification
                 conditions. Safety properties are verified by
                 establishing a simulation relation between transition
                 systems. Liveness properties are verified using methods
                 for proving termination under fairness assumptions.
                 Since specifications can be given at various levels of
                 abstraction, the method is suitable in a development
                 process where a detailed implementation is developed
                 from an abstract specification through a sequence of
                 refinement steps. As an application of the method, an
                 algorithm by Thomas for updating a distributed database
                 is specified and verified.",
  acknowledgement = ack-nhfb # " and " # ack-pb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  keywords =     "theory; verification",
  subject =      "{\bf F.3.1}: Theory of Computation, LOGICS AND
                 MEANINGS OF PROGRAMS, Specifying and Verifying and
                 Reasoning about Programs, Specification techniques.
                 {\bf C.2.2}: Computer Systems Organization,
                 COMPUTER-COMMUNICATION NETWORKS, Network Protocols,
                 Protocol verification. {\bf D.2.1}: Software, SOFTWARE
                 ENGINEERING, Requirements/Specifications,
                 Methodologies. {\bf D.2.2}: Software, SOFTWARE
                 ENGINEERING, Tools and Techniques, Modules and
                 interfaces. {\bf D.2.4}: Software, SOFTWARE
                 ENGINEERING, Program Verification, Correctness
                 proofs.",
}

Related entries