P R O T O C O L (Michael)
                   17th September 2002, Castellon
        Working session: Discussion of verification results




/------------------------------------\
| Discussion of verification results |
\------------------------------------/

1 Overall
---------

Question: Are there any flaws we detected only by formal verification?
Answer: Yes, see Jaundice
* We discovered not only a flaw (property does not hold),
  but a possible fix (assumptions).
* This could seem trivial afterwards, but was not in the beginning.

Question: Where is the origin of the flaw?
* Original protocol
* Asbru version
* KIV formalisation

[=> Even errors introduced in formalisation steps can be remedied by formal verification.]



2 Diabetes properties
---------------------

List of Mar's comments to CBO property
  * trivially violated or satisfied
  * e.g. 1/3 - 2/3 property trivially violated

Selected property:
  "No more than two drugs at the same time"
  
  Dutch protocol satisfies this property trivially

  Peter: Flaw in Dutch version relative to a different property (?)
    This version could (trivially) violate the "2 drugs + insulin" property
    => Check this

Major question:
  Why are the properties on the Diabetes protocol so much easier to
  verify than the ones for Jaundice?

  Possible answers:
  * Better written (?) => we could examine protocol with AGREE instrument
  * More abstract (?)
  * All properties were derived from the protocol (no independent source)
  * Less hidden assumptions with respect to Jaundice (?)



3 Jaundice properties
---------------------

3.1 Summary
-----------

Proved termination, 2 intentions, most challenging indicator 7

Results:
* Problems with termination
* Problems with indicator 7


3.2 Significance of indicator
-----------------------------

* Medical (it originates from MAJIC document)
  - Measurements are risk for baby (reduction of risk)
  - Cost effectiveness

* Why did we use indicator 7?
  => Comment on other indicators
     We took the most challenging one :-)


3.2 Verification of indicator
-----------------------------

How did we verify indicator?
  + Include dirty things in deliverable (statistics about proofs, problems)
  + Comment on problems

Result: Assumptions
(1) If phototherapy is discontinued, TSB (reading) will be 'observation'.
(2) Observation will run for less than 24 hours.
(3) After phototherapy and observation, TSB (reading) will still be 'observation'.

Assumptions seem to make sense. They characterize normal behaviour.

Comments on assumptions
(1) Kitty's expert never experienced that (1) was violated.
(2) Check with experts: Is measuring TSB every 12-24h too simple a strategy?
    Then probably suggest change to protocol.
(3) Check with experts


3.3 Termination
---------------

To discuss in deliverable: Why is termination important?


3.4 Future improvements
-----------------------

* How can you improve the formalisation such that properties can be formulated
  more easily?
  E.g.: Labels added to protocol (acttime time)
  E.g.: Modeling effects of plans to patients (e.g. under-phototherapy flag)



4 Significance of method
------------------------

Is there a benefit to verify properties like this?
(see above)



5 Future projects
-----------------

* How do we come up with interesting properties?
* How do we efficiently prove properties?




/-----------------\
| Overall project |
\-----------------/

Summary
-------

                           |              |       Examples
Technique                  |   Benefit    | Jaundice | Diabetes
---------------------------+--------------+----------+---------
Asbru formalisation        |  Anomalies   |   ...    |   ...     -> [IDPT paper]
---------------------------+--------------+----------+---------
Static verification        |  Quality of  |    -     |    -      -> [part of Ph.D. Georg]
                           |    plans     |          |
                           |  (static)    |          |
---------------------------+--------------+----------+---------
Simulation (Interpreter)   |  Quality of  |          |           -> [Tech. Reports]
                           |    plans     |          |
                           |  (dynamic)   |          |
---------------------------+--------------+----------+---------
Critiquing                 | Do doctors   |          |           -> [Vincent] (sim.)
                           | comply with  |          |           -> [AiME] (manual)
                           |  protocol    |          |
                           | (and v.v.)?  |          |
---------------------------+--------------+----------+---------
Property(1) formalisation  | Clarification|          |           -> [Deliverable WP4]
                           |   of goals   |          |
---------------------------+--------------+----------+---------
Verification               | Confirmation |          |           -> [Deliverable WP4]
                           | Flaws        |          |
                           | Assumptions  |          |
                           | Explicit med.|          |
                           |  knowledge   |          |

(1) Properties, Intentions, Indicators