We describe a tools environment which automates the validation and maintenance of a requirements model written in many-sorted first order logic. We focus on a translator that produces an executable form of the model; blame assignment functions, which input batches of mis-classified tests (i.e. training examples) and output likely faulty parts of the model; and a theory reviser; which inputs the faulty parts and examples and outputs suggested revisions to the model. In particular we concentrate on the problems encountered when applying these tools to a real application: a requirements model containing air traffic control separation standards, operating methods and airspace information.
The different versions of the original document can be found in:
Published on 01/01/2002
Volume 2002, 2002
DOI: 10.1109/ase.1998.732591
Licence: CC BY-NC-SA license
Are you one of the authors of this document?