Skip to content
0:00 / 0:00

#safety-critical#formalverification#standards

"Standards We Love" by Heidy Khlaaf [PWLConf 2018]

PapersWeLove

23K subscribers • 35 videos on Hallway • Community channel

YouTube
  • Recommended by 2 people: 1 on Lobsters and 1 in engineering communities.
  • Presented by Heidy Khlaaf, Research Consultant, Adelard LLP
  • Linked in the descriptionpapers-we-love/pwlconf-info

Intermediate. Assumes working knowledge.

1.9K views8 years ago2 recommendations

Software designSystems programmingFormal methods and verificationSoftware architecture

Heidy Khlaaf explains how software in safety-critical systems is assured, verified, and governed by rigorous standards.

PWLConf 2018 Link: pwlconf.org/2018/heidy-khlaaf/ Slides / Captions: github.com/papers-we-love/pwlconf-info/tree/master/2018/heid… Standards We Love (for assuring and verifying safety-critical systems) Heidy Khlaaf, Research Consultant, Adelard LLP 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 (heidyk.com/) 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. ----------------------------------------------------------------------------------------------------------- Platinum Sponsor: Droit (droit.tech/) Video Sponsor: Datadog (datadoghq.com/) Captioning Sponsor: Comcast (jobs.comcast.com/) -----------------------------------------------------------------------------------------------------------

Why it's here

2 people recommend this

What people say. Recommended as an insightful talk on how safety-critical software is verified and why C remains prevalent in these systems.

Moments people linked to

u/pron98in r/programming • Recommends

On “Would Rust secure cURL?”

Absolutely. Perhaps ironically, for the most safety-critical software, C is still the best choice (and some other specialised languages like SCADE, that compiles to C, and SPARK). For one, it has the best formal verification tools. For another, much of that software is written for custom hardware where C is the only available option. E.g. this Also, Rust, like C++, has some intrinsic problems that make it not a very appealing choice for safety-critical software (not that cURL is safety-critical) like language complexity and a lot of implicitness.
3View on Reddit