Taxonomy/2. Methodology/Focus (correctness)

As explained under Development end Verification and validation, we should state what is given and what not. This should be done for one Chinese Box, i.e. one instance of the Rationality Square and Correctness Theorem at a time.

Problem statement form correctness

Please stay at one level and don't climb up and down! It can be helpful, however, also to fill in a problem statement form for the surrounding artefact.

Problem statement

Problem
Question	Answer	Explanation
→properties
How are the properties under discussion defined?	o by an existing →artefact o by a given →blueprint o by a given →specification o implicitly by the needs of a surrounding artefact o by a more or less vague idea of a customer o together with an incomplete →artefact o together with a partial blueprint
Can the customer be consulted? Who?
What is the problem domain?
Can a Domain expert for the problem domain be consulted? Who?
→specification
Which →specification language is (to be) used? Why?
Is there a specification?	o There is a tentative specification, may be negotiated with the customer o The specification is fixed by a contract o There is a complete formal specification o The specification must be written in a formal language o No specification is possible, but there are principles o No specification is intended, nor are there principles.
If the specification is not fixed: how can it be Validated?
Does the customer or his domain expert understand the specification language?
→blueprint
Which blueprint language is (to be) used? Why?
How complete is the blueprint?	o non-existent o decomposition in parts o some parts, but not all are well-specified o complete
Do the providers of parts or their Domain experts understand the respective →specification languages from the →blueprint?
How should it be established that the blueprint satisfies the specification?
How should it be established that the artefact is a correct realisation of the blueprint?
→artefact
How much of the artefact exists? Where?	o The entire artefact exists. o Most of the artefact exists, but something has to be added. o All of its parts exist but are not yet assembled. o Most of its parts exist, but some don't. o Nothing exists.
If it does not (fully) exist, how and by whom will it be realised?
What are the solution domains for the missing parts?
Who are the Domain experts for the missing parts and their interfaces?
How can the artefact be Validated w.r.t. a specification?
Plan
Step	To do	Comment
1
2

Examples

Case Study1. The batch plant and its control program

Problem statement

Problem #001	Batch plant: Find the specification for the control
Question	Answer	Explanation
Properties
How are the properties under discussion defined?	o by an existing artefact o by a given blueprint o by a given specification o implicitly by the needs of a surrounding artefact x by a more or less vague idea of a customer x together with an incomplete →artefact o together with a partial blueprint	The physical chemical plant is given, including a computer, but without a control program. The required properties are: pump batches around in this plant.
Can the customer be consulted? Who?	The customer is the one who defined this case study
What is the problem domain?	Chemical reactions, mixing, separating
Can a domain expert for the problem domain be consulted? Who?	Yes: Nanette
Specification
Which specification language is (to be) used? Why?	A dialect of predicate logic	Predicate logic because it is basic, a dialect to improve readability
Is there a complete, formal specification?	x There is none o There is a tentative specification, may be negotiated with the customer o The specification fixed by a contract
If the specification is not fixed: how can it be validated?	By asking the "customer"
Does the customer or his domain expert understand the specification language?		Nanette can understand a specification in predicate logic if someone helps.
Blueprint
Which blueprint language is (to be) used? Why?	the same dialect of predicate logic	verification
How complete is the blueprint?	o non-existent x decomposition in parts o some parts, but not all are well-specified o complete	A decomposition in 2 parts is mandatory: the existing plant, including the controller the control program There is no further decomposition or specification for the plant, only a diagram. It shows the interface to the computer program.
Do the providers of parts or their domain experts understand the respective specification languages from the blueprint?	They can explain their diagram. With a little help they can be made to understand the blueprint to be written in logic.
How should it be established that the blueprint satisfies the specification?	Theorem proving with PVS
How should it be established that the artefact is a correct realisation of the blueprint?	For the plant: ask plant expert. For the program: compile and load
Artefact
How much of the artefact exists? Where?	o The entire artefact exists. x Most of the artefact exists, but something has to be added. o All of its parts exist but are not yet assembled. o Most of its parts exist, but some don't. o Nothing exists.	The control program is missing. The rest of the plant exists, but no meaningful decomposition is defined.
If it does not (fully) exist, how and by whom will it be realised?	Angelika will write a control program and send it to Nanette, who will load it into the computer	See problem statement #002
What are the solution domains for the missing parts?	Programming language
Who are the domain experts for the missing parts and their interfaces?	Angelika and Hanno
How can the artefact be validated w.r.t. a specification?	By a correctness proof for this theorem and that of statement #002	Or, in this simple case, by a test. Once it runs, one can see that it works.
Plan
1	Decompose existing plant	Non-Monotonic Refinement
2	Specify components of plant together with overall goal	Non-Monotonic Refinement
3	Determine specification of control to obtain a provable correctness theorem
4	Prove theorem	PVS

Problem statement

Problem #002	Batch Plant: code for the control program
Question	Answer	Explanation
Properties
How are the properties under discussion defined?	o by an existing artefact o by a given blueprint x by a given specification o implicitly by the needs of a surrounding artefact o by a more or less vague idea of a customer o together with an incomplete →artefact o together with a partial blueprint	Problem statement #001
Can the customer be consulted? Who?	Yes, Angelika	Angelika derived the specification and proved the surrounding correctness theorem
What is the problem domain?	Software
Can a domain expert for the problem domain be consulted? Who?	Yes: Hanno	He knows about program correctness
Specification
Which specification language is (to be) used? Why?	A dialect of predicate logic	Given from Problem #001
Is there a complete, formal specification?	o There is none o There is a tentative specification, may be negotiated with the customer x The specification fixed by a contract
If the specification is not fixed: how can it be validated?
Does the customer or his domain expert understand the specification language?	Yes.
Blueprint
Which blueprint language is (to be) used? Why?	The programming language	Because the computer is given
How complete is the blueprint?	x non-existent o decomposition in parts o some parts, but not all are well-specified o complete
Do the providers of parts or their domain experts understand the respective specification languages from the blueprint?	no	Not necessary. The parts are the contructs of the programming language. The programmers understand these and do not need providers' support.
How should it be established that the blueprint satisfies the specification?	software engineering: proving a program correct by constructing it
How should it be established that the artefact is a correct realisation of the blueprint?	compilation, loading
Artefact
How much of the artefact exists? Where?	o The entire artefact exists. o Most of the artefact exists, but something has to be added. x All of its parts exist but are not yet assembled. o Most of its parts exist, but some don't. o Nothing exists.	All of the parts exist because they are the constructs of an existing programming language.
If it does not (fully) exist, how and by whom will it be realised?	Angelika will derive a control program from the specification developed under proplem statement #001	A program is its own blueprint. It has just to be compiled and loaded by Nanette.
What are the solution domains for the missing parts?
Who are the domain experts for the missing parts and their interfaces?
How can the artefact be validated w.r.t. a specification?	Correctness proof a posteriori or systematic development	We assume compilation and loading to be correct.
Plan
1	Write a program for a given, fixed specification	standard software engineering
2	Compile and load it

Protocol verification

Problem statement

Problem	Verification of the alternating pit protocol
Question	Answer	Explanation
Properties
How are the properties under discussion defined?	o by an existing artefact o by a given blueprint o by a given specification x implicitly by the needs of a surrounding artefact o by a more or less vague idea of a customer o together with an incomplete →artefact o together with a partial blueprint	Reliable communication via a lossy channel
Can the customer be consulted? Who?	Yes	The designer of the surrounding artefact wants to rely on communication but became aware that channels can lose messages. He will be able to help to decide what is acceptable and what not in order to obtain a correct design
What is the problem domain?	Computer networks
Can a domain expert for the problem domain be consulted? Who?	Yes	The same designer of the surounding artefact.
Specification
Which specification language is (to be) used? Why?	May be chosen
Is there a complete, formal specification?	o There is none x There is a tentative specification, may be negotiated with the customer o The specification fixed by a contract	There is an informal specification in terms of "as good as possible". The definitive specification will have to be found as the strongest specification that is satisfied by the protocol under discussion.
If the specification is not fixed: how can it be validated?	By asking the customer
Does the customer or his domain expert understand the specification language?	Will depend on the language
Blueprint
Which blueprint language is (to be) used? Why?	algorithms plus a suitable specification language for lossy channels
How complete is the blueprint?	o non-existent o decomposition in parts x some parts, but not all are well-specified o complete
Do the providers of parts or their domain experts understand the respective specification languages from the blueprint?	Yes.
How should it be established that the blueprint satisfies the specification?	Formal verification.
How should it be established that the artefact is a correct realisation of the blueprint?	For the algorithms: compilation. For the channel: validation.
Artefact
How much of the artefact exists? Where?	x The entire artefact exists. o Most of the artefact exists, but something has to be added. o All of its parts exist but are not yet assembled. o Most of its parts exist, but some don't. o Nothing exists.
If it does not (fully) exist, how and by whom will it be realised?
What are the solution domains for the missing parts?
Who are the domain experts for the missing parts and their interfaces?
How can the artefact be validated w.r.t. a specification?	By a correctness proof plus validation of the specification of the lossy channel.	That is the problem!
Plan
1	Fault hypothesis: write and validate a specification for the lossy channel
2	Derive a realistic specification for the overall system	Non-Monotonic Refinement
3	Choose a proof method	and translate everything into the languages supported by the proof tool, if necessary
4	Prove it.

Protocol verification

Problem statement

Problem	Verification of the plans for a self--assembly home--trainer
Question	Answer	Explanation
Properties
How are the properties under discussion defined?	x by an existing artefact x by a given blueprint o by a given specification o implicitly by the needs of a surrounding artefact x by a more or less vague idea of a customer o together with an incomplete →artefact o together with a partial blueprint	We want to know if our assembly--plan, which goes with our cheap hometrainers that people can assemble themselves, at home, is adequate.
Can the customer be consulted? Who?	Yes	We can interview the manufacturer of the product.
What is the problem domain?	Parts, Assembly--plans, Users
Can a domain expert for the problem domain be consulted? Who?	Yes	The designer(s) of the home--trainer, the writer(s) of the assembly plan, the (representative) end--users of the product.
Specification
Which specification language is (to be) used? Why?	Probably some form of (untimed) state machines.	To model the successive states of the parts/agregates.
Is there a complete, formal specification?	x There is none o There is a tentative specification, may be negotiated with the customer o The specification fixed by a contract	There is an implicit specification in terms of the combination of assembly--plan, parts and average user competence as natural language interpreter/mechanic.
If the specification is not fixed: how can it be validated?	We have all the parts and the assembly--plans. We can see if our specifcation is adequate by checking if all the possible assembly steps we modeled are possible in practice and if everything that is possible in practice is either modeled or explicitly disallowed based on the blueprints.
Does the customer or his domain expert understand the specification language?	No
Blueprint
Which blueprint language is (to be) used? Why?	For the parts: CAD/CAM plans. For the assembly plan: natural language with diagrams and pictures.	For the parts: this is the industries' established way to communicate these designs. For the assembly plans: we cannot assume anything more from users.
How complete is the blueprint?	o non-existent o decomposition in parts o some parts, but not all are well-specified x complete
Do the providers of parts or their domain experts understand the respective specification languages from the blueprint?	We assume they do.
How should it be established that the blueprint satisfies the specification?	We can do systematic justification based on our own competence as natural language users. Possibly experiment with users.
How should it be established that the artefact is a correct realisation of the blueprint?	For the parts: this is a matter of quality assurance. For the assembly--plans: this is trivial since they are simply printed.
Artefact
How much of the artefact exists? Where?	o The entire artefact exists. o Most of the artefact exists, but something has to be added. x All of its parts exist but are not yet assembled. o Most of its parts exist, but some don't. o Nothing exists.	The unfinished artefact is the realisation of the blueprints which, in our case is a package of parts (which is given) and an assembly plan (which is directly printed from the blueprints). The correct behavior of this unfinished artefact when offered to a user should lead to a user with a hometrainer (as specified by us).
If it does not (fully) exist, how and by whom will it be realised?	User.
What are the solution domains for the missing parts?	Not applicable.
Who are the domain experts for the missing parts and their interfaces?	Not applicable.
How can the artefact be validated w.r.t. a specification?	By checking if all the possible sequences of steps allowed by the assembly plans + parts are modeled in the specification and, vice versa, all the possible sequences modeled in the specification are allowed by the assembly plans + parts.
Plan
1	Model the possible assembly steps allowed by the current assembly plan.
2	Derive a realistic specification for parts and the ways in which the assembly steps combine them into agregates.	Non-Monotonic Refinement
3	Model the possible, desired results of the assembly process.	Discuss with designers whether each possible resulting device is still a home--trainer.
4	Prove that all possible assembly sequences lead to a desired result.