kirancodes.me
To Proof Maintenance & Beyond!
ASE 2001

Composition and Refinement of Behavioral Specifications

Dusko Pavlovic, Douglas R. Smith

DOI 10.1109/ase.2001.989801dblp

Abstract

This paper presents a mechanizable framework for specifying, developing, and reasoning about complex systems. The framework combines features from algebraic specifications, abstract state machines, and refinement calculus, all couched in a categorical setting. In particular, we show how to extend algebraic specifications to evolving specifications (especs) in such a way that composition and refinement operations extend to capture the dynamics of evolving, adaptive, and self-adaptive software development, while remaining efficiently computable. The framework is partially implemented in the Epoxi system.

BibTeX
@inproceedings{Pavlovic-Smith:ASE01,
  author    = {Dusko Pavlovic and
               Douglas R. Smith},
  title     = {Composition and Refinement of Behavioral Specifications},
  booktitle = {ASE},
  pages     = {157--165},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Related papers