PPT – Requirements Validation PowerPoint presentation | free to download – id: 12fbf3-NDQwY
1
Requirements Validation
Requirements Management
Requirements Validation
2
?? Validation, Verification, Accreditation !!
- Check if evrything is OK
- With respect to what ?
- Mesurement associated with requirements
- Dont get lost with terminology problem
- Some definitions
- IEEE SRS
- EIA-632
build the Right System Build It Right
3
Content
- What the standards say
- Techniques and methods
- Well established techniques
- Case study
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
4
What the standard say (EIA632)
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
5
What the standard say (EIA632)
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
6
What the standard say (EIA632)
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
7
Validation
- Requirements Validation is critical to successful
system product development and implementation.
Requirements are validated when it is certain
that the subject set of requirements describes
the input requirements and objectives such that
the resulting system products can satisfy the
requirements and objectives. - The Requirements Validation Process helps ensure
that the requirements are necessary and
sufficient for creating design solutions
appropriate to meeting the exit criteria of the
applicable engineering life cycle phase and of
the enterprise-based life cycle phase in which
the engineering or reengineering efforts occur.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
8
Requirement 25Requirement Statements Validation
- The developer shall ensure that technical
requirement statements and specified requirement
statements, individually and as sets, are well
formulated.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
9
Requirement 26Acquirer Requirements Validation
- The developer shall ensure that the set of
defined acquirer requirements agrees with
acquirer needs and expectations.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
10
Requirement 27Other Stakeholder Requirements
Validation
- The developer shall ensure that the set of
defined other stakeholder requirements agrees
with other stakeholder needs and expectations
with respect to the system.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
11
Requirement 28System Technical Requirements
Validation
- The developer shall ensure that the set of
defined system technical requirements agrees with
the validated acquirer and other stakeholder
requirements.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
12
Requirement 29Logical Solution Representations
Validation
- The developer shall ensure that each set of
logical solution representations agrees with the
appropriately assigned subset of system technical
requirements.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
13
System Verification
- The System Verification Process is used to
ascertain that - the system design solution generated by
implementing Requirement 19 is consistent with
its source requirements (selected preferred
physical solution representation) - end products at each level of the system
structure implementation, from the bottom upmeet
their specified requirements - enabling product development or procurement for
each associated process is properly progressing
and - required enabling products will be ready and
available when needed to perform.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
14
Requirement 30Design Solution Verification
- The developer shall verify that each end product
defined by the system design solution conforms to
the requirements of the selected physical
solution representation.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
15
Requirement 31End Product Verification
- The developer shall verify that an end product to
be delivered to an acquirer conforms to its
specified requirements.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
16
Requirement 32Enabling Product Readiness
- The developer shall determine readiness of
enabling products for development, production,
test, deployment/installation, training,
support/maintenance, and retirement or disposal.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
17
Requirement 33End Products Validation
- The developer shall ensure that an end product,
or an aggregation of end products, conforms to
its validated acquirer requirements.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
18
(No Transcript)
19
What the standards say ()
- Main standards
- IEEE P1220
- EIA 632
- DoD 2167A
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
20
Correctness and completeness
- A correct, complete set of requirements is one
that correctly and completely states the desires
and needs of the sponsor. - If the requirements are incorrect, the software
may meet the requirements as stated, but will not
do what the sponsor wants it to do. - If the requirements are incomplete, the software
may do only part of what the sponsor hoped it
would do.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
21
Consistent
- Consistency is obtained if the requirements do
not contradict each other. - Inconsistency results when one requirement
contradicts another.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
22
Unambiguous
- If a requirement is subject to more than one
interpretation, it is ambiguous. - Requirements should be stated simply and
completely so that they are unambiguous.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
23
Functional
- Requirements should state what the sponsor
desires the functions and activities to be
performed by the system. - They should not state how the problem is to be
solved or what techniques are to be used. - Such decisions should be left to the system
designers.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
24
Verifiable
- The requirements must be verifiable in two ways
do the requirements satisfy the sponsor’s needs
? - does the system satisfy the requirements?
- In the first case, the requirements must be
compared to the sponsor’s desires and needs. Do
the requirements correctly and completely specify
the sponsor’s desires and needs? - In the second case, once the system has been
developed, it must be compared to the
requirements. Does the system meet the
requirements as they are stated?
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
25
Traceability
- Traceable and easily changed.
- The requirements should be organized and written
in a segmented, top down manner that allows for
easy use (traceability) and easy modification. - A numbering system is useful to label the
paragraphs and parts of the manual for cross
referencing, indexing, and easy modification
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
26
Techniques and methods
- Inspection
- Model Checking
- Simulation
- Prototyping
- Others
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
27
Inspection
- Most common simple et pragmatic method and can be
- Manual Human sense principal instrument
- Automatic (CAI tool) for measurable issues
- Most evident errors/faults can be detected
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
28
Inspection (example)
- This presentation shows how to carry out a
one-half hour inspection with senior managers.
The purpose is to show to make managers aware
that they play a key-role in creating project
delays by approving poor quality of requirements
documents. - The inspection results shown in this real-life
example successfully predicted a project delay of
2 calendar years. - Poor quality marketing requirements documents
prove time and again to be a good predictor of
project delays. - The clue is that requirements documents with a
high defect density are an indicator of a truly
unprofessional engineering culture.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
29
Inspection (example)
Rules
Introduce the following three rules for
inspecting a requirements document
- Three Rules for Requirements
- 1. Unambiguous to intended Readership
- 2. Clear enough to test.
- 3. No Design (how to) mixed in
- with Requirements (how well)
- MARK Design as D
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
30
Inspection (example)
Defect
Explain the definition of a Defect
- A Defect is a violation of a Rule
- Note If there are 10 ambiguous terms in a single
requirement then there are 10 defects!
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
31
Inspection (example)
Severity
- Explain
- the definition of Major Defect
- the checkers must focus on finding Major Defects
- Major a defect severity where there is potential
of - high (x lost engineering hours) loss
- later downstream (test, field).
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
32
Inspection (example)
Exit?
Agree with the management team on a numeric exit
condition
- Exit Conditions (Requirements can go to Design,
Test etc with little risk) - Maximum 1 Major Defect/ (Logical) Page
- Logical Page 300 Non commentary words.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
33
Inspection (example)
- The Job
- You have up to 30 minutes for checking One
requirements Logical page from an 82 pages
document - Count all Rule Violations Defects
- Classify Major and minor
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
34
Inspection (example)
- Page 81 120 majors/p
- Page 82 180 Majors/p
- Average 150 Majors/page x 82 page 12,300
Majors in the document. - —————–
- If a Major has 1/3 chance of causing loss
- And each loss is avg 10 hours then total project
Rework cost is about 41,000 hours loss. - (This project was over a year late)
- 1 year 2,000 hour 10 people
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
35
Inspection (example)
Letter to Your Boss
- Boss!
- We have 2 options for the 82 page Requirements
document. - Our sample shows that we have 180 Majors/Page.
- We can spend 180 hours per page removing them
with Inspection - We can rewrite the pages at a cost of 10hours
each. - Or we can suffer 30 of these as bugs and fault,
at an average removal cost of about 10 hours each
(test and field debugging and re-testing), 1/3 of
180 x 10 600 hours per page if we do not
rewrite (10 hours /Page) or remove before test
(180 hours/Pages). - We suggest rewrite (changing something to avoid
defect injection rate). But you have said you are
against this. So we have to tell you that your
option will delay our project by 600 hours x 82
49,200 hours. - Our project has 10 people on it, and they can do
about 2,000 hours per year. So that is 20,000
work hours per year for our team. The approximate
delay for your decision not to rewrite is this
about 2.5 years worse Time To Market. - We will of course do what you say, but we wanted
to be sure that you understood what your boss
will blame you for later. - Your Loyal Servant, Tom
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
36
Simulation
- Abstract model of either requirements or the
design solution - Coverage of most scenarios
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
37
Model Checking
- Model checking is a method for formally verifying
finite-state concurrent systems - Specifications about the system are expressed as
temporal logic formulas, and efficient symbolic
algorithms are used to traverse the model defined
by the system and check if the specification
holds or not - Extremely large state-spaces can often be
traversed in minutes - The technique has been applied to several complex
industrial systems - Site http//archive.comlab.ox.ac.uk/formal-meth
ods.html
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
38
Model Checking and Formality
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
39
Model Checking and Formality
- Models of a System
- Physical Prototypes Abstractions
- Representations (Working Models)
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
40
Model Checking and Formality
- A mathematical model is an abstract
representation of a system employing mathematical
entities and concepts - Model should be expressive enough to capture the
essential characteristics of the system being
modeled - If the model is intended for deductive reasoning
about the underlying system, it should provide
sufficient analytic power for this purpose
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
41
Model Checking and Formality
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
42
Model Checking and Formality
- Model is more concise and precise than natural
language, pseudo-code, and diagrammatic
representations - Model can be used to calculate and predict system
behavior - Model can be analyzed using mathematical
reasoning — proving properties, deriving new
behaviors, etc.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
43
Model Checking and Formality
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
44
Model Checking and Formality
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
45
Model Checking and Formality
A Simple String Parser Given an input string of
0s and 1s, determine if the string starts and
ends with a 1.
0
0
1
State Transition Function
S1
1
1
current state
S2
start
S0 S1 S2 D
S0
input
0
accept state
0
D S1 S1 D
D
S1 S2 S2 D
1
0, 1
dead state
next state
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
46
Formality
Formal analysis refers to tool-based techniques
used to explore, debug, and verify formal
specifications.
- Methods for Formal Analysis
- Theorem Proof Model Animation
- Proving Checking Checking
Simulation
our focus here
L 5
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
47
Formality-Properties
- Consistent — means it is not possible to derive
a statement and its negation within the system - Complete — means every true statement within the
system is provable - Decidable — means there is an effective
algorithm (e.g. computer program) for determining
whether any statement formed within the system is
true - A system must be consistent to be useable in
formal methods (or any other area). While
decidability and completeness would be nice,
these can not be achieved in most interesting
formal systems. However, this does not prevent
the effective use of these systems.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
48
Formality
- A sequent is written G – D, which means /\ G
implies \/ D, where G is a (possibly empty) list
of formulas A1, , An and D is a (possibly
empty) list of formulas B1, , Bn - the formulas in G are called the antecedents
- the formulas in D are called the succedents or
consequents - To restate, G – D means
- A1 /\ /\ An implies B1 \/ \/ Bn
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
49
Formality
- A sequent calculus proof is a tree of sequents
whose root is a sequent of the form – T where T
is the formula to be proved and the antecedent is
empty - The proof tree is then generated by applying
inference rules of the form - G1 – D1 Gn – Dn
- G – D
- Intuitively, this rule replaces a leaf node in
the proof tree of form G – D with the n new
leaves specified in the rule. If n is zero, that
branch of the proof tree terminates.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
50
Formality
- The Propositional Axiom (Prop_Axiom) is one of
the rules of inference in the sequent calculus.
It has the following form form - (G, A) – (A, D)
- Intuitively, this rule indicates that a proof
branch is complete when the sequent above is
derived. Note that the consequent means the
following - G /\ A implies A \/ D
- which is obviously true.
Prop_Axiom
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
51
Formality
- The Rule for Conjunction on the Right (And_Right)
is another of the rules of inference in the
sequent calculus. It has the following form - G – A, D G – B, D
- G – (A /\ B, D)
- This rule is typical of many sequent calculus
inference rules which divide, but simplify, a
branch of the proof tree. Note that the
consequent is replaced by two simpler formulas
which will be easier for a mechanized theorem
prover to deal with.
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
52
Formality
- The Rule for Conjunction on the Left (And_Left)
is another of the rules of inference in the
sequent calculus. It has the following simple
(non-branching) form - A, B, G – D
- (A /\ B, G) – D
- This rule is typical of several sequent calculus
inference rules which simply restate the
obvious, thereby providing a form easier for a
mechanized theorem prover to deal with.
And_Left
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
53
Formality
- The Rule for Implication on the Left
(Implies_Left) is another of the rules of
inference in the sequent calculus. It has the
following form - G – A, D B, G – D
- (A gt B, G) – D
- Similar to the And_Right rule, this rule again
splits the proof into two cases, each of which
will be easier for the mechanical prover to deal
with.
Implies_Left
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
54
Formality
- The Rule for Implication on the Right
(Implies_Right) is another of the rules of
inference in the sequent calculus. It has the
following form - G, A – B, D
- G – (A gt B, D)
- This rule does not branch, but provides a form
easier for a mechanized theorem prover to deal
with.
Implies_Right
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
55
Formality
- The following example proof in the sequent
calculus (taken from NASA Guidebook
NASA-GB-001-97, Release 1.0, pp. 97-101) will use
only the five sequent calculus inference rules we
define earlier — Prop_Axiom, And_Left,
And_Right, Implies_Left, and Implies_Right. - The theorem (assumed to be named Theorem 1) to
be proved is the following
Theorem 1 (P gt (Q gt R)) gt ((P /\
Q) gt R)
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
56
Formality
Theorem 1 (P gt (Q gt R)) gt ((P /\
Q) gt R)
We begin the proof by forming the requisite
sequent
Antecedents none Consequents Formula 1 (P
gt (Q gt R)) gt ((P /\ Q) gt R)
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
57
Formality
As our first step we apply the rule
Implies_Right. This rule will decompose the
entire formula. Remember there is an implied
implies in the sequent. In other words this
sequent could be written – (P gt (Q gt R)) gt
((P /\ Q) gt R). Hence, the implies we apply
the rule to is the outside implies on the right
of the sequent
Antecedents Formula 1 P gt (Q gt R)
Consequents Formula 1 (P /\ Q) gt R
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
58
Formality
A second application of the rule Implies_Right
will decompose the formula below the line in a
similar way. Remember that rules applying to the
left part of the sequent work on formulas above
the bar rules applying to the right part of
the sequent work below the bar.
Antecedents Formula 1 P gt (Q gt
R) Formula 2 P /\ Q Consequents Formula 1
R
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
59
Formality
We next apply the rule And_Left — this rule will
modify (rewrite) Formula 2 above the line.
Remember that all formulas above the line are
connected by ANDs formulas below the line are
connected by ORs.
Antecedents Formula 1 P gt (Q gt
R) Formula 2 P Formula 3
Q Consequents Formula 1 R
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
60
Formality
We next apply the rule Implies_Left — this rule
will modify Formula 1 above the line. Remember
that Implies_Left splits the proof tree into two
branches. We show and deal with Case 1 first,
then move to Case 2 later.
Case 1 Antecedents Formula 1 Q gt
R Formula 2 P Formula 3 Q Consequents Fo
rmula 1 R
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
61
Formality
To modify Formula 1 above the line, we next apply
the rule Implies_Left again. Again this splits
the proof tree into two branches. We show and
deal with Case 1.1 first, then move to Case 1.2
later.
Case 1.1 Antecedents Formula 1 R Formula
2 P Formula 3 Q Consequents Formula 1 R
Case 1.1 will now yield to an application of
Prop_Axiom
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
62
Formality
As noted, an application of Prop_Axiom (Step 5)
completes Case 1.1. We now move to Case 1.2.
This is the second case resulting from the
application of Implies_Left on the Case 1
sequent. Another application of Prop_Axiom (Step
6) completes Case 1.2 (and in turn Case 1 itself).
Case 1.2 Antecedents Formula 1 P Formula
2 Q Consequents Formula 1 Q Formula 2 R
Case 1.2 will also yield to an application of
Prop_Axiom
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
63
Formality
Having completed the proof for Case 1, we now
move to Case 2. Recall that this is the second
case resulting from our first application of
Implies_Left. Another application of Prop_Axiom
(Step 7) completes Case 2 (and in turn the entire
proof).
Case 2 Antecedents Formula 1 P Formula 2
Q Consequents Formula 1 P Formula 2 R
Case 2 will also yield to an application of
Prop_Axiom
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
64
Prototyping
- Oriented to design model
- Dont confuse with simulation
- Some consider functional requirements only.
- Can be a partial implementation of requirements
- Can be an executable specification
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
65
The Two Vs and techniques
- VV in order to avoid what is gtverifivation and
validation an eternal debate - In either case We check with respect to
something. - Consider a Petri net model of list automation
- Verifying Properties of Petri nets does not mean
the user is satisfied
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
66
VV in EIA 632
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
67
VV in EIA 632
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
68
Conclusions
- Many techniques
- Many tools
- Notation oriented in some cases (formal and
semi-formal methods)
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
69
Next lecture
Verification and Validation
Standards and Case Studies
- ‘Validation Are we building the right product’
‘Verification Are we building the product right’
Requirements ValidationRequirements ManagementRequirements Validation?? Validation, Verification, Accreditation !!build the Right System Build It RightContentWhat the standard say (EIA632)What the standard say (EIA632)What the standard say (EIA632)ValidationRequirement 25Requirement Statements ValidationRequirement 26Acquirer Requirements ValidationRequirement 27Other Stakeholder RequirementsValidationRequirement 28System Technical RequirementsValidationRequirement 29Logical Solution RepresentationsValidationSystem VerificationRequirement 30Design Solution VerificationRequirement 31End Product VerificationRequirement 32Enabling Product ReadinessRequirement 33End Products Validation(No Transcript)What the standards say ()Correctness and completenessConsistentUnambiguousFunctionalVerifiableTraceabilityTechniques and methodsInspectionInspection (example)Inspection (example)RulesIntroduce the following three rules forinspecting a requirements documentInspection (example)DefectExplain the definition of a DefectInspection (example)SeverityInspection (example)Exit?Agree with the management team on a numeric exitconditionInspection (example)Inspection (example)Inspection (example)Letter to Your BossSimulationModel CheckingModel Checking and FormalityModel Checking and FormalityModel Checking and FormalityModel Checking and FormalityModel Checking and FormalityModel Checking and FormalityModel Checking and FormalityModel Checking and FormalityA Simple String Parser Given an input string of0s and 1s, determine if the string starts andends with a 1.State Transition FunctionS1current stateS2startS0 S1 S2 DS0inputaccept stateD S1 S1 DS1 S2 S2 D0, 1dead statenext stateFormalityFormal analysis refers to tool-based techniquesused to explore, debug, and verify formalspecifications.our focus hereL 5Formality-PropertiesFormalityFormalityFormalityProp_AxiomFormalityFormalityAnd_LeftFormalityImplies_LeftFormalityImplies_RightFormalityTheorem 1 (P gt (Q gt R)) gt ((P /\Q) gt R)FormalityTheorem 1 (P gt (Q gt R)) gt ((P /\Q) gt R)We begin the proof by forming the requisitesequentAntecedents none Consequents Formula 1 (Pgt (Q gt R)) gt ((P /\ Q) gt R)FormalityAs our first step we apply the ruleImplies_Right. This rule will decompose theentire formula. Remember there is an impliedimplies in the sequent. In other words thissequent could be written – (P gt (Q gt R)) gt((P /\ Q) gt R). Hence, the implies we applythe rule to is the outside implies on the rightof the sequentAntecedents Formula 1 P gt (Q gt R)Consequents Formula 1 (P /\ Q) gt RFormalityA second application of the rule Implies_Rightwill decompose the formula below the line in asimilar way. Remember that rules applying to theleft part of the sequent work on formulas abovethe bar rules applying to the right part ofthe sequent work below the bar.Antecedents Formula 1 P gt (Q gtR) Formula 2 P /\ Q Consequents Formula 1FormalityWe next apply the rule And_Left — this rule willmodify (rewrite) Formula 2 above the line.Remember that all formulas above the line areconnected by ANDs formulas below the line areconnected by ORs.Antecedents Formula 1 P gt (Q gtR) Formula 2 P Formula 3Q Consequents Formula 1 RFormalityWe next apply the rule Implies_Left — this rulewill modify Formula 1 above the line. Rememberthat Implies_Left splits the proof tree into twobranches. We show and deal with Case 1 first,then move to Case 2 later.Case 1 Antecedents Formula 1 Q gtR Formula 2 P Formula 3 Q Consequents Formula 1 RFormalityTo modify Formula 1 above the line, we next applythe rule Implies_Left again. Again this splitsthe proof tree into two branches. We show anddeal with Case 1.1 first, then move to Case 1.2later.Case 1.1 Antecedents Formula 1 R Formula2 P Formula 3 Q Consequents Formula 1 RCase 1.1 will now yield to an application ofProp_AxiomFormalityAs noted, an application of Prop_Axiom (Step 5)completes Case 1.1. We now move to Case 1.2.This is the second case resulting from theapplication of Implies_Left on the Case 1sequent. Another application of Prop_Axiom (Step6) completes Case 1.2 (and in turn Case 1 itself).Case 1.2 Antecedents Formula 1 P Formula2 Q Consequents Formula 1 Q Formula 2 RCase 1.2 will also yield to an application ofProp_AxiomFormalityHaving completed the proof for Case 1, we nowmove to Case 2. Recall that this is the secondcase resulting from our first application ofImplies_Left. Another application of Prop_Axiom(Step 7) completes Case 2 (and in turn the entireproof).Case 2 Antecedents Formula 1 P Formula 2Q Consequents Formula 1 P Formula 2 RCase 2 will also yield to an application ofProp_AxiomPrototypingThe Two Vs and techniquesVV in EIA 632VV in EIA 632ConclusionsNext lectureVerification and ValidationStandards and Case Studies
