The PROTOCURE project is funded by the Future and Emerging Technologies arm of the IST program, FET-Open scheme, under contract number IST-2001-33049. PROTOCURE is an assessment project running from December 1, 2001, and has a duration of 12 months.

Improving medical protocols by formal methods

Future and Emerging Technologies

Project number IST-2001-33049

Last modified: Tue Feb 26 12:00:55 CET 2002


(See also the Project presentation deliverable)

Problem statement and approach

During the last decade, the approach of evidence-based medicine has given rise to an increasing number of clinical practice guidelines and protocols. They provide clinicians with health-care recommendations based on valid and up-to-date empirical evidence. In this way, they facilitate the spreading of high standard practices that otherwise would have much less impact. Moreover, it has been proved that adherence to guidelines and protocols may reduce health-care costs up to a 25%.

A high number of medical guidelines have been published in the literature and Internet, making them more accessible. However, the work done on developing and distributing guidelines far outweighs the efforts on guaranteeing their quality. Indeed, anomalies like ambiguity and incompleteness are frequent in medical guidelines. Even more, they can be inconsistent because of the lack of familiarity of the designer with certain principles and notations. The most important consequence of these problems is that they preclude the effective application of guidelines.

Recent efforts have tried to address the problem of guideline quality improvement. The medical community has sought to organise and integrate guidelines into compendiums, to make them more accessible, usable and comprehensible. With the aim of ensuring a high degree of quality, the organisations promoting these initiatives have also set minimal standards for the inclusion of guidelines in the compendiums. These standards take into account, for instance, the relevance and validity of the sources employed for the development of the guidelines. These approaches are not sufficient since they rely on informal processes and notations. As a result, many practical guidelines are still ambiguous, incomplete or inconsistent. Even when ambiguity or incompleteness are intentionally included in guidelines by the designer, so that organisational or personal practices can be deployed at certain points, it is important to make them explicit as choices. A substantially different approach, grounded on a formal representation of guidelines, can answer these needs.

An appropriate representation language, with a clear and well-defined semantics, would allow for a systematic verification of guidelines by formal methods. Unlike the after-dissemination activities mentioned before, this approach would make quality improvement possible during the stage of guideline development.

Research from the fields of computer science and artificial intelligence can help in both the definition of an adequate guideline description language and the development of techniques for the formal analysis of guidelines. The language must give means to represent explicitly, and in a non-ambiguous way, all the relevant knowledge about guidelines. Based on the formal semantics of this language, the analysis techniques should allow for the determination of, for instance, completeness (no missing cases), consistency (no contradictions) and correctness (objectives are satisfied).


The solution suggested to the problem of quality improvement of protocols consists in the utilisation of formal methods. It supposes the definition of an adequate protocol representation language, the development of techniques for the formal analysis of protocols described in that language, and more importantly, the evaluation of the feasibility of the approach based on the formalisation and verification of real-life medical protocols. For the first two aspects we will rely on earlier work by consortium partners, on the Asbru language for protocol description and on the KIV interactive verification system. The third aspect, namely the evaluation of the feasibility of the use of formal methods for quality improvement of protocols, constitutes the main objective of this assessment project.

Description of the work

The steps with which we will carry out this evaluation are the following:
  1. Take two real-life reference protocols which cover a wide variety of protocol characteristics
  2. Formalise these reference protocols
  3. Check the formalisation in an exercise for the verification of interesting protocol properties
  4. Determine how many errors (expected and unexpected) can be uncovered in this way
where step 4. will be our measure of success.

We will rely on earlier work by consortium partners, in particular, on the Asbru language for protocol representation and on the KIV interactive verifier system. This leads to the following tasks:

Milestones and expected results

Different reports will be issued during the project, roughly after the completion of every one of the above tasks. The results of this assessment project will be in short:

Back to top


For more information, see the Project presentation deliverable or contact Mar Marcos (e-mail:

Back to top


Back to top


Back to top

Related links

Back to top