Transcript Eliciting Formal Models From Informal Requirements

Eliciting Formal Models From
Informal Requirements
Some issues and an approach.
Nikhil Dinesh, David E. Arney, Aravind K. Joshi,
Owen Rambow, Martha Palmer and Insup Lee
University of Pennsylvania
Chicago, September 24 2003
Sep 2003, Chicago,1
Outline
•
•
•
•
•
Introduction
Example
Specification Language for Requirements
The approach
Future work
Sep 2003, Chicago,2
Issues
• What is the right specification language for
requirements ?
– Natural Language
– Formal Specification Language
– Formal Specification Language with an NLlooking restricted language interface
• Evaluation
– What metrics can be applied in the evaluation
of such a system
Sep 2003, Chicago,3
Overall Approach
NL requirements
NL-based Finite State Machine
Requirements
Engineer
Corrections to requirements
in NL
Policy
Specifier
Extended Finite State Machine
Verification
& Validation
Errors
Sep 2003, Chicago,4
Approach to elicit an EFSM*
• Work is preliminary, no implementation
• Outline the stages in eliciting an EFSM
– Desired output representation at each stage
– How to compute from the NL requirements in
terms of :
• What is available
• What is needed
– What is achievable with existing tools and
what research is needed for the long range
*An Extended Finite State Machine is an FSM with variables. (as in the
HASTEN project)
Sep 2003, Chicago,5
Outline
•
•
•
•
•
Introduction
Example
Specification Language for Requirements
The approach
Future work
Sep 2003, Chicago,6
Example from FDA CFR* 610.40
(a) Except as specified in paragraphs (c) and (d) of this section,
you must test all samples for evidence of infection due to the
following communicable disease agents:
(i) Human immunodeficiency virus
(ii) Hepatitis-B virus
* A policy document from Food and Drug Administration, Code of
Federal Regulations. There are several volumes each of which is
updated once each calendar year and issued on a quarterly basis.
Sep 2003, Chicago,7
Example from FDA CFR 610.40
(a) Except as specified in paragraphs (c) and (d) of this section,
you must test all samples for evidence of infection due to the
following communicable disease agents:
(i) Human immunodeficiency virus
(ii) Hepatitis-B virus
(b) To test for evidence of infection due to communicable disease
agents in paragraph (a), you must use a screening test
approved by the FDA.
Sep 2003, Chicago,8
Example from FDA CFR 610.40
(a) Except as specified in paragraphs (c) and (d) of this section,
you must test all samples for evidence of infection due to the
following communicable disease agents:
(i) Human immunodeficiency virus
(ii) Hepatitis-B virus
(b) To test for evidence of infection due to communicable disease
agents in paragraph (a), you must use a screening test
approved by the FDA. You must perform one or more such test,
as necessary, to reduce adequately and appropriately the risk of
transmission of communicable disease.
Sep 2003, Chicago,9
Outline
•
•
•
•
•
Goals
Example
Specification Language for requirements
The approach
Future work
Sep 2003, Chicago,10
Specification Language for
Requirements
• Natural Language (NL)
– Specification is accessible to people
– Properties should correspond to the requirements
– Hard to compute properties
• Formal Specification Language (FSL)
– Allows specification to be easily verified
– Not easily accessible to people such as policy users
• Application should motivate the choice
– What is the right choice for the policy domain ?
Sep 2003, Chicago,11
Policy
• Large number of policy documents in NL
– Hand conversion to FSL is expensive and
error prone.
• Human readability
– Policy is interpreted by humans.
• Is this just an interface problem ?
Sep 2003, Chicago,12
Interfaces to Specification
Languages
• Suppose policy requirements were in a
formal specification language
• Interface provides NL-looking, restricted
language
• How easily can it be read?
• We examine one such interface
Sep 2003, Chicago,13
Specifying a Property
• PROPEL – An approach supporting property
elucidation [Smith et al], 2002.
• For our example,
– Core phrase : Exactly one occurrence of arrival of a
sample eventually leads to one or more occurrences
of test for diseases.
– Repetition Phrase : The above behavior is repeatable
– Scope Phrase : This property must hold before the
first occurrence of P (where P is a state
corresponding to “Exceptions in paragraphs (c) and
(d)”)
Sep 2003, Chicago,14
How do properties relate to the NL document ?
• Core phrase : Exactly one
occurrence of arrival of a sample
eventually leads to one or more
disease
occurrences of test Test
forfordiseases
• Repetition Phrase : The above
behavior is repeatable
• Scope Phrase : This property must
in (c) and (d) of
hold before theExceptions
first occurrence
P
Sentence 1
Sep 2003, Chicago,15
How do properties relate to the NL document ?
• Core phrase : Exactly one
occurrence of arrival of a sample
One oror
more
tests
eventually leads to one
more
occurrences of test for diseases
• Repetition Phrase : The above
behavior is repeatable
• Scope Phrase : This property must
hold before the first occurrence of
P
Sentence 3
Sep 2003, Chicago,16
How do properties relate to the NL document ?
• Core phrase : Exactly one
Arrival
occurrence of arrival
ofofaa sample
sample
eventually leads to one or more
occurrences of test for diseases
• Repetition Phrase : The above
Repeatability
behavior is repeatable
• Scope Phrase : This property must
hold before the first occurrence of
P
?
Sep 2003, Chicago,17
How do properties relate to the NL document ?
• To enforce use of a screening test:
– test for disease -> screening test for disease
• “test for disease” from Sentence 1
• “screening” from Sentence 2
• Correspondence becomes harder
• Interface starts to look like an FSL
• Not easily accessible to policy users
Sep 2003, Chicago,18
Outline
•
•
•
•
•
Goals
Example
Specification Language for requirements
The approach
Future work
Sep 2003, Chicago,19
NL Document
NLFSM
EFSM
EFSM-like
representation
from NL document
Sep 2003, Chicago,20
NLFSM
Agree to perform test
Agree to use screening test
Do the test
Have you tested ?
Have you reduced risk?
Sep 2003, Chicago,21
NLFSM to EFSM
Clause a
true
V(a)
V(a) == true
Clause b
Sep 2003, Chicago,22
EFSM
Sep 2003, Chicago,23
NL Document
Clause Connective
Dependency Structure
NLFSM
Temporal Ordering
Of Clauses
EFSM
Sep 2003, Chicago,24
Clauses and Connectives
as specified
in paragraphs
(c) and(c)
(d) and
of this
(a) Except
as specified
in paragraphs
(d)section
of this section,
you must test all samples for evidence of infection due to the
following communicable disease agents:
Explicit Connective
Clauses
Except
(i) Human immunodeficiency Connective virus
(ii) Hepatitis-B virus
you must test all samples for evidence of infection
due to the following communicable disease agents :
(i) Human immunodeficiency (ii) Hepatitis-B virus
Sep 2003, Chicago,25
Clauses and Connectives
Totest
test for evidence
disease
agents
in (a)in
(b) To
evidenceofofcommunicable
communicable
disease
agents
paragraph (a), you must use a screening test approved by the
FDA.
Implicit Connective
In
Clauses
order to
You must use a screening test approved by the FDA
Sep 2003, Chicago,26
Predicates and Arguments
John ate the apple
Predicate: ate(Agent,Object)
ate
Dependency
Structure
(Agent)
(Object)
John
The apple
Sep 2003, Chicago,27
Arguments of Connectives
• Except
– Exception
– Default
Sep 2003, Chicago,28
Arguments of Connectives
• In order to
– Action
– Purpose
Sep 2003, Chicago,29
Arguments of Connectives
• In order to
– Action
– Purpose
Sep 2003, Chicago,30
Arguments across sentences
• If X is true do action A. Otherwise do
action B.
Otherwise
(Condition)
(Action)
X is true
Do action B
Sep 2003, Chicago,31
Computing the Dependency
Structure
• Discourse Connectives vs Verbs
– arity, Verbs (1 – 3), Connectives (2)
– Locating the arguments, easier for verbs
– Roles of the arguments, verb-specific
(Propbank), connective-specific (our
approach)
Sep 2003, Chicago,32
Computing the Dependency
Structure
• Chunking
– [Except] [as specified in paragraphs (c) and (d) of this
section] [you must test all samples for evidence of
infection due to the communicable disease agents:
(1) Human immunodeficiency virus (2) Hepatitis B
virus]
• Simple for the cases where there is only one
connective in the sentence.
Sep 2003, Chicago,33
Computing the Dependency
Structure
• You should test donation for evidence of all
disease, except if it is a dedicated donation,
you need not test for diseases (a)(5) and
(a)(6).
Sep 2003, Chicago,34
Computing the Dependency
Structure
• Three Generative, Lexicalized Models for Statistical
Parsing, Michael Collins, Proceedings of the 35th
Annual Meeting of the ACL, Madrid (1997)
• Statistical Parsing with an automatically-extracted tree
adjoining grammar, David Chiang, Proceedings of the
ACL, Hong Kong (2000)
• Discriminative Reranking for Natural Language Parsing,
Michael Collins, ICML (2000)
Sep 2003, Chicago,35
Computing the Dependency
Structure
• Resources available
– Parsers compute rich dependency structure at
the sentence-level
– Accuracy of approximately 90% (Collins 2000)
– Efforts underway for parsers at the discourselevel (DLTAG, Discourse Treebank)
• Resources required
– Some annotation of requirements documents
– Labeling of connective-specific roles
Sep 2003, Chicago,36
NL Document
Clause Connective
Dependency Structure
NLFSM
Temporal Ordering
Of Clauses
EFSM
Sep 2003, Chicago,37
Temporal Ordering of Clauses
• Related to programs
• Cannot impose an order from an
operational perspective (there may be
cycles)
• But can an order be imposed from a
syntactic perspective – the way we write
programs ?
Sep 2003, Chicago,38
Temporal Ordering of Clauses
while(i < 9)
while(i < 9){
True i = i + 1; False
}
i = i – 1;
i=i+1
i=i-1
Temporal Tree
i<9
False
True
i=i+1
True
i=i-1
Operational FSM
Sep 2003, Chicago,39
Computing the Temporal Ordering
(Between Clauses in a Sentence)
Exception before the Default
Sep 2003, Chicago,40
Computing the Temporal Ordering
(Between Clauses in a Sentence)
Action before the check for Purpose
Sep 2003, Chicago,41
Computing the Temporal Ordering
(Between Clauses in a Sentence)
Action before the check for Purpose
Sep 2003, Chicago,42
Computing the Temporal Ordering
(Between Clauses in Different Sentences)
Agreement to use a screening test precedes agreement to test
Noun-Verb “link” through the light verb (use)
Check that test has taken place should follow the test
Finite Verb – Nonfinite Verb “link”
Sep 2003, Chicago,43
Computing the Temporal Ordering
(Between Clauses in Different Sentences)
Sep 2003, Chicago,44
Computing the Temporal Ordering
“tests”
“screeningSentences)
tests” are related.
(Between Clauses
in and
Different
But the order is not quite clear from these in
isolation. However these clauses are both
scoped by purpose clauses
reduce follows test
Desirable to keep scopes
Sep 2003, Chicago,45
nested.
Sep 2003, Chicago,46
Computing the Temporal Ordering
• Resources available
– Work on noun coreference (Morton)
– New Machine Learning algorithms (Maximum
Entropy Models, Conditional Random Fields
etc)
• Research needed
– Granularity of annotation
– Incorporating world knowledge
Sep 2003, Chicago,47
NL Document
Clause Connective
Dependency Structure
NLFSM
Temporal Ordering
Of Clauses
EFSM
Sep 2003, Chicago,48
From Temporal Trees to NLFSM
• Find the phrases/connectives indicative of
iterative constructs
– while, for (connectives)
– “one or more” (phrases)
• Identify the scope and add the back-edges
in the temporal tree.
• Scope given by purpose clauses or
relations between verbs
Sep 2003, Chicago,49
Sep 2003, Chicago,50
Outline
•
•
•
•
•
Goals
Example
Specification Language for requirements
The approach
Future work
Sep 2003, Chicago,51
Future Work: NLP
• Extending and adapting ongoing NLP work
– Discourse Structure
– Discourse Connectives
– Temporal relations between clauses
• Adapt existing tools
– Parsers
– Chunkers
– Shallow semantic parsers
Sep 2003, Chicago,52
Future Work: Verification
• Completeness
– NL documents are usually underspecified
– Harmless vs. Harmful underspecification
• Harmless – What happens if an FDA-approved screening
test cannot be used ?
• Harmful – What happens if you cannot do the test ? (because
in repeated testing one might run out of a sample)
– Relations between connectives
• “if” without a corresponding “else” or “otherwise”
– Some domain specific way ?
Sep 2003, Chicago,53
Future Work: Verification
• Consistency
– Relations between variables preventing certain
transitions from being taken
• A donation shipped prior to testing cannot have been tested
– Requires lexical knowledge and/or world knowledge
• A shipped donation is not longer in the possession of the
establishment
• Safety
– Check if the system behaves as intended
• A sample of blood should not be shipped before testing
unless in the case of dire emergencies
– Associating this statement with ones in the document
Sep 2003, Chicago,54
Future Work: Evaluation
Evaluation
– Corpus-based evaluation of NLP techniques
– Comparison with models from other systems
– Experts evaluation of the models generated
Sep 2003, Chicago,55
NP
D
N
the
end
Sep 2003, Chicago,56