Hacker News new | past | comments | ask | show | jobs | submit login
Software Requirements Errors in Safety-Critical, Embedded Systems (1993) [pdf] (semanticscholar.org)
67 points by blacksmythe on Dec 1, 2017 | hide | past | favorite | 39 comments



Can't help but think we'd learn a lot if other industries were as mature in tracking these things as the safety critical ones.


I'm always surprised by how thoroughly uninterested the Haskell and Rust communities are in learning from the Ada/High Integrity Software community.

Here you have people who are actually doing what you purport to be interested in (creating defect-free code) who have a great deal of experience and a great many insights from actually putting their code into avionics bays knowing that thousands of lives are depending upon it.

But they're not valley programmers. They skew older. Heck most of them don't even live in California. And they don't "get" what's so amazing about category theory as a programming paradigm so obviously they're morons. Plus they seem to be process-obsessed and that process ain't agile.

Maybe eventually the valley bros will rediscover most of what the Ada programmers already know.


Hm, I find this to be a pretty mischaracterizing view of Rust. Nobody on the core team lives in California. We never talk about category theory. Our average age is mid-30s. And in general, we love hearing about other languages, including Ada.


We're using Rust in building safety-critical runtime software for autonomous vehicles precisely because we do care about these kinds of things for non-R&D products.

We have many experiments showing how trivially easy it is to write MISRA compliant C, that normally passes muster for "safety-critical" in automotive, which is horribly unsafe, but for which analogous Rust fails to even compile.

We're also working to go many steps beyond ISO 26262 in terms of process and process verification. To the point that we're going to attempt to have a formally verified development lifecycle in addition to as much of the software that comes out of it being formally verified as well.

We're not stopping at formal verification for the software or process either due to fairly glaring gaps/shortcomings in the methods available today.


If we are talking about the community of users, the experiences of Ada programmers are likely of no little help to someone working with Haskell. Ada is an imperative language with explicit declarations and mutation everywhere. Its mechanims to help out with safety basically have to do with managing side effects.


> I'm always surprised by how thoroughly uninterested the Haskell and Rust communities are in learning from the Ada/High Integrity Software community.

If you read the paper you would find that the VAST majority of issues were human communication or understanding of the problem. No programming language can fix that.

Rust was started with one overriding goal: make programming on Firefox manageable. And they identified a primary problem: uncontrolled sharing. And they killed it: Rust disallows sharing by default. Everything else in Rust stems from that. "category theory" or any other academic CS is used when it helps the primary mission--otherwise it gets deferred.

> Maybe eventually the valley bros will rediscover most of what the Ada programmers already know.

And yet Ada exists practically nowhere that requires timely deliverables. Funny that.

Much like Lisp, if Ada were such a force multiplier, there would be someone who would use it to make lots of money.


A few years ago, AdaCore's Robert Dewar observed that nobody has ever been killed by a flaw in Avonics software. That's perhaps not a good elevator pitch for a hockey stick startup but it's a good testament to the capabilities and skills of the people in the High Integrity community.

It's true that High Integrity development is not compatible with deadline or budget driven projects.

But there is a lot to learn from the High Integrity community and I think it's a shame that people who claim to be interested in making software more reliable ignore a community with decades of experience doing just that.


> A few years ago, AdaCore's Robert Dewar observed that nobody has ever been killed by a flaw in Avonics software.

While that may be technically correct, I would consider the crash of Air France Flight 447 to be partially an avionics software failure.

Responding to an inconsistent airspeed measurement by disconnecting the autopilot and then dropping into a weird, modal operating state (alternate law) and throwing control over to the very surprised humans counts as a software failure in my book. Having a stall warning that tells you to do the wrong thing is a software failure in my book (the stall warning turned off when inputs were invalid, but then turned back on when the pilots actually made the correct maneuvers because the inputs weren't invalid anymore).

While ultimately the failure for that flight was human error, a smart reaction by the software at any point would have prevented that tragedy. The biggest "smart reaction" would have been to flag the invalid airspeed to humans but don't change anything.

Whoever thought that dropping a suddenly dynamic system into the hands of surprised humans was a useful action should be shot. In reality, nobody thought it. Each individual subsystem had their own failure procedures, and nobody ever tested what happened when they interacted.


> partially an avionics software failure... Responding to an inconsistent airspeed measurement by disconnecting the autopilot and then dropping into a weird, modal operating state

You could write that software in rust to do exactly the same thing.


Quoting myself upthread:

> If you read the paper you would find that the VAST majority of issues were human communication or understanding of the problem. No programming language can fix that.

At no point did I argue that Rust would have prevented the Air France Flight 447 kind of failure. However, neither would Ada have prevented this kind of failure.

I WAS however taking issue with the quoted "nobody has ever been killed by a flaw in Avonics software".


> Avonics software

It's not the software that killed people it's the spec.


Welcome to the entire basis of SAE Level-3 autonomy. Yes, it does often seem fairly silly.


> And yet Ada exists practically nowhere that requires timely deliverables. Funny that.

Yes, the people who prioritize "working" over "correct" make sloppy mistakes and avoid the languages that would make them be less sloppy.

> if Ada were such a force multiplier, there would be someone who would use it to make lots of money.

The embedded world sends its regards.


Ada exists where killing people is not an option for sloppy programming.

The moment software companies start to actually pay heavy fines and are forced to do refunds for sloppy software like in other industries, the situation will change.


Probably an advantage of Ada vs other languages, hard to find a sloppy Ada programmer.


Can anyone recommend any links/articles/books about the relationships between specification, implementation, testing, provability, TDD, BDD, etc.?

I have been working on designing some software for improving the specifications process, and quickly realized that it's a very interconnected concept: the specification can be treated very formally, leading to things like BDD (behavior-driven development), but also to things like formal provability.

I'm generally interested in the relationships/processes that mediate between design <-> specification <-> actual programming. In reality, there's a lot of feedback, and I want to create ways of radically improving these processes.


It looks like you are looking for the V-Model development process used in the industry (e.g. automotive).

A typical requirement in this model is handled like this: 1. the high level specification define what is the change about (e.g. implement a hillholder function). 2. architecture phase: you identify which part/module of the system are impacted by the high level requirement. You define what each part will do and you specify how they interface. 3. detailed design phase: each part is formally specified, in the automotive industry we typically use Model based development (Simulink) to specify this phase. 4. implementation: actual coding being done, if you use Simulink this is done by the Simulink/dSpace. A unit test is then performed to check that the detailed design from part 3 has been correctly done. 5. Integration and test: all parts are collected and compiled, and we look that the interfaces are matching. 6. System test: all parts are now tested together against the specifications done in the architecture phase (part 2) and part 1

In the automotive industry, each step can be done by a different person/team/company thus the documentation done in each phase is extremely important to avoid finger pointing in case a problem is detected after delivery.


Excellent, I knew there had to be a ton of history here, but I hadn't known about this specifically. Thank you!


Oh—also—do you know what software out there is already used for managing this complexity? Thanks again!


I've used DOORS. It was adequate, though not a pleasure to use. (It might have been a pleasure if the alternative was doing it manually...)


Having done it manually, DOORS is a dream.

I haven’t used a recent incarnation of it though. It’s UI circa 2008-2010 was entirely mediocre but sufficient for the task.


I think Product Lifecycle Management (PLM) is the buzzword your looking for.


PLM I'm familiar with, though none of the ones I've seen seem to focus in any particular was on the requirements/specification end of the equation...


JAMA is a more recent one that's fairly modern feeling. I tried to get my company to get it but they didn't bit. (pricey)


Thank you for this--extremely relevant! This is very very close to what I've been looking for / researching...


Ah okay. So PLM systems would be used to store and manage the requirements, the requirement documents are going to be, at least in my corner of the world... Word and/or Excel templates.


Which is only narrow subset of what PLM system does. PLM is generally about tracking what data artifacts (drawings, manufacturer datasheets and so, formal specifications are somewhat secondary to that) are relevant for given assembly and how such subassemblies fit together on high level.


Yes, that's much more of what I am aware of in the context of PLM. As I wrote in a sibling comment, I'm interested in improving the storage and representation of the requirements/spec itself...


Right, and this is actually exactly the area that I am interesting in improving: providing a canonical, systematic way to store and represent the actual requirements & specifications, and provide ways to feed into other software such as PLM or project management, etc.


On my corner of the world it would UML, using tools like Enterprise Architect.


If you search for the SEL4 kernel, or the L4 family in general, there's a fair number of papers and presentations on their activity in this area. I don't know if I would characterize it as a particularly fast development process though.

https://en.wikipedia.org/wiki/L4_microkernel_family


Design to specification can be handled using systems like DOORS or other requirements management software. There’s an interchange format (XML) that many of these support called ReqIF. If you look that up you’ll find an Eclipse based tool (RMF) that is free and let’s you see how linking between requirements and such can be done.

I’ve not seen tracing attempted down to the code level though we did do tracing to the test procedures.

There’s a plug-in for Event-B in Eclipse that can, in theory, play well with RMF (connect requirements and specs to elements of the formal model). I’ve not spent much time with it but it did seem to do the job.


Ah ha, this is exactly the kind of stuff that I knew must be out there, I but had to find it. Thank you, internet stranger!


No problem. I’m about to embark, with my sister, on a project that will benefit by interacting with these system so I’ve been researching it.


The thing the specs have in common with your code is they represent entities involved in the systems operation internally or externally to as abstract or concrete detail as you require. They also typically represent the structure and/or order of your system's activities. The abstractions that hide messy details of the machine can let you more easily analyze properties of your system with your eyes, spec/model-checkers, or proof. Some can generate tests from specs. Then, the code's modules should map closely to those abstract actions so you mainky just have to analyze code for isdues that just show up in those parts.

The easiest method to start with is Design by Contract plus property-based and fuzz testing. By itself, it lets you specify key properties that are highlighted during a test or runtime failure. Combined with SPARK Ada, you can prove the code is correct against those specs.

https://www.eiffel.com/values/design-by-contract/introductio...

http://www.anthonyhall.org/c_by_c_secure_system.pdf

https://en.m.wikipedia.org/wiki/SPARK_(programming_language)


You might be interested in this study as a way of refining your interests and goals:

http://loonwerks.com/publications/pdf/cofer2013fmics.pdf

It's a big world out there; this has been an active area of research basically since Turing. Many of the "relationship between" questions you ask have their own conference or workshop series.

> formal provability

IMO the best way to start down this road is to just begin using some of the tools out there -- TLA+, Coq, whatever - and touch base with the community around your choice of tool (conferences, workshops, or even going back to school for a phd). The best way to learn about the strengths and limitations of current software practice is to sit down and churn out code, preferably with a strong mentor. The same is true for proof programming.


Strange how whatever Adrian Colyer covers in his The Morning Paper makes its way here. People perfer posting the original paper rather than his blogs posts.


This happens because the HN submission guidelines at https://news.ycombinator.com/newsguidelines.html say:

“Please submit the original source. If a post reports on something found on another site, submit the latter.”

The main objective is to highlight and share interesting research, and if a post on ‘The Morning Paper’ achieves that and promotes informative discussions like the ones in this thread, then I’m happy.

On a good day, I like to think there’s enough in my posts that the commentary does qualify as an “original source.” On a bad day, the post may be a more straightforward summary of the paper content (though I’ve occasionally tried passing the text of a paper through an auto-summariser for fun, and let’s just say it doesn’t look like I’m going to be out of a job anytime soon!).

For example, the post that presumably inspired this HN thread (the timing certainly suggests that) is more a straightforward summary: https://blog.acolyer.org/2017/12/01/analyzing-software-requi.... The post from the day before on a related topic is interwoven with much more personal commentary: https://blog.acolyer.org/2017/11/30/the-role-of-software-in-....

Even in the ‘straightforward summary’ case, I will typically have spent a couple of hours or more reading the original paper, trying to distil the key points and putting them across succinctly. (It’s not for me to judge whether or not I succeed at that, but this is the aim!).

My hypothesis is that more people have time to read a long-ish slightly informal blog post than they do to scan a 12-20 page research paper. And it would be shame if when presented with only the link to the original paper pdf, they miss out on some of the key ideas within it because it feels like too much effort to read or scan the paper when presented like that. For one paper I’ll be covering next week for example (and this is an outlier), I spent about 5 hours in total on reading, trying to understand, getting the background and context clear, and then writing it up.

In those cases when the original HN link is to the full paper pdf rather than to my post, then I guess an easy way to give readers the benefit of both is simply a comment in the thread pointing to the ‘Morning Paper’ summary... The main thing though, as I said at the top, is that interesting and thought-provoking research reaches a bigger audience.


Thanks for taking out the time to write such an elaborate clarification, Mr Colyer. I was unaware of the guidelines until you brought them to my attention. I myself am quite an avid reader of The Morning Paper, and was initially taken aback to see that people post the original paper after reading your blog, and don't mention you anywhere. It kind of didn't feel right to me. But now after reading your explaination, I am okay. Thanks again :)




Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: