kirancodes.me
To Proof Maintenance & Beyond!

Complementing semi-formal specifications with Z

Yves Ledru

Abstract

The insertion of formal techniques into the daily practice of software engineering definitely improves the quality of specifications. An approach is proposed where semi-formal specifications are translated into the formal specification language Z and enriched by formal annotations. The paper starts from a specification of an access control system using classical description techniques: entity-relationship schemas, data-flow diagrams, and state machine descriptions. It shows how these can be combined with formal definitions of types, constraints and functions.

BibTeX
@inproceedings{Ledru:ASE96,
  author    = {Yves Ledru},
  title     = {Complementing semi-formal specifications with Z},
  booktitle = {ASE},
  pages     = {52--61},
  publisher = {{IEEE} Computer Society},
  year      = {1996},
}

Related papers