Heidy Khlaaf

Standards We Love (for assuring and verifying safety-critical systems)

Safety-Critical systems are prevalent throughout our everyday life, from using electricity generated by a nuclear power plant to riding an airplane in order to attend your favorite conference. Despite the increasingly-complex software used in these systems, both the tech and verification communities are largely unaware of the issues, processes, and standards that govern them. This talk will provide an overview of safety-critical systems and how the software used is assured and verified up to standards that ensure our safety.

References

• The UK’s Office for Nuclear Regulation Technical Assessment Guide (TAG) dealing with the software of computer based safety systems (SSs)
• The “Golden boy” standard used in the TAG above, and in all other safety-critical applications. The standard itself isn’t publicly available.
• A standard book explaining what model-checking is, and it is referenced to in 61508.
• Process papers regarding our work at Adelard:
  • Assessment and Qualification of Smart Sensors by S. Guerra, P. Bishop, R. Bloomfield, and D. Sheridan
  • V&V Techniques for FPGA-Based I&C Systems – How Do They Compare with Techniques For Microprocessors? by S. George and S. Guerra
• Academic papers that attempt to solve some of our technical issues, but make some inaccurate assumptions about the systems being dealt with:
  • Analysing Memory Resource Bounds for Low-Level Programs by W. Chin, H.H. Nguyen, C. Popeea, S. Qin
  • Formal Techniques for Effective Co-verification of Hardware/Software Co-designs by R. Mukherjee, M. Purandare, R. Polig, D. Kroening
• The only academic paper I have found that accurately addresses issues dealt with in embedded systems:
  • Static Checking of Interrupt-driven Software by D. Brylow, N.Damgaard, J. Palsberg

Biography

Heidy Khlaaf is a Research Consultant at Adelard LLP where she evaluates, specifies, and verifies the implementations of safety-critical systems, and also contributes to the production of standards and guidelines for safety and security related applications and their development. Previously, she received her PhD from University College London where she developed novel research methodologies, in part with Microsoft Research, to fully-automate the verification of temporal properties over software systems in the tool T2.

Links

• DBLP
• HeidyKhlaaf / Twitter