Taxonomy/supplement/The problem statement table

The overal problem is to verify the specification against the requirement.

Problem statement

Problem	Designing an artefact specification and verifying it. The overall requirement is R0: Get 1 or two cups of hot coffee when desired.
Question	Answer	Explanation
→properties
How are the properties under discussion defined?	o by a more or less vague idea of a customer o together with a partial blueprint	There is a customer who wants some kind of a coffee machine. There is already a solution, but I want to make smth new. However, I will make the (specification of a) coffee machine that satisfies the same requirement. Also, I will use their sketch of the artefact as a help for the design of the mechanical parts.
Can the customer be consulted? Who?	Yes, we have a customer (Ms A. Ivanovic).	First I came up with the offer for the coffee machine. The initial requirements of the customer were: (R0) "I want the machine that produces 1 or 2 cups of coffee. One cup of coffee is made of 1 dl of water and 15g of the coffee. Water reservoir should have the capacity of 1 liter and the coffee reservoir should have the capacity of 0.5 kg of the coffee." Question for the customer: Do you agree to have a machine that will produce only one kind of coffee (ordinary Dutch coffee)? Do you agree that it is without the option of getting sugar and/or milk in it?
What is the problem domain?	I see two levels: Problem domain #1: Recipe for a coffee (ingredients, their amounts and possibly cooking time). Problem domain #2: Mechanical and electrical parts that will constitute the artefact.	At the Lego problem, we said that the problem domain is sorting Lego blocks. Maybe the problem domain #2 belongs to the realization of the specification, which is not the problem we are solving here. No, we need some characteristics of mechanical and electrical parts.
Can a Domain expert for the problem domain be consulted? Who?	For the Problem domain #1: we will consult our customer for the recipe for the coffee.	I propose the following recipe: 15 g of the coffee milled for the 'filter coffee', 1dl of hot water (95 oC). Mix 5 seconds and pour through the filter. I also have a domain expert for mechanical and electrical parts (that is Mr D. Jovanovic)
→specification
Which →specification language is (to be) used? Why?	Predicate logic	This is the language that the verification expert knows. It allow us to prove the specification with the theorem prover.
Is there a complete, formal specification?	o There is none	The first try: ∀t:T. (one_cup_cofee_desired(t) ∨ two_cups_cofee_desired), (cup_placed ⇒ (one_cup_cofee_desired(t) ⇒ 1dl_cofee_in_cup(t))) ∧ (two_cups_placed ⇒ (two_cups_cofee_desired(t) ⇒ (1dl_cofee_in_left_cup(t) ∧ 1dl_cofee_in_right_cup(t))))
If the specification is not fixed: how can it be Validated?	Negotiation with the customer
Does the customer or his domain expert understand the specification language?	No, he doesn't. But the verification expert will translate statements written in predicate logic, back to English language.
→blueprint
Which blueprint language is (to be) used? Why?	In different stages we will use different languages and notations. We first start with an informal sketch of the artifact. The next thing is to draw a problem diagram. It will help us to identify interfaces between components, where components are parts of the plant and the control Each part will be described with the predicate logic.
How complete is the blueprint?	o some parts, but not all are well-specified	There is a sketch of mechanical parts. There isn't a specification of these parts. And there is no control blueprint.
Do the providers of parts or their Domain experts understand the respective →specification languages from the →blueprint?	We will use problem diagrams and predicate logic and our customer understands them.	The interesting question is - what if the customer doesn't understand our specification language? We have to write down everything in natural language or in the language that we both understand.
How should it be established that the blueprint satisfies the specification?	We will formally verify description of the plant and the control (using a theorem prover, PVS for example).
How should it be established that the artefact is a correct realisation of the blueprint?	Here, we will only verify the blueprint. Building an artefact is another problem.	It can happen that, while building an artefact, we realize that parts of the blueprint have to changed. But, here we are exercising NMR only until the realization of the blueprint.
→artefact
How much of the artefact exists? Where?	o Nothing exists.
If it does not (fully) exist, how and by whom will it be realised?	We are now designing a blueprint. Realisation is left for a later stage.
What are the solution domains for the missing parts?	Mechanical parts (reservoirs, pipes), electro-mechanical parts (motors, valves, warmer), control part that will be realised by software running on a microprocessor
Who are the Domain experts for the missing parts and their interfaces?	Mechanical, electrical, control, software engineers
How can the artefact be Validated w.r.t. a specification?	Not being done here.
Plan
Step	To do	Comment
1	Design the specification of the plant parts
2	At the same time parts of the control specification are designed
3	Design (finish) the control specification
4	Verify formally the overall specification