Creating High-Confidence, Dependable Software
Creating high confidence,
highly dependable,
critical software
Roger L. Costello
October 15, 2017
View the “Notes” section
•
I added notes under each slide.
•
Be sure to read the notes.
Traditional approach
•
Test the heck out of it.
•
Microsoft: One tester for every developer
•
Verification
•
Mathematical theorem-proving techniques
•
Follow a formal certification process.
•
Aeronautical software: follow the DO-178C process
Testing to produce dependable software
Acknowledgement: this diagram is from Greg Dennis’ Ph.D dissertation.
Certification process to produce dependable
software
•
DO-178C, Software Considerations in Airborne Systems and
Equipment Certification
is the primary document by which the
certification authorities such as FAA, approve all commercial
software-based aerospace systems.
•
IEC 60880
provides requirements for the purpose of achieving highly
reliable nuclear software.
Model of an aircraft
Model of software
software
(application)
model of the
software
MIT Professor Daniel Jackson created Alloy for
making software models
Alloy = “lightweight formal modeling”
http://www.cs.cornell.edu/conferences/formalnetworks/pamela-slides-i.pdf
Traditional testing
Alloy analysis
Creating software that is highly dependable
Testing
Certification process
Software model and analysis (Alloy)
Dependable software
Acknowledgement
•
Much of the information in these slides come from these sources:
•
The book
Software Abstractions
by Daniel Jackson.
•
The
National Academy of Sciences book
(see 2 slides back).
•
Greg Dennis’ Ph.D dissertation
.
For the last year I’ve been interested in how to make software more dependable, how to have more confidence in our software. I’d like to share with you some of the things I’ve learned.
This content delves into the traditional approach and testing methods to ensure the production of dependable software, emphasizing certification processes like DO-178C. It highlights the importance of models in software development, such as Alloy by MIT Professor Daniel Jackson. Explore the journey towards highly reliable software creation through rigorous testing and formal modeling.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Creating high confidence, highly dependable, critical software Roger L. Costello October 15, 2017
View the Notes section I added notes under each slide. Be sure to read the notes.
Traditional approach Test the heck out of it. Microsoft: One tester for every developer Verification Mathematical theorem-proving techniques Follow a formal certification process. Aeronautical software: follow the DO-178C process
Acknowledgement: this diagram is from Greg Dennis Ph.D dissertation.
Certification process to produce dependable software DO-178C, Software Considerations in Airborne Systems and Equipment Certification is the primary document by which the certification authorities such as FAA, approve all commercial software-based aerospace systems. IEC 60880 provides requirements for the purpose of achieving highly reliable nuclear software.
Model of software model of the software software (application)
MIT Professor Daniel Jackson created Alloy for making software models
Alloy = lightweight formal modeling http://www.cs.cornell.edu/conferences/formalnetworks/pamela-slides-i.pdf
Traditional testing Alloy analysis
Creating software that is highly dependable Testing Certification process Dependable software Software model and analysis (Alloy)
Acknowledgement Much of the information in these slides come from these sources: The book Software Abstractions by Daniel Jackson. The National Academy of Sciences book (see 2 slides back). Greg Dennis Ph.D dissertation.
