Document Open Access Logo

Toward a Dependability Case Language and Workflow for a Radiation Therapy System

Authors Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, Xi Wang

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2015.103.pdf
  • Filesize: 7.69 MB
  • 10 pages

Document Identifiers

Author Details

Michael D. Ernst
Dan Grossman
Jon Jacky
Calvin Loncaric
Stuart Pernsteiner
Zachary Tatlock
Emina Torlak
Xi Wang

Cite AsGet BibTex

Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang. Toward a Dependability Case Language and Workflow for a Radiation Therapy System. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 103-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.SNAPL.2015.103

Abstract

We present a near-future research agenda for bringing a suite of modern programming-languages verification tools - specifically interactive theorem proving, solver-aided languages, and formally defined domain-specific languages - to the development of a specific safety-critical system, a radiotherapy medical device. We sketch how we believe recent programming-languages research advances can merge with existing best practices for safety-critical systems to increase system assurance and developer productivity. We motivate hypotheses central to our agenda: That we should start with a single specific system and that we need to integrate a variety of complementary verification and synthesis tools into system development.
Keywords
  • Synthesis
  • Proof Assistants
  • Verification
  • Dependability Cases
  • Domain Specific Languages
  • Radiation Therapy

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. John Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, April 2003. Google Scholar
  2. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. Formal certification of code-based cryptographic proofs. In Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL), pages 90-101, Savannah, GA, January 2009. Google Scholar
  3. Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. A static analyzer for large safety-critical software. In PLDI, pages 196-207, San Diego, CA, June 2003. Google Scholar
  4. Adam Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI'11 [32], pages 234-245. Google Scholar
  5. Coq development team. Coq Reference Manual, Version 8.4pl5. INRIA, October 2014. URL: http://coq.inria.fr/distrib/current/refman/.
  6. National Research Council, Daniel Jackson, and Martyn Thomas. Software for Dependable Systems: Sufficient Evidence? National Academy Press, Washington, DC, USA, 2007. Google Scholar
  7. Simon Cruanes, Grégoire Hamon, Sam Owre, and Natarajan Shankar. Tool integration with the evidential tool bus. In Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni, editors, VMCAI, volume 7737 of Lecture Notes in Computer Science, pages 275-294. Springer, 2013. Google Scholar
  8. Anne Dardenne, Axel van Lamsweerde, and Stephen Fickas. Goal-directed requirements acquisition. In Selected Papers of the Sixth International Workshop on Software Specification and Design, 6IWSSD, pages 3-50, Amsterdam, The Netherlands, The Netherlands, 1993. Elsevier Science Publishers B. V. Google Scholar
  9. Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. Commun. ACM, 22(5):271-280, May 1979. Google Scholar
  10. Greg Dennis, Robert Seater, Derek Rayside, and Daniel Jackson. Automating commutativity analysis at the design level. In Proceedings of the 2004 International Symposium on Software Testing and Analysis, pages 165-174, Boston, MA, July 2004. Google Scholar
  11. EPICS. URL: http://www.aps.anl.gov/epics/.
  12. Galois. URL: http://galois.com.
  13. Gerard J. Holzmann. The power of 10: Rules for developing safety-critical code. Computer, 39(6):95-97, June 2006. Google Scholar
  14. Gerard J. Holzmann. Mars code. Commun. ACM, 57(2):64-73, February 2014. Google Scholar
  15. Daniel Jackson. A direct path to dependable software. Commun. ACM, 52(4):78-88, April 2009. Google Scholar
  16. Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, February 2012. Google Scholar
  17. Daniel Jackson and Eunsuk Kang. Property-part diagrams: A dependence notation for software systems. Technical report, Massachusetts Institute of Technology, 2009. URL: http://hdl.handle.net/1721.1/61343.
  18. Michael Jackson. Problem Frames: Analysing and Structuring Software Development Problems. Addison-Wesley, 2001. Google Scholar
  19. Jonathan Jacky. Formal safety analysis of the control program for a radiation therapy machine. In Wolfgang Schlegel and Thomas Bortfeld, editors, The Use of Computers in Radiation Therapy, pages 68-70. Springer Berlin Heidelberg, 2000. Google Scholar
  20. Jonathan Jacky. EPICS-based control system for a radiation therapy machine. In International Conference on Accelerator and Large Experimental Physics Control Systems (ICALEPCS), 2013. Google Scholar
  21. Jonathan Jacky and Ruedi Risler. Clinical neutron therapy system reference manual. Technical Report 99-10-01, University of Washington, Department of Radiation Oncology, 2002. Google Scholar
  22. Jonathan Jacky and Ruedi Risler. Clinical neutron therapy system therapist’s guide. Technical Report 99-07-01, University of Washington, Department of Radiation Oncology, 2002. Google Scholar
  23. Jonathan Jacky, Ruedi Risler, David Reid, Robert Emery, Jonathan Unger, and Michael Patrick. A control system for a radiation therapy machine. Technical Report 2001-05-01, University of Washington, Department of Radiation Oncology, 2001. Google Scholar
  24. Dongseok Jang, Zachary Tatlock, and Sorin Lerner. Establishing browser security guarantees through formal shim verification. In Proceedings of the 21st Usenix Security Symposium, pages 113-128, Bellevue, WA, August 2012. Google Scholar
  25. Eunsuk Kang and Daniel Jackson. Formal modeling and analysis of a flash filesystem in Alloy. In Proceedings of the 1st International Conference on Abstract State Machines, B and Z, ABZ'08, pages 294-308, Berlin, Heidelberg, 2008. Springer-Verlag. Google Scholar
  26. Tim Kelly and Rob Weaver. The goal structuring notation - a safety argument notation. In Proceedings of the Dependable Systems and Networks 2004 Workshop on Assurance Cases, July 2004. Google Scholar
  27. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Michael Norrish, Rafal Kolanski, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207-220, Big Sky, MT, October 2009. Google Scholar
  28. Kevin Lano. The B Language and Method: A Guide to Practical Formal Development. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1st edition, 1996. Google Scholar
  29. Vu Le, Mehrdad Afshari, and Zhendong Su. Compiler validation via equivalence modulo inputs. In PLDI'14 [33], pages 216-226. Google Scholar
  30. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, July 2009. Google Scholar
  31. Joseph P. Near, Aleksandar Milicevic, Eunsuk Kang, and Daniel Jackson. A lightweight code analysis and its role in evaluation of a dependability case. In Proceedings of the 33rd International Conference of Computer Safety, Reliability and Security, pages 31-40, Waikiki, Honolulu, HI, May 2011. Google Scholar
  32. Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), San Jose, CA, June 2011. Google Scholar
  33. Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Edinburgh, UK, June 2014. Google Scholar
  34. Tahina Ramananandro. Mondex, an electronic purse: Specification and refinement checks with the alloy model-finding method. Form. Asp. Comput., 20(1):21-39, December 2007. Google Scholar
  35. J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1989. Google Scholar
  36. Emina Torlak and Rastislav Bodik. Growing solver-aided languages with Rosette. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, Onward! 2013, pages 135-152, Indianapolis, IN, 2013. Google Scholar
  37. Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI'14 [33], pages 530-541. Google Scholar
  38. Richard Uhler and Nirav Dave. Smten with satisfiability-based search. In Proceedings of the 2014 Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 157-176, Portland, OR, October 2014. Google Scholar
  39. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and understanding bugs in C compilers. In PLDI'11 [32], pages 283-294. Google Scholar
  40. Pamela Zave. Using lightweight modeling to understand Chord. SIGCOMM Comput. Commun. Rev., 42(2):49-57, March 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact