#!/usr/local/bin/php Bloodbank
RTG Home  |   PRECISE  |   CIS Home  |   Penn Engineering  |   Penn

Policy documents contain rules that must be adhered to when implementing policy. The Food and Drug Administration (FDA) has created rules or regulations for blood bank organizations which are contained in the Code of Federal Regulations (CFR). These documents are written in natural language which makes them prone to under-specifications, conflicts, ambiguities, etc. This makes the extraction of an algorithmic procedure difficult and error prone.

Our case study identified inconsistencies in the document and implementation using domain knowledge and an extracted formal model which has a high degree of traceability to the document. This model was checked for internal inconsistency and totality using existing boolean satisfiability checkers. The case study also explained a testing procedure to check for conformance of an implementation to the policy. Conformance failure can be traced back to the policy document using the formal model.

We used the tests generated from the model to check a blood bank software implementation against the regulations. We discovered several problems in the implementation, mostly corresponding to areas of ambiguity in the regulations.

RTG Home  |   PRECISE  |   CIS Home  |   Penn Engineering  |   Penn