kirancodes.me
To Proof Maintenance & Beyond!
ICSE 1992

Graphical Specifications for Concurrent Software Systems

Laura K. Dillon, George Kutty, Louise E. Moser, P. M. Melliar-Smith, Y. S. Ramakrishna

PDFDOI 10.1145/143062.143116dblp

Abstract

We present a description of a graphical interval logic that is the foundation of a toolset we are developing to support formal specification and verification of concurrent software systems. Experience has shown that most software engineers find standard temporal logics difficult to under- stand and to use. Our objective is to enable software engineers to specify and reason about temporal properties of concurrent systems more easily by providing them with a logic that has an intuitive graphical representation and with tools that support its use. To illustrate the use of our graphical interval logic, we provide a specification for a readers/writers database system and prove several properties of the specification.

BibTeX
@inproceedings{Dillon-al:ICSE92,
  author    = {Laura K. Dillon and
               George Kutty and
               Louise E. Moser and
               P. M. Melliar{-}Smith and
               Y. S. Ramakrishna},
  title     = {Graphical Specifications for Concurrent Software Systems},
  booktitle = {ICSE},
  pages     = {214--224},
  publisher = {{ACM}},
  year      = {1992},
}

Related papers