I have just spent one week at Schloss Dagstuhl, a center for informatics research in a rural part of Germany, meeting other researchers interested in software certification.
The seminar brought together researchers from academia and industry, looking at software certification problems in a variety of domains, including nuclear power, aviation, medical devices and transportation.
The seminar was very worthwhile and I learned many new things. I also gave a presentation entitled: “Certification of Medical IS – A paradigm shift: from devices to systems, from functions to data“.
There were many interesting presentations and discussions and I will post about several of them in the next few weeks while I collect my thoughts on what I learned. One presentation that was very well done and that resonated with me in a special way was given by John Rushby of SRI International. The title of his presentation was on “Logic and Epistemology in Assurance Cases“. Traditionally many of the correctness assurance methods in software engineering have concentrated on proving that the software artifacts meet specified requirements. This is commonly called software verification and may be based on logic or other theories.
Notably though, many of the problems we see with health information system software today do not pertain to software not meeting its specified requirements but rather to problems with the specified requirements, for example making unrealistic assumptions about the clinical context and being incomplete.
Assurance cases have recently seen much attention as a method to structure safety or security arguments in software systems. The three main concepts in Assurance Cases are
Claim <– Argument <– Evidence
Assurance cases go beyond software verification (and logic reasoning about the software program and its specification) and also consider validation of the software, explicitly testing our knowledge and assumptions about the real world. In other words they span epistemology (the knowledge we have about the world) and logic.
John Rushby made an interesting point in his presentation stating that in software certification we can to some degree trade complexity between the two domains of epistemology and logic: if we specify strong assumptions about the world (the software’s deployment environment), we can get away with simpler program logic, and vice versa.
Resilient systems are those that make weak assumptions on the environment. Which means that the resulting program logic will have to deal with more complexity. The health care environment is known to be complex and ill-structured. Consequently, we need to shift complexity from epistemology to logic in order to provide resilient systems. This may be one of the key challenges in certification of health information system software.