| Bloodbank |
|
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. |