The Use of Machine Learning in the Validation of a Formal Requirements Specification: the work of IMPRESS
A previous project, FAROAS, established a formal requirements specification for the control of aircraft flying in the eastern half of the North Atlantic. The requirements, written in Many Sorted First Order Logic, are held in a tools environment supporting validation in 5 key ways: full grammatical...
Main Authors: | , , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
1996
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8309 |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.45.8309 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.45.8309 2023-05-15T17:32:52+02:00 The Use of Machine Learning in the Validation of a Formal Requirements Specification: the work of IMPRESS M. M. West T. L. Mccluskey J. M. Porteous The Pennsylvania State University CiteSeerX Archives 1996 application/postscript http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8309 en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8309 Metadata may be used without restrictions as long as the oai identifier remains attached to it. ftp://helios.hud.ac.uk/pub/scommmw/re97.ps text 1996 ftciteseerx 2016-01-08T05:49:16Z A previous project, FAROAS, established a formal requirements specification for the control of aircraft flying in the eastern half of the North Atlantic. The requirements, written in Many Sorted First Order Logic, are held in a tools environment supporting validation in 5 key ways: full grammatical checking, inspection by domain experts, formal reasoning about their properties, automatic generation of a prototype for use with a test harness for batch testing, and a graphical interface for animation. Each of these five validation strategies uncovered errors in the initial encoding of the requirements, and their use improved the accuracy of the model. Unfortunately our experience led us to believe that these diverse forms of validation were still insufficient as far as uncovering bugs and fixing bugs was concerned; for example, tests may succeed for the wrong reasons, and where tests fail (i.e the expert decision is at variance with the prototype 's decision) it is still very difficult t. Text North Atlantic Unknown |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
description |
A previous project, FAROAS, established a formal requirements specification for the control of aircraft flying in the eastern half of the North Atlantic. The requirements, written in Many Sorted First Order Logic, are held in a tools environment supporting validation in 5 key ways: full grammatical checking, inspection by domain experts, formal reasoning about their properties, automatic generation of a prototype for use with a test harness for batch testing, and a graphical interface for animation. Each of these five validation strategies uncovered errors in the initial encoding of the requirements, and their use improved the accuracy of the model. Unfortunately our experience led us to believe that these diverse forms of validation were still insufficient as far as uncovering bugs and fixing bugs was concerned; for example, tests may succeed for the wrong reasons, and where tests fail (i.e the expert decision is at variance with the prototype 's decision) it is still very difficult t. |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
M. M. West T. L. Mccluskey J. M. Porteous |
spellingShingle |
M. M. West T. L. Mccluskey J. M. Porteous The Use of Machine Learning in the Validation of a Formal Requirements Specification: the work of IMPRESS |
author_facet |
M. M. West T. L. Mccluskey J. M. Porteous |
author_sort |
M. M. West |
title |
The Use of Machine Learning in the Validation of a Formal Requirements Specification: the work of IMPRESS |
title_short |
The Use of Machine Learning in the Validation of a Formal Requirements Specification: the work of IMPRESS |
title_full |
The Use of Machine Learning in the Validation of a Formal Requirements Specification: the work of IMPRESS |
title_fullStr |
The Use of Machine Learning in the Validation of a Formal Requirements Specification: the work of IMPRESS |
title_full_unstemmed |
The Use of Machine Learning in the Validation of a Formal Requirements Specification: the work of IMPRESS |
title_sort |
use of machine learning in the validation of a formal requirements specification: the work of impress |
publishDate |
1996 |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8309 |
genre |
North Atlantic |
genre_facet |
North Atlantic |
op_source |
ftp://helios.hud.ac.uk/pub/scommmw/re97.ps |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8309 |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766131159993942016 |