MISRA related document - safety and security on c and c++

「MISRA-C」で検索した。

人名ではなく題材としてMISRA_C、MISRA_C++については４文献。
CERT Cだとこのうちの１文献。

STARC RTL Design style guideだと0件。
verilog HDLで１６件だから、スタイルガイドまで手が回っていない感じ。

MISRA C:2012は、発行後、公式の掲示板で質疑の記録があり、
日本から３０件の意見が出ていて、かなりの部分がCorrigendumで訂正済である。
https://www.misra.org.uk/forum/viewforum.php?f=214&sid=69f12d55e53ec28c352d0b1dd1ce2ee6

Arxivの４件を拝読して、課題を順次追記中。

なお、URLを追記している。
->の記号の資料は、文献中にあるURLよりも良さげなものを記載。

1

MISRA C, for Security's Sake!
Roberto Bagnara
https://arxiv.org/pdf/1705.03517.pdf, 2017

唯一CERT Cについて書いている。

自分はトンネルを掘る方が専門で防ぐ方が専門でない。
CERT Cのbibliographyのリンク切れを修正したことがある。
https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography

2

The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software
Roberto Bagnara, Abramo Bagnara, Patricia M. Hill
https://arxiv.org/abs/1809.00821, , 2018

misra.c

uint32_t i = 1;
i = i << 32; /* Undefined behavior. */

3

Extending a User Interface Prototyping Tool with Automatic MISRA C Code Generation
Gioacchino Mauro, Harold Thimbleby, Andrea Domenici, Cinzia Bernardeschi
https://arxiv.org/pdf/1701.08468.pdf, 2017

4

BARR-C:2018 and MISRA C:2012: Synergy Between the Two Most Widely Used C Coding Standards
Roberto Bagnara, Michael Barr, Patricia M. Hill
https://arxiv.org/pdf/2003.06893.pdf, 2020

Coding standardというよりは、その運用方法の例という感じ。

reference 1

[1] A. Avizienis, J.-C. Laprie, B. Randell, and C. Landwehr. Basic concepts and taxonomy of dependable and secure computing. IEEE Trans- actions on Dependable and Secure Computing, 1(1):11–33, 2004.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.219.5446&rep=rep1&type=pdf

[2] CERT. SEI CERT C Coding Standard: Rules for Developing Safe, Reliable, and Secure Sys- tems. Software Engineering Institute, Carnegie Mellon University, 2016 edition, 2016.
https://resources.sei.cmu.edu/downloads/secure-coding/assets/sei-cert-c-coding-standard-2016-v01.pdf

[3] K. M. Goertzel and L. Feldman. Software survivability: Where safety and security converge. In AIAA Infotech@Aerospace Conference 2009, Seattle, Washington, 2009. American Institute of Aeronautics and Astronautics.
https://www.academia.edu/1383715/Software_Survivability_Where_Safety_and_Security_Converge?auto=download
[4] ISO/IEC. ISO/IEC TS 17961:2013, Informa- tion technology — Programming languages, their environments & system software interfaces — C Secure Coding Rules. ISO/IEC, Geneva, Switzer- land, November 2013.
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1624.pdf

[5] MISRA. MISRA-C:2012 — Guidelines for the use of the C language in critical systems. MIRA Limited, Nuneaton, Warwickshire, UK, March 2013.
https://www.misra.org.uk/forum/viewforum.php?f=214&sid=69f12d55e53ec28c352d0b1dd1ce2ee6

[6] MISRA. MISRA C:2012 Addendum 2 — Cov- erage of MISRA C:2012 against ISO/IEC TS 17961:2013 “C Secure”. HORIBA MIRA Lim- ited, Nuneaton, Warwickshire, UK, April 2016.
https://www.misra.org.uk/forum/viewtopic.php?f=241&t=1841

[7] MISRA. MISRA C:2012 Amendment 1 — Ad- ditional security guidelines for MISRA C:2012. HORIBA MIRA Limited, Nuneaton, Warwick- shire, UK, April 2016.
https://www.misra.org.uk/forum/viewtopic.php?f=241&t=1564

[8] R. C. Seacord. The CERT C Secure Coding Standard. Addison-Wesley, 2008.

[9] R. C. Seacord. The CERT C Coding Standard: 98 Rules for Developing Safe, Reliable, and Se- cure Systems. Addison-Wesley, second edition, 2014.

[10] R. C. Seacord. Safety and security coding standards for C. Engineering & Technology Reference, 2016. DOI: 10.1049/etr.2016.0024.
https://digital-library.theiet.org/content/reference/10.1049/etr.2016.0024

reference 2

[1] Bagnara, R.: MISRA C, for security’s sake! In: Lami, G. (ed.) Informal pro- ceedings of the 14th Workshop on Automotive Software & Systems. Milan, Italy (2016), available at http://www.automotive-spin.it/. Also published as Report arXiv:1705.03517 [cs.SE], available at http://arxiv.org/

[2] Banks, A.: MISRA C — recent developments and a road map to the future. Presentation slides available at http://www.his-2018.co.uk/session/misra-c-updates-2016 (Nov 2016), presented at the High Integrity Software Conference 2016, Bristol, UK, November 1, 2016

-> https://www.slideshare.net/AdaCore/misra-c-recent-developments-and-a-road-map-to-the-future

[3] Barr, M.: Embedded C Coding Standard. Barr Group, Germantown, MD, USA (2013)
https://barrgroup.com/embedded-systems/books/embedded-c-coding-standard

[4] BarrGroup,Germantown,MD,USA:Embedded Systems Safety & Security Survey (Feb 2018), available at http://www.barrgroup.com/

-> https://barrgroup.com/sites/default/files/barr_c_coding_standard_2018.pdf

[5] Baudin, P., Cuoq, P., Filliˆatre, J.C., March ́e, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, version 1.13 edn. (2018)
https://frama-c.com/download/acsl_1.13.pdf

[6] CERT:SEI CERT C Coding Standard:Rules for Developing Safe, Reliable, and Secure Systems. Software Engineering, Carnegie Mellon University, 2016 edn. (2016)

[7] Cousot, P., Cousot, R., Feret, J., Min ́e, A., Mauborgne, L., Monniaux, D., Ri- val, X.: Varieties of static analyzers: A comparison with ASTREE. In: First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007). pp. 3–20. IEEE Computer Society, Shanghai, China (Jun 2007)
https://www.researchgate.net/publication/4255150_Varieties_of_Static_Analyzers_A_Comparison_with_ASTREE

[8] Crocker, D., Carlton, J.: Verification of C programs using automated reasoning. In: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007). pp. 7–14. IEEE Computer Society, London, UK (2007)
https://www.researchgate.net/publication/4279187_Verification_of_C_Programs_Using_Automated_Reasoning

[9] Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-
based modular verification of concurrent C. In: 31st International Conference on Software Engineering (ICSE 2009), Companion Volume. pp. 429–430. IEEE Computer Society, Vancouver, Canada (2009)
https://www.microsoft.com/en-us/research/wp-content/uploads/2008/01/VCCContractBasedVerificationdraft08.pdf

[10] Gosling, J., Joy, B., Steele, G.L., Bracha, G., Buckley, A.: The Java Language Specification: Java SE 8 Edition. Java Series, Addison-Wesley, Upper Saddle River, NJ, USA, 5th edn. (2014)

[11] Hatton, L.: Safer C: Developing Software for High-Integrity and Safety-Critical Systems. McGraw-Hill, Inc., New York, NY, USA (1995)
https://www.amazon.co.jp/Safer-High-Integrity-Safety-Critical-McGraw-Hill-International/dp/0077076400

[12] Intel Corporation: Intel 64 and IA-32 Architectures Software Developer’s Manual — Volume 2 (2A, 2B, 2C & 2D): Instruction Set Reference, A-Z (2018)
https://software.intel.com/content/www/us/en/develop/download/intel-64-and-ia-32-architectures-sdm-combined-volumes-1-2a-2b-2c-2d-3a-3b-3c-3d-and-4.html

[13] ISO: ISO 26262:2011: Road Vehicles — Functional Safety. ISO, Geneva, Switzer- land (Nov 2011)

[14] ISO/IEC: ISO/IEC 9899:1990: Programming Languages — C. ISO/IEC, Geneva, Switzerland (1990)

[15] ISO/IEC: ISO/IEC 9899:1990/AMD 1:1995: Programming Languages — C. ISO/IEC, Geneva, Switzerland (1995)

[16] ISO/IEC: ISO/IEC 9899:1999: Programming Languages — C. ISO/IEC, Geneva, Switzerland (1999)

[17] ISO/IEC: ISO/IEC 9899:1999/Cor 3:2007: Programming Languages — C. ISO/IEC, Geneva, Switzerland, Technical Corrigendum 3 edn. (2007)

[18] ISO/IEC: ISO/IEC 9899:2011: Programming Languages — C. ISO/IEC, Geneva, Switzerland (2011)

[19] ISO/IEC: ISO/IEC TS 17961:2013, Information technology — Programming lan- guages, their environments & system software interfaces — C Secure Coding Rules. ISO/IEC, Geneva, Switzerland (Nov 2013)

[20] ISO/IEC: ISO/IEC TS 17961:2016, Information technology — Programming languages, their environments & system software interfaces — C Secure Coding Rules. ISO/IEC, Geneva, Switzerland (Aug 2016)
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2010.htm

[21] Jacobs, B., Smans, J., Philippaerts, P., F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) Proceedings of NASA Formal Meth- ods — Third International Symposium (NFM 2011). Lecture Notes in Computer Science, vol. 6617, pp. 41–55. Springer, Pasadena, CA, USA (2011)
https://people.cs.kuleuven.be/~bart.jacobs/nfm2011.pdf

[22] Le Charlier, B. (ed.): Static Analysis, First International Static Analysis Symposium (SAS’94), Lecture Notes in Computer Science, vol. 864. Springer, Namur, Belgium (1994)
https://link.springer.com/book/10.1007/3-540-58485-4

[23] Motor Industry Software Reliability Association: MISRA-C:1998 — Guidelines for the use of the C language in vehicle based sofware. MIRA Ltd, Nuneaton, War- wickshire CV10 0TU, UK (Jul 1998)

[24] Motor Industry Software Reliability Association: MISRA-C:2004 — Guidelines for the use of the C language in critical systems. MIRA Ltd, Nuneaton, Warwickshire CV10 0TU, UK (Oct 2004)

[25] MISRA: MISRA C:2012 — Guidelines for the use of the C language in critical systems. MIRA Ltd, Nuneaton, Warwickshire CV10 0TU, UK (Mar 2013)

[26] MISRA: MISRA C:2012 Amendment 1 — Additional security guidelines for MISRA C:2012. HORIBA MIRA Ltd, Nuneaton, Warwickshire CV10 0TU, UK (Apr 2016)

[27] MISRA: MISRA Compliance:2016 — Achieving compliance with MISRA Coding Guidelines. HORIBA MIRA Ltd, Nuneaton, Warwickshire CV10 0TU, UK (Apr 2016)

[28] MISRA: MISRA C:2012 Technical Corrigendum 1 — Technical clarification of MISRA C:2012. HORIBA MIRA Ltd, Nuneaton, Warwickshire CV10 0TU, UK (Jun 2017)
https://www.misra.org.uk/forum/viewtopic.php?f=241&t=1670

[29] MISRA: MISRA C:2012 Addendum 2 — Coverage of MISRA C:2012 (including Amendment 1) against ISO/IEC TS 17961:2013 “C Secure”. HORIBA MIRA Ltd, Nuneaton, Warwickshire CV10 0TU, UK, 2nd edn. (Jan 2018)

[30] MISRA: MISRA C:2012 Addendum 3 — Coverage of MISRA C:2012 (including Amendment 1) against CERT C 2016 Edition. HORIBA MIRA Ltd, Nuneaton, Warwickshire CV10 0TU, UK (Jan 2018)
https://www.misra.org.uk/forum/viewtopic.php?f=241&t=1709
[31] Motor Industry Software Reliability Association: MISRA C++:2008 — Guidelines for the use of the C++ language in critical systems. MIRA Ltd, Nuneaton, War- wickshire CV10 0TU, UK (Jun 2008)

[32] N ́elis, V., Yomsi, P.M., Pinho, L.M.: The variability of application execution times on a multi-core platform. In: Schoeberl, M. (ed.) Proceedings of the 16th Inter- national Workshop on Worst-Case Execution Time Analysis (WCET 2016). OASICS, vol. 55, pp. 6:1–6:11. Schloss Dagstuhl — Leibniz-Zentrum fu ̈r Informatik, Toulouse, France (2016)
https://drops.dagstuhl.de/opus/volltexte/2016/6899/pdf/OASIcs-WCET-2016-6.pdf

[33] Nowotsch, J., Paulitsch, M.: Leveraging multi-core computing architectures in avionics. In: Constantinescu, C., Correia, M.P. (eds.) Proceedings of the Ninth European Dependable Computing Conference (EDCC 2012). pp. 132–143. IEEE Computer Society, Sibiu, Romania (2012)
https://ieeexplore.ieee.org/document/6214768

[34] Nowotsch, J., Paulitsch, M., Buhler, D., Theiling, H., Wegener, S., Schmidt, M.: Multi-core interference-sensitive WCET analysis leveraging runtime resource capacity enforcement. In: Proceedings of the 26th Euromicro Conference on Real- Time Systems (ECRTS 2014). pp. 109–118. IEEE Computer Society, Madrid, Spain (2014)
https://www.researchgate.net/publication/286592702_Multi-core_Interference-Sensitive_WCET_Analysis_Leveraging_Runtime_Resource_Capacity_Enforcement

[35] Philippaerts, P., Mu ̈hlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: Industrial case studies. Science of Computer Programming 82, 77–97 (2014)
https://www.sciencedirect.com/science/article/pii/S0167642313000191

[36] Rainer-Harbach, M.:Methods and Tools for the Formal Verification of Software:An Analysis and Comparison. Master’s thesis, Fakult ̈at fu ̈r Informatik der Technischen Universit ̈at Wien, Wien, Austria (Nov 2011)
https://www.ac.tuwien.ac.at/files/pub/rainer-harbach_11.pdf

[37] Ritchie, D.M.: The development of the C language. SIGPLAN Notices 28(3), 201– 208 (Mar 1993)
https://www.bell-labs.com/usr/dmr/www/chist.html
http://heim.ifi.uio.no/inf2270/programmer/historien-om-C.pdf

[38] Signoles, J.: EACSL: Executable ANSI/ISO C Specification Language, version 1.12 edn. (2018)
Version 1.5-3
http://www.open-do.org/wp-content/uploads/2011/05/e-acsl.pdf

[39] Software Engineering Center: Embedded System Development Coding Reference: C Language Edition. Information-Technology Promotion Agency, Japan (Jul 2014), version 2.0
https://www.ipa.go.jp/files/000065271.pdf

reference 3

[1] Motor Industry Software Reliability Association (1998): Guidelines for the Use of the C Language in Vehicle Based Software. Motor Industry Research Association.

[2] Ayan Banerjee & Sandeep K. S. Gupta (2014): Model Based Code Generation for Medical Cyber Physical Systems. In: 1st Workshop on Mobile Medical Applications (MMA ’14), pp. 22–27, doi:10.1145/2676431.2676646.
https://asu.pure.elsevier.com/en/publications/model-based-code-generation-for-medical-cyber-physical-systems

[3] M. Beine, R. Otterbach & M. Jungmann (2004): Development of safety-critical software using automatic code generation. Technical Report, SAE Technical Papers, doi:10.4271/2004-01-0708.
https://www.sae.org/publications/technical-papers/content/2004-01-0708/

[4] C. Bernardeschi, L. Cassano, A. Domenici & L. Sterpone (2013): Unexcitability Analysis of SEUs Affecting the Routing Structure of SRAM-based FPGAs. In: Proc. of the 23rd ACM Great Lakes Symposium on VLSI, GLSVLSI ’13, pp. 7–12, doi:10.1145/2483028.2483050.
https://dl.acm.org/doi/abs/10.1145/2483028.2483050

[5] Cinzia Bernardeschi, Paolo Masci & Holger Pfeifer (2008): Early Prototyping of Wireless Sensor Network Algorithms in PVS, pp. 346–359. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-540- 87698-4_29.

[6] J. Bowen & A. Hinze (2011): Supporting Mobile Application Development with Model-Driven Emulation. In: Formal Methods for Interactive Systems 2011, Electr. Comm. EASST 45, doi:10.14279/tuj.eceasst.45.634.
https://journal.ub.tu-berlin.de/eceasst/article/view/634/656

[7] J. Bowen & S. Reeves (2012): Modelling User Manuals of Modal Medical Devices and Learning from the Experience. In: 4th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS ’12), pp. 121–130, doi:10.1145/2305484.2305505.
https://dl.acm.org/doi/abs/10.1145/2305484.2305505

[8] J. Bowen & S. Reeves (2015): Design Patterns for Models of Interactive Systems. In: 24th Australasian Software Engineering Conference (ASWEC), IEEE, pp. 223–232, doi:10.1109/ASWEC.2015.30.
https://researchcommons.waikato.ac.nz/bitstream/handle/10289/9842/Bowen-Reeves-p12.pdf?sequence=2

[9] A. Cerone, P. Curzon, J. Bowen & S. Reeves (2007): Formal Models for Informal GUI Designs. Electronic Notes in Theoretical Computer Science 183, pp. 57–72, doi:10.1016/j.entcs.2007.01.061.
https://www.sciencedirect.com/science/article/pii/S1571066107004288

[10] Guiran Chang, Chunguang Tan, Guanhua Li & Chuan Zhu (2010): Developing Mobile Applications on the Android Platform. In: Mobile Multimedia Processing, pp. 264–286, doi:10.1007/978-3-642-12349-8_15.
https://link.springer.com/chapter/10.1007/978-3-642-12349-8_15

[11] T. Erkkinen & M. Conrad (2007): Safety-critical software development using automatic production code generation. Technical Report, SAE Technical Papers, doi:10.4271/2007-01-1493.
https://www.researchgate.net/publication/228749528_Safety-Critical_Software_Development_Using_Automatic_Production_Code_Generation
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.471.5369&rep=rep1&type=pdf

[12] J.Fitzgerald, P.G.Larsen, P.Mukherjee, N.Plat&M.Verhoef(2005): Validated Designs For Object-oriented Systems. Springer-Verlag TELOS, Santa Clara, CA, USA.
https://www.amazon.com/Validated-Designs-Object-oriented-Systems-Fitzgerald/dp/1852338814

[13] J. D. Foley & P. Noi Sukaviriya (1994): History, Results, and Bibliography of the User Interface Design Environment (UIDE), an Early Model-based System for User Interface Design and Implementation. In: Proceedings of Design, Verification and Specification of Interactive Systems (DSVIS’94), pp. 3–14, doi:10.1007/978-3-642-87115-3_1.
https://link.springer.com/chapter/10.1007/978-3-642-87115-3_1

[14] (2016): Handlebars Semantic Template. Available at http://handlebarsjs.com.

[15] M. D. Harrison, J. C. Campos & P. Masci (2015): Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering 11(2), pp. 95–111, doi:10.1007/s11334- 013-0201-3.
https://www.ipa.go.jp/files/000065271.pdf

[16] MD. Harrison, JC. Campos, R. Rimvydas & P. Curzon (2016): Modelling information resources and their salience in medical device design. In: 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS ’16), doi:10.1145/2933242.2933250.
https://haslab.uminho.pt/jccampos/files/ocbeics16pub.pdf

[17] Campos JC & Harrison MD (2001): Model checking interactor specifications. Automated Software Engineer- ing 8(3–4), pp. 5275–310, doi:10.1023/A:1011265604021.
https://www.researchgate.net/publication/220136143_Model_Checking_Interactor_Specifications

[18] (2016): Java Native Interface. http://docs.oracle.com/javase/8/docs/technotes/guides/jni/.

[19] P. Masci, A. Ayoud, P. Curzon, MD. Harrison, I. Lee & H. Thimbleby (2013): Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, (EICS ’13), doi:10.1145/2494603.2480302.
https://haslab.uminho.pt/michaelharrison/files/mascietal.pdf

[20] P. Masci, P. Mallozzi, F. L. De Angelis, G. Di Marzo Serugendo & P. Curzon (2015): Using PVSio-web and SAPERE for rapid prototyping of user interfaces in Integrated Clinical Environments. In: Verisure2015, Workshop on Verification and Assurance, co-located with CAV2015.
https://www.researchgate.net/publication/278241299_Using_PVSio-web_and_SAPERE_for_rapid_prototyping_of_user_interfaces_in_Integrated_Clinical_Environments

[21] P. Masci, P. Oladimeji, P. Curzon & H. Thimbleby (2014): Tool demo: Using PVSio-web to demonstrate software issues in medical user interfaces. In: 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014).

[22] P. Masci, P. Oladimeji, P. Curzon & H. Thimbleby (2015): PVSio-web 2.0: Joining PVS to Human-Computer Interaction. In: 27th International Conference on Computer Aided Verification (CAV2015), Springer, doi:10.1007/978-3-319-21690-4_30. Tool and application examples available at http://www.pvsioweb.org.

[23] P.Masci, YiZhang, P.Jones, P.Oladimeji, E.D’Urso, C.Bernardeschi, P.Curzon & H.Thimbleby(2014): Combining PVSio with State flow. In: 6th NASA Formal Methods Symposium (NFM2014), doi:10.1007/978- 3-319-06200-6_16.

[24] C. Muñoz (2003): Rapid prototyping in PVS. Technical Report NIA 2003-03, NASA/CR-2003-212418, National Institute of Aerospace, Hampton, VA, USA.

[25] (2016): NDK. Available at http://developer.android.com/ndk.

[26] P.Oladimeji, P.Masci, P.Curzon & H.Thimbleby(2013):PVSio-web:atoolforrapidprototypingdeviceuser interfaces in PVS. In: FMIS2013, 5th International Workshop on Formal Methods for Interactive Systems, doi:10.14279/tuj.eceasst.69.963.

[27] S. Owre, J. M. Rushby & N. Shankar (1992): PVS: A Prototype Verification System. In: Automated Deduction—CADE-11: 11th International Conference on Automated Deduction, pp. 748–752, doi:10.1007/3- 540-55602-8_217.

[28] M. Pajic, Zhihao Jiang, Insup Lee, O. Sokolsky & R. Mangharam (2014): Safety-critical Medical Device Development Using the UPP2SF Model Translation Tool. ACM Trans. Embed. Comput. Syst. 13(4s), pp. 127:1–127:26, doi:10.1145/2584651.

[29] F. Paternò, C. Santoro & L. D. Spano (2009): MARIA: A Universal, Declarative, Multiple Abstraction-level Language for Service-oriented Applications in Ubiquitous Environments. ACM Trans. Comput.-Hum. Interact. 16(4), pp. 19:1–19:30, doi:10.1145/1614390.1614394.
https://www.researchgate.net/publication/220286389_MARIA_A_universal_declarative_multiple_abstraction-level_language_for_service-oriented_applications_in_ubiquitous_environments

[30] A Raymond Merrill Smullyan (1995): First-order logic. Dover publications, New York. Mandayam Srivas, Harald Rueß & David Cyrluk (1997): Hardware Verification Using PVS. In Thomas Kropf, editor: Formal Hardware Verification: Methods and Systems in Comparison, Lecture Notes in Computer Science 1287, Springer-Verlag, pp. 156–205, doi:10.1007/3-540-63475-4_4.
https://link.springer.com/chapter/10.1007/3-540-63475-4_4

Reference 4

REFERENCES
[1] Embedded Systems Safety & Security Survey, Barr Group, Germantown, MD, USA, Feb. 2018, available at http://www.barrgroup.com/.

[2] 2011 Embedded Engineer Survey, VDC Research, Natick, MA, USA, Aug. 2011.

[3] R. Bagnara, A. Bagnara, and P. M. Hill, “The MISRA C coding standard and its role in the development and analysis of safety- and security- critical embedded software,” in Static Analysis: Proceedings of the 25th International Symposium (SAS 2018), ser. Lecture Notes in Computer Science, A. Podelski, Ed., vol. 11002. Freiburg, Germany: Springer International Publishing, 2018, pp. 5–23.
[4] ——, “The MISRA C coding standard: A key enabler for the develop- ment of safety- and security-critical embedded software,” in embedded world Conference 2019 — Proceedings, DESIGN&ELEKTRONIK, Ed. Nuremberg, Germany: WEKA FACHMEDIEN, Richard-Reitzner-Allee 2, 85540 Haar, Germany, 2019, pp. 543–553.
[5] IEC, IEC 61508-1:2010: Functional Safety of Electri- cal/Electronic/Programmable Electronic Safety-Related Systems. Geneva, Switzerland: IEC, Apr. 2010.
[6] ISO, ISO 26262:2011: Road Vehicles — Functional Safety. Geneva, Switzerland: ISO, Nov. 2011.
[7] CENELEC, EN 50128:2011: Railway applications — Communication, signalling and processing systems - Software for railway control and protection systems. CENELEC, Jun. 2011.
[8] RTCA, SC-205, DO-178C: Software Considerations in Airborne Sys- tems and Equipment Certification. RTCA, Dec. 2011.
[9] General Principles of Software Validation; Final Guidance for In- dustry and FDA Staff, Version 2.0 ed., U.S. Department Of Health and Human Services; Food and Drug Administration; Center for De- vices and Radiological Health; Center for Biologics Evaluation and Research, Jan. 2002, available at http://www.fda.gov/MedicalDevices/ DeviceRegulationandGuidance/GuidanceDocuments/ucm085281.htm.
[10] P. Cousot, R. Cousot, J. Feret, A. Mine ́, L. Mauborgne, D. Monniaux, and X. Rival, “Varieties of static analyzers: A comparison with AS- TREE,” in First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007). Shanghai, China: IEEE Computer Society, Jun. 2007, pp. 3–20.
[11] C.JonesandO.Bonsignour,TheEconomicsofSoftwareQuality,1sted. Addison-Wesley Professional, 2011.
[12] R. M. dos Santos and M. A. Gerosa, “Impacts of coding practices on readability,” in Proceedings of the 26th Conference on Program Comprehension (ICPC 2018). Gothenburg, Sweden: Association for Computing Machinery, 2018, pp. 277–285.
[13] MISRA, MISRA-C:2012 — Guidelines for the use of the C language critical systems. Nuneaton, Warwickshire CV10 0TU, UK: HORIBA MIRA Limited, Feb. 2019, third edition, first revision.
[14] M. Barr, BARR-C:2018 — Embedded C Coding Standard. www. barrgroup.com: Barr Group, 2018.
[15] ISO/IEC, ISO/IEC 9899:1999/Cor 3:2007: Programming Languages — C, Technical Corrigendum 3 ed. Geneva, Switzerland: ISO/IEC, 2007.
[16] R. Bagnara, “That’s C, baby. C!” Report arXiv:1909.06353
[cs.PL], 2019, available at http://arxiv.org/.
[17] MISRA, MISRA C:2012 — Guidelines for the use of the C language in
critical systems. Nuneaton, Warwickshire CV10 0TU, UK: MIRA Ltd,
Mar. 2013.
[18] The Motor Industry Research Association, Development Guidelines For
Vehicle Based Software. Nuneaton, Warwickshire CV10 0TU, UK: The
Motor Industry Research Association, Nov. 1994.
[19] Motor Industry Software Reliability Association, MISRA-C:1998 —
Guidelines for the use of the C language in vehicle based sofware. Nuneaton, Warwickshire CV10 0TU, UK: MIRA Ltd, Jul. 1998.

reference 1-1

[1] T.F. Arnold, “The Concept of Coverage and Its Effect on the Reliability Model of Repairable Systems,” IEEE Trans. Computers, vol. 22, no. 6, pp. 251-254, June 1973.
[2] D. Avresky, J. Arlat, J.C. Laprie, and Y. Crouzet, “Fault Injection for Formal Testing of Fault Tolerance,” IEEE Trans. Reliability, vol. 45, no. 3, pp. 443-455, Sept. 1996.
[3] A. Avizienis, “Design of Fault-Tolerant Computers,” Proc. 1967 Fall Joint Computer Conf., AFIPS Conf. Proc., vol. 31, pp. 733-743, 1967.
[4] A. Avizienis and L. Chen, “On the Implementation of N-Version Programming for Software Fault Tolerance During Execution,” Proc. IEEE COMPSAC 77 Conf., pp. 149-155, Nov. 1977.
[5] A. Avizienis and Y. He, “Microprocessor Entomology: A Taxonomy of Design Faults in COTS Microprocessors,” Dependable Computing for Critical Applications 7, C.B. Weinstock and J. Rushby, eds., pp. 3-23, 1999.
[6] A. Avizienis and J.P.J. Kelly, “Fault Tolerance by Design Diversity: Concepts and Experiments,” Computer, vol. 17, no. 8, pp. 67-80, Aug. 1984.
[7] B.W. Boehm, “Guidelines for Verifying and Validating Software Requirements and Design Specifications,” Proc. European Conf. Applied Information Technology (IFIP ’79), pp. 711-719, Sept. 1979.
[8] W.G. Bouricius, W.C. Carter, and P.R. Schneider, “Reliability Modeling Techniques for Self-Repairing Computer Systems,” Proc. 24th Nat’l Conf. ACM, pp. 295-309, 1969.
[9] C. Cachin, J. Camenisch, M. Dacier, Y. Deswarte, J. Dobson, D. Horne, K. Kursawe, J.C. Laprie, J.C. Lebraud, D. Long, T. McCutcheon, J. Muller, F. Petzold, B. Pfitzmann, D. Powell, B. Randell, M. Schunter, V. Shoup, P. Verissimo, G. Trouessin, R.J. Stroud, M. Waidner, and I. Welch, “Malicious- and Accidental- Fault Tolerance in Internet Applications: Reference Model and Use Cases,” LAAS report no. 00280, MAFTIA, Project IST-1999-11583, p. 113, Aug. 2000.
[10] V. Castelli, R.E. Harper, P. Heidelberger, S.W. Hunter, K.S. Trivedi, K. Vaidyanathan, and W.P. Zeggert, “Proactive Manage- ment of Software Aging,” IBM J. Research and Development, vol. 45, no. 2, pp. 311-332, Mar. 2001.
[11] “Termes et De ́ finitions Concernant la Qualite ́ de Service, la Disponibilite ́ et la fiabilite ́,”Recommandation G 106, CCITT, 1984. [12] Information Technology Security Evaluation Criteria, Harmo- nized criteria of France, Germany, the Netherlands, the United
Kingdom, Commission of the European Communities, 1991.
[13] R. Chillarege, I.S. Bhandari, J.K. Chaar, J. Halliday, D.S. Moebus, B.K. Ray, and M.-Y. Wong, “Orthogonal Defect Classification-A Concept for In-Process Measurements,” IEEE Trans. Software Eng.,
vol. 18, no. 11, pp. 943-956, Nov. 1992.
[14] F. Cristian, “Understanding Fault-Tolerant Distributed Systems,” Comm. ACM, vol. 34, no. 2, pp. 56-78, 1991.
[15] H. Debar, M. Dacier, M. Nassehi, and A. Wespi, “Fixed vs. Variable- Length Patterns for Detecting Suspicious Process Behavior,” Proc. Fifth European Symp. Research in Computer Security, Sept. 1998.
[16] R.J. Ellison, D.A. Fischer, R.C. Linger, H.F. Lipson, T. Longstaff, and N.R. Mead, “Survivable Network Systems: An Emerging Discipline,” Technical Report CMU/SEI-97-TR-013, Carnegie Mellon Univ., May 1999.
[17] J.C. Fabre, V. Nicomette, T. Perennou, R.J. Stroud, and Z. Wu, “Implementing Fault Tolerant Applications Using Reflective Object-Oriented Programming,” Proc 25th IEEE Int’l Symp. Fault- Tolerant Computing (FTCS-25), pp. 489-498, 1995.
[18] S. Forrest, S.A. Hofmeyr, A. Somayaji, and T.A. Longstaff, “A Sense of Self for Unix Processes,” Proc. 1996 IEEE Symp. Security and Privacy, pp. 120-128, May 1996.
[19] A. Fox and D. Patterson, “Self-Repairing Computers,” Scientific Am., vol. 288, no. 6, pp. 54-61, 2003.
[20] J.M. Fray, Y. Deswarte, and D. Powell, “Intrusion Tolerance Using Fine-Grain Fragmentation-Scattering,” Proc. 1986 IEEE Symp. Security and Privacy, pp. 194-201, Apr. 1986.
[21] “Fundamental Concepts of Fault Tolerance,” Proc. 12th IEEE Int’l Symp. Fault-Tolerant Computing (FTCS-12), pp. 3-38, June 1982.
[22] A.G. Ganek and T.A. Korbi, “The Dawning of the Autonomic Computing Era,” IBM Systems J., vol. 42, no. 1, pp. 5-18, 2003.
[23] J.N. Gray, “Why do Computers Stop and What Can Be Done About It?” Proc. Fifth Symp. Reliability in Distributed Software and Database Systems, pp. 3-12, Jan. 1986.
[24] J. Gray, “Functionality, Availability, Agility, Manageability, Scalability—the New Priorities of Application Design,” Proc. Int’l Workshop High Performance Trans. Systems, Apr. 2001.
[25] R. Grigonis, “Fault-Resilience for Communications Convergence,” Special Supplement to CMP Media’s Converging Comm. Group, Spring 2001.
[26] J.E. Hosford, “Measures of Dependability,” Operations Research, vol. 8, no. 1, pp. 204-206, 1960.
[27] Y. Huang, C. Kintala, N. Kolettis, and N.D. Fulton, “Software Rejuvenation: Analysis, Module and Applications,” Proc. 25th IEEE Int’l Symp. Fault-Tolerant Computing, pp. 381-390, June 1995.
[28] Y. Huang and C. Kintala, “Software Fault Tolerance in the Application Layer,” Software Fault Tolerance, M. Lyu, ed., pp. 231- 248, 1995.
[29] Industrial-Process Measurement and Control—Evaluation of System Properties for the Purpose of System Assessment, Part 5: Assessment of System Dependability, Draft, Publication 1069-5, Int’l Electro- technical Commission (IEC) Secretariat, Feb. 1992.
[30] “Functional Safety of Electical/Electronic/Programmable Electro- nic Safety-Related Systems,” IEC Standard 61505, 1998.
[31] “Quality Concepts and Terminology,” part 1: Generic Terms and Definitions, Document ISO/TC 176/SC 1 N 93, Feb. 1992.
[32] “Common Criteria for Information Technology Security Evalua- tion,”ISO/IEC Standard 15408, Aug. 1999.
[33] J. Jacob, “The Basic Integrity Theorem,” Proc. Int’l Symp. Security and Privacy, pp. 89-97, 1991.
[34] J. Johnson, “Chaos: The Dollar Drain of IT Project Failures,” Application Development Trends, pp. 41-47, Jan. 1995.
[35] M.K. Joseph and A. Avizienis, “A Fault Tolerance Approach to Computer Viruses,” Proc. Symp. Security and Privacy, pp. 52-58, Apr. 1988.
[36] M.K. Joseph and A. Avizienis, “Software Fault Tolerance and Computer Security: A Shared Problem,” Proc. Ann. Joint Conf. Software Quality and Reliability, pp. 428-432, Mar. 1988.
[37] “DBench Dependability Benchmarks,” DBench, Project IST-2000- 25425, K. Kanoun et al., eds., pp. 233, May 2004.
[38] L. Lamport, R. Shostak, and M. Pease, “The Byzantine Generals Problem,” ACM Trans. Programming Languages and Systems, vol. 4, no. 3, pp. 382-401, July 1982.
[39] C.E. Landwher, A.R. Bull, J.P. McDermott, and W.S. Choi, “A Taxonomy of Computer Program Security Flaws,” ACM Comput- ing Survey, vol. 26, no. 3, pp. 211-254, 1994.
[40] J.C. Laprie, “Dependable Computing and Fault Tolerance: Con- cepts and Terminology,” Proc. 15th IEEE Int’l Symp. Fault-Tolerant Computing (FTCS-15), pp. 2-11, June 1985.
[41] Dependability: Basic Concepts and Terminology, J.C. Laprie, ed., Springer-Verlag, 1992.
[42] J.C. Laprie, “Dependability—Its Attributes, Impairments and Means,” Predictably Dependable Computing Systems, B. Randell et al., eds., pp. 3-24, 1995.
[43] N.A. Lynch, Distributed Algorithms. Morgan Kaufmann, 1996.
[44] J. McLean, “A Comment on the ‘Basic Security Theorem’ of Bell and LaPadula,” Information Processing Letters, vol. 20, no. 2, pp. 67- 70, 1985.
[45] J.F. Meyer, “On Evaluating the Performability of Degradable Computing Systems,” Proc. Eighth IEEE Int’l Symp. Fault-Tolerant Computing (FTCS-8), pp. 44-49, June 1978.
[46] J. Musa, “The Operational Profile in Software Reliability En- gineering: An Overview,” Proc. Third IEEE Int’l Symp. Software Reliability Eng. (ISSRE ’92), pp. 140-154, 1992.
[47] An Introduction to Computer Security: The NIST Handbook, Special Publication 800-12, Nat’l Inst. of Standards and Technology, 1995. [48] National Science and Technology Council, “Information Technol- ogy Frontiers for a New Millennium,”Supplement to the
Prsident’s FY 2000 Budget, 2000.
[49] R. Ortalo, Y. Deswarte, and M. Kaaniche, “Experimenting with
Quantitative Evaluation Tools for Monitoring Operational Secur- ity,” IEEE Trans. Software Eng., vol. 25, no. 5, pp. 633-650, Sept./ Oct. 1999.
[50] D. Parnas, “On the Criteria to be Used in Decomposing Systems into Modules,” Comm. ACM, vol. 15, no. 12, pp. 1053-1058, Dec. 1972.
[51] M.C. Paulk, B. Curtis, M.B. Chrissis, and C.V. Weber, “Capability Maturity Model for Software,” Technical Reports CMU/SEI-93- TR-24, ESC-TR-93-177, Software Eng. Inst., Carnegie Mellon Univ., Feb. 1993.
[52] C.P. Pfleeger, “Data Security,” Encyclopedia of Computer Science, A. Ralston et al., eds., Nature Publishing Group, pp. 504-507, 2000.
[53] D. Powell, G. Bonn, D. Seaton, P. Verissimo, and F. Waeselynck, “The Delta-4 Approach to Dependability in Open Distributed Computing Systems,” Proc. 18th IEEE Int’l Symp. Fault-Tolerant Computing (FTCS-18), pp. 246-251, June 1988.
[54] D. Powell, “Failure Mode Assumptions and Assumption Cover- age,” Proc. 22nd IEEE Int’l Symp. Fault-Tolerant Computing (FTCS-22), pp. 386-395, June 1992.
[55] “Conceptual Model and Architecture of MAFTIA,”MAFTIA, Project IST-1999-11583, D. Powell and R. Stroud, eds., p. 123, Jan. 2003.
[56] M.O. Rabin, “Efficient Dispersal of Information for Security, Load Balancing and Fault Tolerance,” J. ACM, vol. 36, no. 2, pp. 335-348, Apr. 1989.
[57] B. Randell, “System Structure for Software Fault Tolerance,” IEEE Trans. Software Eng., vol. 1, no. 2, pp. 220-232, June 1975.
[58] “Software Considerations in Airborne Systems and Equipment Certification,”DO-178-B/ED-12-B, Requirements and Technical Concepts for Aviation/European Organization for Civil Aviation Equipement, 1992.
[59] J. Rushby, “Formal Specification and Verification of a Fault- Masking and Transient-Recovery Model for Digital Flight Control Systems,” Proc. Second Int’l Symp. Formal Techniques in Real Time and Fault-Tolerant Systems, 1992.
[60] J. Rushby, “Formal Methods and Their Role in the Certification of Critical Systems,” Technical Report CSL-95-1, SRI Int’l, 1995.
[61] W.H. Sanders, M. Cukier, F. Webber, P. Pal, and R. Watro,
“Probabilistic Validation of Intrusion Tolerance,” Supplemental Volume Int’l Conf. Dependable Systems and Networks (DSN-2002), pp. 78-79, June 2002.
[62] Trust in Cyberspace. F. Schneider, ed., Nat’l Academy Press, 1999. [63] D.P. Siewiorek and R.S. Swarz, Reliable Computer Systems, Design
and Evaluation. Digital Press, 1992.
[64] R.M. Smith, K.S. Trivedi, and A.V. Ramesh, “Performability
Analysis: Measures, an Algorithm, and a Case Study,” IEEE
Trans. Computers, vol. 37, no. 4, pp. 406-417, Apr. 1988.
[65] “Dependability Assessment Criteria,” SQUALE project (ACTS95/
AC097), LAAS Report no. 98456, Jan. 1999.
[66] P. Thevenod-Fosse, H. Waeselynck, and Y. Crouzet, “An
Experimental Study on Softawre Structural Testing: Determinis- tic Testing Versus Random Input Generation,” Proc. 21st IEEE Int’l Symp. Fault-Tolerant Computing, pp. 410-417, June 1981.
[67] USA Department of Transportation, Office of Inspector General, “Audit Report: Advance Automation System,”Report AV-1998- 113, Apr. 1998.
[68] A. Valdes, M. Almgren, S. Cheung, Y. Deswarte, B. Dutertre, J. Levy, H. Sa ̈ıdi, V. Stavridou, and T. Uribe, “An Adaptative Intrusion-Tolerant Server Architecture,” Proc. 10th Int’l Workshop Security Protocols, Apr. 2002.
[69] E.J. Weyuker, “On Testing Nontestable Programs,” The Computer J., vol. 25, no. 4, pp. 465-470, 1982.
[70] A. Wood, “NonStop Availability in a Client/Server Environ- ment,” Tandem Technical Report 94.1, Mar. 1994.

reference 1-10

Miller, C., Valasek, C.: ‘Remote exploitation of an unaltered passenger vehicle’, August 2015.
2)
Kazman, R., Klein, M., Barbacci, M., et al: ‘The architecture tradeoff analysis method’. Technical Report, CMU/SEI-98-TR-008, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, 1998.
3)
RTCA DO-332: ‘Object-Oriented Technology and Related Techniques Supplement to DO-178C and DO-278A’, December 2011.
4)
ISO/IEC: ‘Programming languages – C (ISO/IEC 9899:2011)’ (ISO, Geneva, Switzerland, 2011, 3rd edn.).
5)
Seacord, R.: ‘C secure coding rules: past, present, and future’. Available at http://www.informit.com/articles/article.aspx?p=2088511, accessed 18 April 2016.
6)
MISRA (Motor Industry Software Reliability Association): ‘MISRA C: 2004 Guidelines for the use of the C language in critical systems’ (MIRA, Nuneaton, UK, 2004), ISBN 095241564X.
7)
ISO/IEC: ‘Programming languages – C (ISO/IEC 9899:1999)’ (ISO, Geneva, Switzerland, 1999, 2nd edn.).
8)
ISO/DIS 26262 – Road vehicles – Functional safety. The standard consists of several parts, published in 2011.
9)
DO-178C/ED-12C: ‘Software Considerations in Airborne Systems and Equipment Certification’, RTCA, 2011.
10)
Hack the S. Available at http://www.su-tesla.space/2016/04/hack-s.html, accessed 19 April 2016.
11)
MISRA C:2012 Addendum 2 Coverage of MISRA C:2012 against ISO/IEC TS 17961:2013 ‘C Secure’. Nuneaton, UK: HORIBA MIRA, 2016 (ISBN 978-1-906400-15-6).
12)
ISO/IEC: ‘Programming languages – C (ISO/IEC 9899:1990)’ (ISO, Geneva, Switzerland, 1990).
13)
MISRA C – WG14 Liaison Report WG14 Meeting, London 11th–14th April 2016 Andrew Banks. Available at http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2035.pdf, accessed 22 April 2016.
14)
FIPS PUB 199: ‘Standards for Security Categorization of Federal Information and Information Systems’, 2004.
15)
Road Vehicles – Vehicle Cybersecurity Engineering. Available at standardsproposals.bsigroup.com/Home/Proposal/5410, accessed 21 April 2016.
16)
Checkoway, S., McCoy, D., Kantor, B., et al: ‘Comprehensive experimental analyses of automotive attack surfaces’. D. Wagner (Chair), SEC'11, Proc. of the 20th USENIX Conf. on Security, San Francisco, CA, 8–12 August 2011. Available at http://www.usenix.org/events/sec11/tech/full_papers/Checkoway.pdf.
17)
SAE J3061 Cybersecurity Guidebook for Cyber-Physical Vehicle Systems. Available at http://standards.sae.org/wip/j3061/.
18)
ISO/IEC TS 17961: ‘Information technology – programming languages, their environments and system software interfaces – C secure coding rules’ (ISO, Geneva, Switzerland, 2012).
19)
Seacord, R.: ‘The CERT C coding standard, second edition: 98 rules for developing safe, reliable, and secure systems’ (Addison-Wesley, 2014).
20)
Lockheed Martin: ‘Joint Strike Fighter Air Vehicle C++ Coding Standards for the system development and demonstration program’, Document Number 2RDU00001 Rev C., December 2005. Available at http://www.stroustrup.com/JSF-AV-rules.pdf, accessed 22 April 2016.
21)
Seacord, R.: ‘The CERT C secure coding standard’ (Addison-Wesley, 2008).
22)
IEC 61508:2010: ‘Functional safety of electrical/electronic/programmable electronic safety-related systems’, International Electrotechnical Commission, in 7 parts published in 2010.
23)
MISRA (Motor Industry Software Reliability Association): ‘Guidelines for the use of the C language in vehicle based software’ (MIRA, Nuneaton, UK, 1998), ISBN 978-0-9524156-6-4.
24)
MISRA C:2012 Amendment 1. Additional security guidelines for MISRA C:2012. Nuneaton, UK: HORIBA MIRA, 2016 (ISBN 978-1-906400-16-3).
25)
MISRA (Motor Industry Software Reliability Association): ‘MISRA C3: Guidelines for the use of the C language in critical systems 2012’ (MIRA, Nuneaton, UK, 2012), ISBN 978-1-906400-10-1.
26)
Gerard, J.: ‘NASA/JPL laboratory for reliable software. 2006. The power of 10: rules for developing safety-critical code’, Computer, 2006, 39, (6), pp. 95–97, doi: http://www.dx.doi.org/10.1109/MC.2006.212.
27)
McCarthy, C., Harnett, K., Carter, A.: ‘Characterisation of potential security threats in modern automobiles: a composite modelling approach’. Report no. DOT HS 812 074, National Highway Traffic Safety Administration, Washington, DC, October, 2014.

reference 2-4

[Barr]
Barr, Michael. “Programming Embedded Systems in C and C++." O’Reilly, 1999.
[C90]
“ISO/IEC9899:1990, Programming Languages – C,” ISO, 1990.
[C99]
“ISO/IEC9899:1999, Programming Languages – C,” ISO, 1999.
[CERT-T]
Seacord, Robert C. "The CERT C Coding Standard, Second Edition." Pearson, 2014
[Harbison]
Harbison III, Samuel P. and Guy L. Steele, Jr. "C: A Reference Manual, Fifth Edition." Prentice Hall, 2002.
[Hatton]
Hatton, Les. “Safer C: Developing Software for High-Integrity and Safety-Critical Systems.” McGraw-Hill, 1994.
[Holub]
Holub, Allen I. “Enough Rope to Shoot Yourself in the Foot: Rules for C and C++ Programming.” McGraw-Hill, 1995.
[IEC61508]
“Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems,” International Electromechanical Commission, 1998-2000.
[Koenig]
Koenig, Andrew. “C Traps and Pitfalls.” Addison-Wesley, 1988.
[Loudon]
Loudon, Kyle. "C++ Pocket Reference." O'Reilly, 2003
[MISRA-C]
“MISRA-C:2012 Guidelines for the use of C language in critical systems,” MIRA, March 2013.
[MISRA-C++]
“MISRA-C++ Guidelines for the use of C++ language in critical systems,” MIRA, June 2008.
[Prinz]
Prinz, Peter and Ulla Kirch-Prinz. “C Pocket Reference.” O’Reilly, 2003.
[Sutter]
Sutter, Herb and Andrei Alexandrescu. “C++ Coding Standards: 101 Rules, Guidelines, and Best Practices.” Pearson, 2005.
[Uwano]
Uwano, H., Nakamura, M., Monden, A., and Matsumoto, K. “Analyzing Individual Performance of Source Code Review Using Reviewer’s Eye Movement,” Proceedings of the 2006 Symposium on Eye Tracking Research & Applications, San Diego, March 27-29, 2006.

reference 2-5 frama c

[1] Jean-Raymond Abrial. The B-Book: Assigning Programs to Meanings. Cambridge Uni- versity Press, 1996.
[2] Ali Ayad and Claude Marché. Behavioral properties of floating-point programs. Hisseo publications, 2009. http://hisseo.saclay.inria.fr/ayad09.pdf.
[3] Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Pro- grams. In 18th IEEE International Symposium on Computer Arithmetic, pages 187–194, Montpellier, France, June 2007.
[4] Patrice Chalin. Reassessing JML’s logical foundation. In Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP’05), Glasgow, Scotland, July 2005.
[5] Patrice Chalin. A sound assertion semantics for the dependable systems evolution veri- fying compiler. In Proceedings of the International Conference on Software Engineering (ICSE’07), pages 23–33, Los Alamitos, CA, USA, 2007. IEEE Computer Society.
[6] David R. Cok. OpenJML: JML for Java 7 by Extending OpenJDK. In Mihaela Bobaru, Klaus Havelund, Gerard Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, volume 6617 of Lecture Notes in Computer Science, pages 472–479. Springer Berlin / Heidelberg, 2011. 10.1007/978-3-642-20398-5_35.
[7] David R. Cok. OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In F-IDE, pages 79–92, 2014.
[8] David R. Cok and Joseph R. Kiniry. ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system. In Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), volume 3362 of Lecture Notes in Computer Science, pages 108–128. Springer, 2005.
[9] Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, and Westley Weimer. Ccured in the real world. In PLDI ’03: Proceedings of the ACM SIGPLAN 2003 con- ference on Programming language design and implementation, pages 232–244, 2003.
[10] Jeremy Paul Condit, Matthew Thomas Harren, Zachary Ryan Anderson, David Gay, and George Necula. Dependent types for low-level programming. In ESOP ’07: Proceedings of the 16th European Symposium on Programming, October 2006.
[11] Jean-Christophe Filliâtre and Claude Marché. Multi-prover verification of C programs. In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, 6th International Conference
107
BIBLIOGRAPHY
on Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science, pages 15–29, Seattle, WA, USA, November 2004. Springer.
[12] Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Werner Damm and Holger Hermanns, editors, 19th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Berlin, Germany, July 2007. Springer.
[13] A. Giorgetti and J. Groslambert. JAG: JML Annotation Generation for verifying tempo- ral properties. In FASE’2006, Fundamental Approaches to Software Engineering, volume 3922 of LNCS, pages 373–376, Vienna, Austria, March 2006. Springer.
[14] International Organization for Standardization (ISO). The ANSI C standard (C99). http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf.
[15] Brian Kernighan and Dennis Ritchie. The C Programming Language (2nd Ed.). Prentice- Hall, 1988.
[16] Gary Leavens. Jml. http://www.eecs.ucf.edu/~leavens/JML/.
[17] Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06i, Iowa State University, 2000.
[18] Gary T. Leavens, K. Rustan M. Leino, and Peter Müller. Specification and verification challenges for sequential object-oriented programs. Form. Asp. Comput., 19(2):159–189, 2007.
[19] Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA 2000 Companion, Minneapolis, Minnesota, pages 105–106, 2000.
[20] Claude Marché. Towards modular algebraic specifications for pointer programs: a case study. In H. Comon-Lundh, C. Kirchner, and H. Kirchner, editors, Rewriting, Compu- tation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 235–258. Springer-Verlag, 2007.
[21] Yannick Moy. Union and cast in deductive verification. Technical Report ICIS-R07015, Radboud University Nijmegen, July 2007. http://www.lri.fr/~moy/union_and_cast/ union_and_cast.pdf.
[22] George C. Necula, Scott McPeak, and Westley Weimer. CCured: Type-safe retrofitting of legacy code. In Symposium on Principles of Programming Languages, pages 128–139, 2002.
[23] Arun D. Raghavan and Gary T. Leavens. Desugaring JML method specifications. Tech- nical Report 00-03a, Iowa State University, 2000.
[24] David Stevenson et al. An american national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices, 22(2):9–25, 1987.
[25] Wikipedia. First order logic. http://en.wikipedia.org/wiki/First_order_logic.
[26] Wikipedia. IEEE 754. http://en.wikipedia.org/wiki/IEEE_754-1985.

2-7 reference

on Varieties of static analyzers: A comparison with ASTREE.
[1] T. Ball and S. Rajamani. The SLAM project: debugging
system software via static analysis. In 29th ACM Symp. on
Principles of Prog. Lang., POPL ’02, pp. 1–3, 2002.
[2] D. Beyer, T. Henzinger, R. Jhala, and R. Majumdar. Checking
memory safety with BLAST. In 8th Int. Conf. on Fundamental
Approaches to Soft. Eng., FASE ’05, LNCS 3442, pp.
2–18. Springer, 2005.
[3] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne,
A. Min´e, D. Monniaux, and X. Rival. Design and Implementation
of a Special-Purpose Static Program Analyzer
for Safety-Critical Real-Time Embedded Software. In The
Essence of Computation: Complexity, Analysis, Transformation.
Essays Dedicated to Neil D. Jones, LNCS 2566, pp.
85–108. Springer, 2002.
[4] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne,
A. Min´e, D. Monniaux, and X. Rival. A Static Analyzer
for Large Safety-Critical Software. In ACM Conf. on Prog.
Lang. Design and Impl., PLDI ’03, pp. 196–207, 2003.
[5] S. Boldo and J.-C. Filliˆatre. Formal Verification of Floating-
Point Programs. In 18th IEEE Int. Symp. on Computer Arithmetic,
ARITH ’18, 2007.
[6] B. Brew and M. Johnson. Value Lattice Static Analysis, A
New Approach to Static Analysis. Dr. Dobbs J., 2001.
[7] W. Bush, J. Pincus, and D. Sielaff. A Static Analyzer for
Finding Dynamic Programming Errors. Soft. Pract. and
Exp., 30(7):775–802, 2000.
[8] S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular
Verification of Software Components in C. IEEE Trans. on
Soft. Eng., 30(6):388–402, 2004.
[9] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith.
Counterexample-guided abstraction refinement for symbolic
model checking. J. Acm, 50(5):752–794, 2003.
[10] E. Clarke and D. Kroening. ANSI-C Bounded Model
Checker User Manual. Technical report, School of Computer
Science, Carnegie Mellon University, 2006.
[11] E. Clarke, D. Kroening, and F. Lerda. A tool for checking
ANSI-C programs. In Tools and Algorithms for the Construction
and Analysis of Systems, TACAS ’04, LNCS 2988,
pp. 168–176. Springer, 2004.
[12] T. Copeland. PMD Applied. Centennial Books, 2005.
[13] P. Cousot and R. Cousot. Static determination of dynamic
properties of programs. In 2nd Int. Symp. on Programming,
pp. 106–130, Paris, France, 1976. Dunod.
[14] P. Cousot and R. Cousot. Abstract interpretation: a unified
lattice model for static analysis of programs by construction
or approximation of fixpoints. In Conf. Rec. 4th ACM Symp.
on Principles of Prog. Lang., POPL ’77, pp. 238–252, 1977.
[15] P. Cousot and R. Cousot. Systematic design of program analysis
frameworks. In Conf. Rec. 6th ACM Symp. on Principles
of Prog. Lang., POPL ’79, pp. 269–282, 1979.
[16] P. Cousot and R. Cousot. Comparing the Galois Connection
and Widening/Narrowing Approaches to Abstract Interpretation.
In 4th Int. Symp. Prog. Lang. Implementation and
Logic Programming, PLILP ’92, LNCS 631, pp. 269–295.
Springer, 1992.
[17] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min´e,
D. Monniaux, and X. Rival. The ASTR´EE analyser. In 14th
European Symp. on Prog. Lang. and Systems, ESOP ’05,
LNCS 3444, pp. 21–30. Springer, 2005.
[18] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min´e,
D. Monniaux, and X. Rival. Combination of Abstractions
in the ASTR´E E Static Analyzer. In 11th Asian Comp. Sci.
Conf., ASIAN 06, LNCS. Springer, 2006.
[19] P. Cousot and N. Halbwachs. Automatic discovery of linear
restraints among variables of a program. In Conf. Rec. 5th
ACM Symp. on Principles of Prog. Lang., POPL ’78, pp. 84–
97, 1978.
[20] A. Deutsch. Static Verification Of Dynamic Properties.
PolySpace Technologies, www.polyspace.com.
[21] D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf.
Bugs as Deviant Behavior: A General Approach to Inferring
Errors in Systems Code. In 18th ACM Symp. on Operating
Systems Principles, 2001.
[22] M. Fagan. Design and code inspections to reduce errors
in program development. IBM Systems J., 15(3):258–287,
1976.
[23] J. Feret. Static Analysis of Digital Filters. In 13th European
Symp. on Prog. Lang. and Systems, ESOP ’2004, Barcelona,
Spain, LNCS 2986, pp. 33–48. Springer, 2004.
[24] J. Feret. The Arithmetic-Geometric Progression Abstract
Domain. In 6th International Conference on Verification,
Model Checking and Abstract Interpretation, VMCAI ’2005,
Paris, France, LNCS 3385, pp. 42–58. Springer, 2005.
[25] J.-C. Filliˆatre and C. March´e. Multi-Prover Verification of C
Programs. In 6th Int. Conf. on Formal Engineering Methods,
ICFEM ’04, LNCS 3308, pp. 15–29. Springer, 2004.
[26] C. Flanagan, K. M. Leino, M. Lillibridge, G. Nelson, J. Saxe,
and R. Stata. Extended static checking for Java. In ACM
Conf. on Prog. Lang. Design and Impl., PLDI ’02, pp. 234–
245, 2002.
[27] J. Foster, M. F¨ahndrich, and A. Aiken. Polymorphic versus
Monomorphic Flow-insensitive Points-to Analysis for C. In
7th Int. Sym. on Static Analysis, SAS ’00, LNCS 1824, pp.
175–198. Springer, 2000.
[28] P. Godefroid. Software Model Checking: The VeriSoft Approach.
Formal Methods in System Design, 26(2):77–101,
2005.
[29] S. Graf and H. Sa¨ıdi. Verifying Invariants Using Theorem
Proving. In 8th Int. Conf. on Computer Aided Verification,
CAV ’97, LNCS 1102, pp. 196–207. Springer, 1996.
[30] P. Granger. Static Analysis of Arithmetical Congruences. Int.
J. Comput. Math., 30:165–190, 1989.
[31] D. Grossman, M. Hicks, T. Jim, and G. Morrisett. Cyclone:
a Type-safe Dialect of C. C/C++ Users J., 23(1), 2005.
[32] S. Gupta and G. Sreenivasamurthy. Navigating “C”
in a “leaky” boat? Try Purify. www-128.ibm.com/
developerworks/rational/library/06/0822_
satish-Giridhar/, 2006.
[33] L. Hatton. Safer C: Developing for High-Integrity and
Safety-Critical Systems. McGraw-Hill, 1995.
[34] T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy
abstraction. In Proc. 29th ACM Symp. on Principles of Prog.
Lang., POPL ’02, pp. 58–70. ACM Press, 2002.
[35] G. Holzmann. UNO: Static Source Code Checking for User-
Defined Properties. In 6th World Conf. on Integrated Design
and Process Technology, IDPT ’02, 2002.
[36] G. Holzmann. The SPIN MODEL CHECKER, Primer and
Reference Manual. Addison-Wesley, Sept. 2003.
[37] D. Hovemeyer, J. Spacco, and W. Pugh. Evaluating and tuning
a static analysis to find null pointer bugs. In ACM Workshop
on Program Analysis For Software Tools and Engineering,
PASTE ’05, pp. 13–19, 2005.
[38] Esterel Technologies. SCADE SuiteTM, The Standard for the
Development of Safety-Critical Embedded Software in the
Avionics Industry. www.esterel-technologies.com/
products/scade-suite/.
[39] Gimpel Software
R . PC-lintTM/ FlexeLintTM Value Tracking.
www.gimpel.com.
[40] GrammaTech
R . CodeSonar: A code-analysis tool that identifies
complex bugs at compile time. www.grammatech.
com/products/codesurfer/.
[41] Klocwork
R . Klocwork K7TM. www.klocwork.com.
[42] The MathWorks. Simulink
R — Simulation and Model-
Based Design. www.mathworks.com/products/
simulink/.
[43] Reasoning, Inc. Reasoning inspection service defect
data, Tomcat, version 4.1.24. www.reasoning.com/pdf/
Tomcat_Defect_Report.pdf, 2003.
[44] R. Iosif, M. Dwyer, and J. Hatcliff. Translating Java for
Multiple Model Checkers: The Bandera Back-End. Formal
Methods in System Design, 26(2):137–180, 2005.
[45] ISO/IEC. International standard – Programming languages
– C, 1999. Standard 9899:1999.
[46] D. Jackson. Software Abstractions: Logic, Language, and
Analysis. MIT Press. Cambridge, MA., 2006.
[47] B. Jeannet and A. Min´e. The Apron Numerical Abstract
Domain Library. apron.cri.ensmp.fr/library/.
[48] J. Kodumal and A. Aiken. Banshee: A Scalable Constraint-
Based Analysis Toolkit. In 7th Int. Sym. on Static Analysis,
SAS ’07, LNCS 3672, pp. 218–234. Springer, 2005.
[49] N. Kumar and R. Peri. Transparent Debugging of Dynamically
Instrumented Programs. ACM SIGARCH Computer
Architecture News, 33(5):57–62, 2005.
[50] D. Larochelle and D. Evans. Statically Detecting Likely
Buffer Overflow Vulnerabilities. In 2001 USENIX Security
Symposium, Washington, D.C., 2001.
[51] K. Leino and G. Nelson. An Extended Static Checker for
Modula-3. In 7th Int. Conf. on Compiler Construction,
CC ’98, LNCS 1383, pp. 302–305. Springer, 1998.
[52] X. Leroy. Coinductive Big-Step Operational Semantics.
In 15th European Symp. on Prog. Lang. and Systems,
ESOP ’2006, LNCS 3924, pp. 54–68. Springer, 2006.
[53] X. Leroy. Formal certification of a compiler back-end or:
programming a compiler with a proof assistant. In Conf. Rec.
33rd ACM Symp. on Principles of Prog. Lang., POPL’06, pp.
42–54, 2006.
[54] T. Lev-Ami, R. Manevich, and M. Sagiv. TVLA: A System
for Generating Abstract Interpreters. In P. Jacquart, editor,
Building the Information Society, chapter 4, pp. 367–376.
Kluwer Academic
Publishers, Dordrecht, The Netherlands,
2004.
[55] M. Martel. An Overview of Semantics for the Validation of
Numerical Programs. In 6th Int. Conf. on Verification, Model
Checking, and Abstract Interpretation, VMCAI ’05, LNCS
3385, pp. 59–77, 2005.
[56] L. Mauborgne. ASTR´E E: verification of absence of run-time
error. In P. Jacquart, editor, Building the Information Society,
chapter 4, pp. 385–392. Kluwer Acad. Pub. Dordrecht, The
Netherlands, 2004.
[57] L. Mauborgne and X. Rival. Trace Partitioning in Abstract
Interpretation Based Static Analyzer. In 14th European
Symp. on Prog. Lang. and Systems, ESOP ’05, LNCS 3444,
pp. 5–20. Springer, 2005.
[58] R. Milner. A theory of type polymorphism in programming.
J. of Comp. and Sys. Sciences, 17:348–375, 1978.
[59] A. Min´e. A Few Graph-Based Relational Numerical Abstract
Domains. In 9th Int. Symp. on Static Analysis, SAS ’02,
LNCS 2477, pp. 117–132. Springer, 2002.
[60] A. Min´e. Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors. In 13th European Symp. on Prog. Lang. and Systems, ESOP ’04, LNCS 2986, pp. 3–17. Springer, 2004.
[61] A. Min´e. The Octagon Abstract Domain. Higher-Order and Symbolic Computation, 19:31–100, 2006.
[62] A. Min´e. Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics. In ACM Conf. on Languages, Compilers, and Tools for Embedded Systems, LCTES ’2006, pp. 54–63, 2006.
[63] A. Min´e. Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. In 7th Int. Conf. on Verification, Model Checking and Abstract Interpretation VMCAI ’06, LNCS 3855, pp. 348–363. Springer, 2006.
[64] MISRA (The Motor Industry Software Reliability Association).
Guidelines for the use of the C language in vehicle based systems Software. www.misra.org.uk, 1998.
[65] D. Monniaux. The Parallel Implementation of the ASTR´E E Static Analyzer. In 3rd Asian Symp. on Prog. Lang. and Systems, APLAS ’05, LNCS 3780, pp. 86–96. Springer, 2005.
[66] D. Monniaux. Compositional Analysis of Floating-Point Linear Numerical Filters. In 17th Int. Conf. on Computer Aided Verification, CAV ’05, LNCS 3576, pp. 199–212. Springer, 2005.
[67] N. Nagappan and T. Ball. Static analysis tools as early indicators of pre-release defect density. In Proc. 27th ACM SIGSOFT Int. Conf. on Software engineering, pp. 580–586. ACM Press, 2005.
[68] G. Necula, J. Condit, M. Harren, S. McPeak, andW.Weimer. CCured: Type-Safe Retrofitting of Legacy Software. ACM Trans. Program. Lang. Syst., 27(3):477–526, 2005.
[69] N. Nethercote and J. Seward. Valgrind: A Framework for Heavyweight Dynamic Binary Instrumentation. In ACM Conf. on Prog. Lang. Design and Impl., PLDI ’07, 2007.
[70] A. Pnueli, O. Shtrichman, and M. Siegel. The Code Validation Tool CVT: Automatic Verification of a Compilation Process. Int. J. on Soft. Tools for Tech. Trans., 2(2):192–201, 1998.
[71] W. Pugh and D. Wonnacott. Static Analysis of Upper and Lower Bounds on Dependences and Parallelism. ACM Trans. Program. Lang. Syst., 16(4):1248–1278, 1994.
[72] F. Randimbivololona, J. Souyris, P. Baudin, A. Pacalet, J. Raguideau, and D. Schoen. Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. In
World Congress on Formal Methods in the Development of Computing Systems, LNCS 1709, pp. 1798–1815. Springer, 1999.
[73] X. Rival. Abstract Interpretation Based Certification of Assembly Code. In 4th Int. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAIS ’03, LNCS 2575, pp. 41–55. Springer, 2003.
[74] X. Rival. Symbolic Transfer Functions-based Approaches to Certified Compilation. In Conf. Rec. 31st ACM Symp. on Principles of Prog. Lang., POPL ’01, pp. 1–13, 2004.
[75] Robby, M. Dwyer, and J. Hatcliff. Domain-specific Model Checking Using The Bogor Framework. In 21st IEEE/ACM Int. Conf. on Automated Software Engineering, ASE ’06, Tokyo, Japan, 2006.
[76] A. Venet and G. Brat. Precise and Efficient Static Array Bound Checking for Large Embedded C Programs. In Int. Conf. on Prog. Lang. Design and Impl., PLDI ’04, pp. 231–242. ACM Press, 2004.
[77] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model Checking Programs. Automated Soft. Eng. J., 10(2), 2003.
[78] K. Yi, H. Choi, J. Kim, and Y. Kim. An Empirical Study on Classification Methods for Alarms from a Bug-Finding Static C Analyzer. Inf. Proc. Let., 102(2-3):118–123, 2007.
[79] J. Zheng, L.Williams, N. Nagappan,W. Snipes, J. Hudepohl, and M. Vouk. On the value of static analysis for fault detection in software. IEEE Trans. on Soft. Eng., 32(4):240–253, 2006.
[80] F. Zhou, J. Condit, Z. Anderson, I. Bagrak, R. Ennals, M. Harren, G. Necula, and E. Brewer. SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques.
In Operating System Design and Implementation, OSDI ’06. USENIX Assoc., 2006.

reference 2-8

Verification of C Programs Using Automated Reasoning

[1] P. Cousot and R. Cousot, Abstract interpretation: a
unified lattice model for static analysis of programs by
construction or approximation of fixpoints (ACM POPL
1977).
[2] J-R. Abrial, The B-Book: Assigning Programs to Meanings
(Cambridge University Press, 1996).
[3] American National Standard for Information Systems -
Programming Language C, ANSI X3.159-1989 (American
National Standards Institute, 1989).
[4] ISO/IEC 9899-1999, Programming Languages - C (International
Standards Organization, 1999).
[5] Mike Barnett, K. Rustan M. Leino, and Wolfram
Schulte, The Spec# programming system: An overview
(CASSIS 2004, LNCS vol. 3362, Springer, 2004).
[6] K. Rustan M. Leino, Greg Nelson, and James B. Saxe,
ESC/Java User’s Manual (Technical Note 2000-002,
Compaq Systems Research Center, October 2000).
[7] Jamie Stark and Andrew Ireland, Invariant Discovery
via Failed Proof Attempts (Lecture Notes in Computer
Science 1559, 271-288, 1999).
[8] K. Rustan M. Leino, Francesco Logozzo, Loop Invariants
on Demand (APLAS 2005, 119-134).
[9] J. V. Guttag and J. J. Horning, Introduction to
LCL, A Larch/C Interface Language (available at
http://ftp.digital.com/pub/Compaq/SRC/researchreports/
abstracts/src-rr-074.html).
[10] MISRA-C:2004 - Guidelines for the use of the C language
in critical systems (Motor Industry Software Reliability
Association 2004, ISBN 0 9524156 2 3).
[11] D. Crocker and J. Carlton, A High Productivity
Tool for Formally Verifed Software Development
(Escher Technologies, 2004. Available at
http://www.eschertech.com/papers/pdpaper.pdf).
[12] J. Barnes, High Integrity Software: The SPARK Approach
to Safety and Security (Addison Wesley 2003,
ISBN 0-321-13616-0).
[13] David Evans and David Larochelle, Improving Security
Using Extensible Lightweight Static Analysis (IEEE Software, Jan/Feb 2002).
[14] David Crocker, Safe Object-Oriented Software: the Verified Design-by-Contract paradigm (Proceedings of the Twelfth Safety-Critical Systems Symposium (ed. F.Redmill & T.Anderson) 19-41, Springer-Verlag, London, 2004. ISBN 1-85233-800-8).
[15] J.-C. Fillitre, Why: a multi-language multi-prover verification tool (Research Report 1366, LRI, Universit Paris Sud, 2003).
[16] Jean-Christophe Fillitre and Claude March, Multi-Prover Verification of C Programs (Lecture Notes in Computer Science 3308, 15-29, 2004).

reference 2-9

Verification of C Programs Using Automated Reasoning
[1] E. Cohen, M. Moskal, W. Schulte, and S. Tobies. A practical verification methodology for concurrent programs. 2008. To appear.
[2] E. Cohen, M. Moskal, W. Schulte, and S. Tobies. A precise yet efficient memory model for C. 2008. To appear.
[3] L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary, 2008.
[4] R.DeLineand K.R.M.Leino.Boogie PL:A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, Mar. 2005.
[5] S. Maus, M. Moskal, and W. Schulte. Vx86: x86 assembler simulated in C powered by automated theorem proving. In 12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008), LNCS 5140, 2008.
[6] The Verisoft XT project. http://www.verisoftxt.de/, 2007.

reference 2-12

Intel® 64 and IA-32 Architectures
Software Developer’s Manual
1.4 RELATED LITERATURE
Literature related to Intel 64 and IA-32 processors is listed and viewable on-line at:
https://software.intel.com/en-us/articles/intel-sdm
See also:
• The latest security information on Intel® products:
https://www.intel.com/content/www/us/en/security-center/default.html
• Software developer resources, guidance and insights for security advisories:
https://software.intel.com/security-software-guidance/
• The data sheet for a particular Intel 64 or IA-32 processor
• The specification update for a particular Intel 64 or IA-32 processor
• Intel® C++ Compiler documentation and online help:
http://software.intel.com/en-us/articles/intel-compilers/
• Intel® Fortran Compiler documentation and online help:
http://software.intel.com/en-us/articles/intel-compilers/
• Intel® Software Development Tools:
https://software.intel.com/en-us/intel-sdp-home
• Intel® 64 and IA-32 Architectures Software Developer’s Manual (in one, four or ten volumes):
https://software.intel.com/en-us/articles/intel-sdm
• Intel® 64 and IA-32 Architectures Optimization Reference Manual:
https://software.intel.com/en-us/articles/intel-sdm#optimization
• Intel 64 Architecture x2APIC Specification:
http://www.intel.com/content/www/us/en/architecture-and-technology/64-architecture-x2apic-specification.
html
• Intel® Trusted Execution Technology Measured Launched Environment Programming Guide:
http://www.intel.com/content/www/us/en/software-developers/intel-txt-software-development-guide.html
• Developing Multi-threaded Applications: A Platform Consistent Approach:
https://software.intel.com/sites/default/files/article/147714/51534-developing-multithreaded-applications.
pdf
• Using Spin-Loops on Intel® Pentium® 4 Processor and Intel® Xeon® Processor:
https://software.intel.com/sites/default/files/22/30/25602
• Performance Monitoring Unit Sharing Guide
http://software.intel.com/file/30388
Literature related to selected features in future Intel processors are available at:
• Intel® Architecture Instruction Set Extensions Programming Reference
https://software.intel.com/en-us/isa-extensions
• Intel® Software Guard Extensions (Intel® SGX) Programming Reference
https://software.intel.com/en-us/isa-extensions/intel-sgx
More relevant links are:
• Intel® Developer Zone:
https://software.intel.com/en-us
• Developer centers:
http://www.intel.com/content/www/us/en/hardware-developers/developer-centers.html
• Processor support general link:
http://www.intel.com/support/processors/
• Intel® Hyper-Threading Technology (Intel® HT Technology):
http://www.intel.com/technology/platform-technology/hyper-threading/index.htm

reference 2-21

on VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java

1. Bart Jacobs, Jan Smans, and Frank Piessens. A quick tour of the VeriFast program verifier. In APLAS, 2010.
2. Bart Jacobs, Jan Smans, and Frank Piessens. The VeriFast program verifier: A tutorial. At http://www.cs.kuleuven.be/ ̃bartj/verifast/, 2010.
3. Richard Bornat, Cristiano Calcagno, Peter O’Hearn, and Matthew Parkinson. Per- mission accounting in separation logic. In POPL, 2005.
4. Bart Jacobs and Frank Piessens. Expressive modular fine-grained concurrency spec- ification. In POPL, 2011.
5. Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. A local shape analysis based on separation logic. In TACAS, 2006.
6. Cristiano Calcagno, Dino Distefano, Peter O’Hearn, and Hongseok Yang. Compo- sitional shape analysis by means of bi-abduction. In POPL, 2009.

2-32

The Variability of Application Execution Times on a Multi-Core Platform*

1 Benoît Dupont de Dinechin, Yves Durand, Duco van Amstel, and Alexandre Ghiti. Guaran- teed services of the noc of a manycore processor. In Proceedings of the 2014 International Workshop on Network on Chip Architectures, NoCArc’14, Cambridge, United Kingdom,
December 13-14, 2014, pages 11–16, 2014. doi:10.1145/2685342.2685344.

2 Benoît Dupont de Dinechin, Duco van Amstel, Marc Poulhiès, and Guillaume Lager. Time- critical computing on a single-chip massively parallel processor. In Design, Automation &
Test in Europe Conference & Exhibition, DATE 2014, Dresden, Germany, March 24-28, 2014, pages 1–6, 2014. doi:10.7873/DATE.2014.110.

3 Benjamin Lesage, David Griffin, Sebastian Altmeyer, and Robert I. Davis. Static prob- abilistic timing analysis for multi-path programs. In 2015 IEEE Real-Time Systems Symposium, RTSS 2015, San Antonio, Texas, USA, December 1-4, 2015, pages 361–372, 2015. doi:10.1109/RTSS.2015.41.

4 Vincent Nélis, Patrick Meumeu Yomsi, and Luís Miguel Pinho. Methodologies for the WCET analysis of parallel applications on many-core architectures. In 2015 Euromicro
Conference on Digital System Design, DSD 2015, Madeira, Portugal, August 26-28, 2015, pages 748–755, 2015. doi:10.1109/DSD.2015.105.

5 Timing Analysis on Code-Level. http://http://www.tacle.eu/index.php/activities/ taclebench. Accessed: 2016-05-06.

6 Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter Puschner, Jan Staschulat, and Per Stenström. The Worst-case Execution-time Problem; Overview of Methods and Survey of Tools. ACM Trans. Embed. Comput. Syst., 7(3):36:1–36:53, 2008.

7 Reinhard Wilhelm, Daniel Grund, Jan Reineke, Marc Schlickling, Markus Pister, and Christian Ferdinand. Memory Hierarchies, Pipelines, and Buses for Future Architectures in Time-Critical Embedded Systems. IEEE Trans. on CAD of Integrated Circuits and Systems ,28(7):966–978, 2009. doi:10.1109/TCAD.2009.2013287.

reference 2-34

Multi-core Interference-Sensitive WCET Analysis Leveraging Runtime Resource Capacity Enforcement
[1] EASA, “Certification memorandum - development assurance of airborne
electronic hardware (chapter 9),” Software & Complex Electronic
Hardware section, European Aviation Safety Agency, CM EASA CM

• SWCEH - 001 Issue 01, 11th Aug. 2011.
  [2] RTCA, DO-297 - Integrated Modular Avionics (IMA) Development
  Guidance and Certification Considerations, Std., 2005.
  [3] A. Wilson, W. River, T. Preyssler, and W. River, “Incremental certification
  and integrated modular avionics,” Proceedings of the 27th
  IEEE/AIAA Digital Avionics Systems Conference (DASC), pp. 1–8,

[4] Aeronautical Radio Inc., “ARINC 653: Avionics application software
standard interface,” Oct. 2003, 2551 Riva Road, Annapolis, MD 21401,
U.S.A.
[5] RTCA, DO-178C/ED-12C - Software considerations in airborne systems
and equipment certification, RTCA, Inc Std., 2012.
[6] C. Rochange and P. Sainrat, “Multicores and critical systems: Challenges
for temporal analysability,” SAE AeroTech Congress & Exhibition,
pp. 1–15, 2011.
[7] J. Littlefield-Lawwill and L. Kinnan, “System considerations for robust
time and space partitioning in integrated modular avionics,” Proceedings
of the 27th Digital Avionics Systems Conference, 2008.
[8] C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt,
H. Theiling, S. Thesing, and R. Wilhelm, “Reliable and precise WCET
determination for a real-life processor,” in Proceedings of EMSOFT
2001, First Workshop on Embedded Software, ser. Lecture Notes in
Computer Science, vol. 2211. Springer-Verlag, 2001, pp. 469–485.
[9] C. Ferdinand, “Cache Behavior Prediction for Real-Time Systems,”
Ph.D. dissertation, Saarland University, 1997.
[10] H. Theiling and C. Ferdinand, “Combining abstract interpretation and
ILP for microarchitecture modelling and program path analysis,” in
Proceedings of the 19th IEEE Real-Time Systems Symposium, Madrid,
Spain, Dec. 1998, pp. 144–153.
[11] J. Reineke, B. Wachter, S. Thesing, R. Wilhelm, I. Polian, J. Eisinger,
and B. Becker, “A Definition and Classification of Timing Anomalies,”
in International Workshop on Worst-Case Execution Time Analysis
(WCET), F. Mueller, Ed., July 2006.
[12] T. Lundqvist and P. Stenstr¨om, “Timing anomalies in dynamically
scheduled microprocessors,” in Real-Time Systems Symposium (RTSS),
December 1999.
[13] R. Kirner and P. Puschner, “Obstacles in worst-case execution time
analysis,” in Proceedings of the 11th IEEE Symposium on Object
Oriented Real-Time Distributed Computing (ISORC), 2008, pp. 333–
339.
[14] J. Reineke, D. Grund, C. Berg, and R. Wilhelm, “Timing predictability
of cache replacement policies,” Real-Time Systems, vol. 37, no. 2, pp.
99–122, 2007.
[15] C. Cullmann, C. Ferdinand, G. Gebhard, D. Grund, C. Maiza,
J. Reineke, B. Triquet, and R. Wilhelm, “Predictability considerations
in the design of multi-core embedded systems,” in Proceedings of
Embedded Real Time Software and Systems, May 2010, pp. 36–42.
[16] S. Thesing, R. Heckmann, J. Souyris, F. Randimbivololona, M. Langenbach,
R. Wilhelm, and C. Ferdinand, “An Abstract Interpretation-Based
Timing Validation of Hard Real-Time Avionics Software,” Proceedings
of 33th International Conference on Dependable Systems and Networks
(DSN), 2003.
[17] SYSGO AG, “Rheinmetall selects DO-178B certifiable PikeOS
from SYSGO for A400M project,” http://www.sysgo.com/en/newsevents/
press/press/details/article/rheinmetall-selects-do-178bcertifiable-
pikeos-from-sysgo-for-a400m-project/.
[18] ——, “Airbus selects SYSGOs PikeOS as DO-178B reference
platform for the A350 XWB,” http://www.sysgo.com/en/newsevents/
press/press/details/article/airbus-selects-sysgos-pikeos-as-do-
178b-reference-platform-for-the-a350-xwb/.
[19] R. Wilhelm, D. Grund, J. Reineke, M. Schlickling, M. Pister, and
C. Ferdinand, “Memory hierarchies, pipelines, and buses for future
architectures in time-critical embedded systems,” IEEE TCAD, 2009.
[20] The Embedded Microprocessor Benchmark Consortium,
“EEMBC AutoBench 1.1 benchmark software,”
http://www.eembc.org/benchmark/automotive sl.php.
[21] J. Nowotsch and M. Paulitsch, “Leveraging multi-core computing
architectures in avionics,” Proceedings of the 9th European Dependable
Computing Conference, 2012.
[22] Freescale Semiconductor, “e500mc core reference manual, all revisions,
chapter 4.13,” 2012.
[23] B. Green, J. Marotta, B. Petre, K. Lillestolen, R. Spencer, N. Gupta,
D. O’Leary, J. Lee, J. Strasburger, A. Nordsieck, B. Manners, and
R. Mahapatra, “DOT/FAA/AR-11/2 - handbook of the selection and
evaluation of microprocessors for airborne systems,” FAA, Tech. Rep.,
2011.
[24] F. Bellosa, “Process cruise control: Throttling memory access in a soft
real-time environment,” University of Erlangen, Tech. Rep., 1997.
[25] ——, “Memory access - the third dimension of scheduling,” University
of Erlangen, Tech. Rep., 1997.
[26] H. Yun, G. Yao, R. Pellizzoni, M. Caccamo, and L. Sha, “Memory
access control in multiprocessor for real-time systems with mixed
criticality,” Proceedings of 24th Euromicro Conference on Real-Time
Systems (ECRTS), pp. 299 – 308, 2012.
[27] A. Schranzhofer, J.-j. Chen, and L. Thiele, “Timing predictability on
multi-processor systems with shared resources,” Embedded Systems
Week - Workshop on Reconciling Performance with Predictability, 2009.
[28] R. Pellizzoni, E. Betti, S. Bak, G. Yao, J. Criswell, M. Caccamo, and
R. Kegley, “A predictable execution model for COTS-based embedded
systems,” Proceedings of the 17th IEEE Real-Time and Embedded
Technology and Applications Symposium, pp. 269 – 279, 2011.
[29] F. Boniol, H. Cass´e, E. Noulard, and C. Pagetti, “Deterministic execution
model on COTS hardware,” Proceedings of the 25st international
conference on Architecture of computing systems (ARCS), 2012.
[30] J. Yan and W. Zhang, “WCET analysis for multi-core processors with
shared L2 instruction caches,” Proceedings of the 14th IEEE Real-Time
and Embedded Technology and Applications Symposium, pp. 80–89,
2008.
[31] Y. Li, V. Suhendra, Y. Liang, T. Mitra, and A. Roychoudhury, “Timing
analysis of concurrent programs running on shared cache multi-cores,”
Proceedings of the 30th IEEE Real-Time Systems Symposium, pp. 57 –
67, 2009.
[32] D. Hardy, T. Piquet, and I. Puaut, “Using bypass to tighten WCET
estimates for multi-core processors with shared instruction caches,”
Proceedings of the 30th IEEE Real-Time Systems Symposium, 2009.
[33] S. Chattopadhyay, A. Roychoudhury, and T. Mitra, “Modeling shared
cache and bus in multi-cores for timing analysis,” Proceedings of the
13th International Workshop on Software & Compilers for Embedded
Systems, 2010.
[34] T. Kelter, H. Falk, P. Marwedel, S. Chattopadhyay, and A. Roychoudhury,
“Bus-aware multicore WCET analysis through TDMA offset
bounds,” Proceedings of the 23rd Euromicro Conference on Real-Time
Systems, 2011.
[35] S. Chattopadhyay, C. L. Kee, A. Roychoudhury, T. Kelter, P. Marwedel,
and H. Falk, “A unified WCET analysis framework for multi-core platforms,”
Proceedings of the 18th Real Time and Embedded Technology
and Applications Symposium, 2012.
[36] J. Rosen, A. Andrei, P. Eles, and Z. Peng, “Bus access optimization for predictable implementation of real-time applications on multiprocessor systems-on-chip,” Proceedings of the 28th IEEE International Real-Time Systems Symposium, pp. 49 – 60, 2007.
[37] M. Paolieri, F. J. Cazorla, M. Valero, and G. Bernat, “Hardware support
for WCET analysis of hard real-time multicore systems,” Proceedings of the 36th annual international symposium on Computer architecture, 2009.

reference 2-35

[1] J.Woodcock,P.G.Larsen,J.Bicarregui,J.Fitzgerald,Formalmethods:practiceandexperience,ACMComput.Surv.41(4)(2009)1–36.[2] B. Jacobs, J. Smans, F. Piessens, A quick tour of the VeriFast program verifier, in: APLAS, 2010, in: LNCS, vol. 6461, Springer, Heidelberg, 2010,pp.304–311.[3] P. O’Hearn, J. Reynolds, H. Yang, Local reasoning about programs that alter data structures, in: CSL, 2001, in: LNCS, vol. 2142, Springer, Heidelberg,2001,pp.1–19.[4] J.Berdine,C.Calcagno,P.O’Hearn,Symbolicexecutionwithseparationlogic,in:APLAS,2005,in:LNCS,vol.3780,Springer,Heidelberg,2005,pp.52–68.[5] R.Bornat,C.Calcagno,P.O’Hearn,M.Parkinson,Permissionaccountinginseparationlogic,in:POPL2005,ACM,NewYork,2005,pp.259–270.[6] ISO/IEC,9899:2011,Informationtechnology–Programminglanguages–C,availableathttp://www.iso.org/iso/iso_catalogue/catalogue_tc/catalogue_detail.htm?csnumber=57853,2011.[7] M. Parkinson, Class invariants: the end of the road? in: International Workshop on Aliasing, Confinement and Ownership in Object-orientedProgramming,IWACO,2007.[8] Oracle,Javacardtechnology,availableathttp://www.oracle.com/technetwork/java/javacard/overview/,2011.[9] D.DeCock,K.Wouters,B.Preneel,IntroductiontotheBelgianEIDcard,in:PublicKeyInfrastructure,in:LNCS,vol.3093,Springer,Heidelberg,2004,pp.621–622.[10] P. Philippaerts, F. Vogels, J. Smans, B. Jacobs, F. Piessens, The Belgian electronic identity card: a verification case study, in: AVOCS, in: ElectronicCommunicationsoftheEASST,vol.46,2011,pp.1–16.[11] IEEE standard for information technology – portable operating system interface (POSIX) base specifications, Issue 7, Tech. Rep. 1003.1-2008, IEEE,2008.[12] W. Penninckx, J.T. Mühlberg, J. Smans, B. Jacobs, F. Piessens, Sound formal verification of Linux’s USB BP keyboard driver, in: NFM 2012, in: LNCS,vol.7226,Springer,Heidelberg,2012,pp.210–215.[13] J.C. Filliâtre, C. Marché, The Why/Krakatoa/Caduceus platform for deductive program verification, in: CAV 2007, in: LNCS, vol. 4590, Springer,Heidelberg,2007,pp.173–177.[14] B.Jacobs,J.Smans,P.Philippaerts,F.Vogels,W.Penninckx,F.Piessens,VeriFast:Apowerful,sound,predictable,fastverifierforCandJava,in:NASAFormalMethods2011,in:LNCS,vol.6617,Springer,Heidelberg,2011,pp.41–55.[15] H.Yang,O.Lee,J.Berdine,C.Calcagno,B.Cook,D.Distefano,P.O’Hearn,Scalableshapeanalysisforsystemscode,in:CAV2008,in:LNCS,vol.5123,Springer,Heidelberg,2008,pp.385–398.[16] J.Brotherston,R.Bornat,C.Calcagno,Cyclicproofsofprogramterminationinseparationlogic,SIGPLANNot.43(2008)101–112.[17] B.Cook,A.Gotsman,A.Podelski,A.Rybalchenko,M.Y.Vardi,Provingthatprogramseventuallydosomethinggood,SIGPLANNot.42(2007)265–276.[18] C.Calcagno,M.Parkinson,V.Vafeiadis,Modularsafetycheckingforfine-grainedconcurrency,in:SAS’07,in:LNCS,vol.4634,Springer,Heidelberg,2007,pp.233–248.[19] A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, M. Sagiv, Local reasoning for storable locks and threads, in: APLAS ’07, in: LNCS, vol. 4807, Springer,Heidelberg,2007,pp.19–37.[20] D.Distefano,M.J.Parkinson,jStar:TowardspracticalverificationforJava,in:OOPSLA’08,ACM,NewYork,2008,pp.213–226.[21] D.Distefano,P.O’Hearn, H.Yang,Alocal shapeanalysisbasedonseparation logic,in:TACAS2006, in:LNCS,vol.3920, Springer, Heidelberg,2006,pp.287–302.[22] J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, T. Wies, H. Yang, Shape analysis for composite data structures, in: CAV 2007, in: LNCS,vol.4590,Springer,Heidelberg,2007,pp.178–192.[23] C.Calcagno,D.Distefano,P.O’Hearn,H.Yang,Compositionalshapeanalysisbymeansofbi-abduction,SIGPLANNot.44(1)(2009)289–300.[24] D.Distefano,Attackinglargeindustrialcodewithbi-abductiveinference,in:FMICS2009,in:LNCS,vol.5825,Springer,Heidelberg,2009,pp.1–8.[25] F. Vogels, B. Jacobs, F. Piessens, J. Smans, Annotation inference for separation logic based verifiers, in: FMOODS 2011, in: LNCS, vol. 6722, Springer,Heidelberg,2011,pp.319–333.[26] C.Flanagan,K.Rustan,M.Leino,M.Lillibridge,G.Nelson,J.B.Saxe,R.Stata,ExtendedstaticcheckingforJava,in:PLDI2002,ACM,NewYork,2002,pp.234–245.[27] W.Mostowski,E.Poll,MidletnavigationgraphsinJML,in:SBMF2010,in:LNCS,vol.6527,Springer,Heidelberg,2010,pp.17–32.[28] N.Cataño,M.Huisman,FormalspecificationofGemplus’electronicpursecasestudyusingESC/Java,in:FormalMethodsEurope,in:LNCS,vol.2391,Springer,Heidelberg,2002,pp.272–289.[29] K.R.M.Leino,G.Nelson,J.B.Saxe,ESC/Javauser’smanual,Tech.rep.,CompaqSystemsResearchCenter,2000.[30] B. Jacobs, F. Piessens, Expressive modular fine-grained concurrency specification, in: Proceedings of the 38th Annual ACM SIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,POPL2011,46(1)2011,pp.271–282.[31] B.E.G.Gomes,A.M.Moreira,D.Déharbe,DevelopingJavacardapplicationswithB,in:SBMF2005,in:ENTCS,vol.184,Elsevier,2005,pp.81–96.[32] M. Huisman, D. Gurov, C. Sprenger, G. Chugunov, Checking absence of illicit applet interactions: a case study, in: FASE 2004, in: LNCS, vol. 2984,Springer,Heidelberg,2004,pp.84–98.[33] W.Mostowski,FullyverifiedJavaCardAPIreferenceimplementation,in:InternationalVerificationWorkshop,VERIFY,2007.[34] W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, P.H. Schmitt, The KeY tool, Soft. Syst.Model.4(2005)32–54.[35] P.H.Schmitt,I.Tonin,VerifyingtheMondexcasestudy,in:SEFM2007,IEEE,Washington,2007,pp.47–58.[36] E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, J. ACM 50 (5) (2003)752–794.[37] T.A.Henzinger,R.Jhala,R.Majumdar,G.C.Necula,G.Sutre,W.Weimer,Temporal-safetyproofsforsystemscode,in:CAV2002,in:LNCS,vol.2402,Springer,Heidelberg,2002,pp.382–399.[38] T.Ball,E.Bounimova,B.Cook,V.Levin,J.Lichtenberg,C.McGarvey,B.Ondrusek,S.K.Rajamani,A.Ustuner,Thoroughstaticanalysisofdevicedrivers,SIGOPSOper.Syst.Rev.40(4)(2006)73–85.[39] J.T.Mühlberg,G.Lüttgen,BLASTingLinuxcode,in:FMICS,in:LNCS,vol.4346,Springer,Heidelberg,2007,pp.211–226.[40] T. Witkowski, N. Blanc, D. Kroening, G. Weissenbacher, Model checking concurrent Linux device drivers, in: ASE 2007, ACM, New York, 2007,pp.501–504.

reference on 2-36

Methods and Tools for the Formal Verification of Software

[1] Wolfgang Ahrendt et al. “The KeY tool”. In: Software and Systems Modeling 4 (1 2005), pp. 32–54. issn: 1619-1366. doi: 10.1007/s10270- 004-0058-x.
Mike Barnett et al. “Boogie: A Modular Reusable Verifier for Object- Oriented Programs”. In: Formal Methods for Components and Objects. Vol. 4111. Lecture Notes in Computer Science. Springer Berlin / Hei- delberg, 2006, pp. 364–387. doi: 10.1007/11804192_17.
Patrick Baudin et al. ACSL: ANSI/ISO C Specification Language. Version 1.5 – Carbon-20110201. 2011. url: http://frama-c.com/ download.html.
Bernhard Beckert, Reiner Ha ̈hnle, and Peter H. Schmitt, eds. Verifi- cation of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer-Verlag, 2007. isbn: 3-540-68977-X.
Bernhard Beckert and Claude March ́e. Formal Verification of Object- Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. Technical report. Fakulta ̈t fu ̈r Infor- matik, Universita ̈t Karlsruhe, 2010. url: http://digbib.ubka.uni- karlsruhe.de/volltexte/1000019083.
Sascha Bo ̈hme et al. “HOL-Boogie – An Interactive Prover-Backend for the Verifying C Compiler”. In: Journal of Automated Reasoning 44 (1–2 Feb. 2010), pp. 111–144. issn: 0168-7433. doi: 10.1007/s10817-
009-9142-9.
Armin Biere et al. “Symbolic Model Checking without BDDs”. In: Tools and Algorithms for the Construction and Analysis of Systems. Vol. 1579. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 1999, pp. 193–207. doi: 10.1007/3-540-49059-0_14.
CEA – LIST. Frama-C publications. 2011. url: http://bts.frama- c.com/dokuwiki/doku.php?id=mantis:frama-c:publications# jessie.
119
120 BIBLIOGRAPHY
[9] CEA – LIST. Frama-C/Jessie website. 2011. url: http://frama-
c.com/jessie.html.
[10] Patrice Chalin. “Improving JML: For a Safer and More Effective Language”. In: FME 2003: Formal Methods. Vol. 2805. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2003, pp. 440–461. isbn: 978-3-540-40828-4. doi: 10.1007/978-3-540-45236-2_25.
[11] Edmund Clarke and Daniel Kro ̈ning. “Hardware Verification using ANSI-C Programs as a Reference”. In: Proceedings of ASP-DAC 2003. IEEE Computer Society Press, Jan. 2003, pp. 308–311. isbn: 0-7803- 7659-5.
[12] Edmund Clarke, Daniel Kro ̈ning, and Flavio Lerda. “A Tool for Check- ing ANSI-C Programs”. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). Vol. 2988. Lecture Notes in Computer Science. Springer, 2004, pp. 168–176. isbn: 3-540-21299-X.
[13] Edmund M. Clarke and E. Allen Emerson. “Design and synthesis of synchronization skeletons using branching time temporal logic”. In: Logics of Programs. Vol. 131. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 1982, pp. 52–71. doi: 10.1007/BFb0025 774.
[14] Ernie Cohen et al. “Local Verification of Global Invariants in Concur- rent Programs”. In: Computer Aided Verification. Vol. 6174. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2010. doi: 10.1007/978-3-642-14295-6_42.
[15] Ernie Cohen et al. “VCC: A Practical System for Verifying Concurrent C”. In: Theorem Proving in Higher Order Logics. Vol. 5674. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2009, pp. 23– 42. doi: 10.1007/978-3-642-03359-9_2.
[16] Ernie Cohen et al. Verifying Concurrent C Programs with VCC. Work- ing draft, version 0.2. Apr. 18, 2011. url: http://vcc.codeplex. com/.
[17] Lo ̈ıc Correnson, Zaynah Dargaye, and Anne Pacalet. WP Plug-in (Draft) Manual. Version 0.3 for Carbon-20110201. 2011. url: http: //frama-c.com/download.html.
[18] Lo ̈ıc Correnson et al. Frama-C User Manual. Release Carbon-20110201. 2011. url: http://frama-c.com/download.html.
[19] David Crocker. David Crocker’s Verification Blog. 2011. url: http: //critical.eschertech.com/.
[20] David Crocker. “Perfect Developer: A tool for Object-Oriented Formal Specification and Refinement”. In: Tools Exhibition Notes at Formal Methods Europe. 2003. url: http://www.eschertech.com/papers/ index.php.
[21] David Crocker. Personal communication. Oct. 26, 2011.
[22] David Crocker.“Safe Object-Oriented Software: the Verified Design-by- Contract paradigm”. In: Practical Elements of Safety: Proceedings of the Twelfth Safety-critical Systems Symposium. Springer, 2004, pp. 19– 41. isbn: 9781852338008.
[23] David Crocker and Judith Carlton. A High Productivity Tool for Formally Verified Software Development. Technical report. Presented at the Formal Methods Workshop in Industrial Applications. Ghent, Belgium. Escher Technologies, 2003. url: http://www.eschertech. com/papers/index.php.
[24] David Crocker and Judith Carlton. “Verification of C Programs Using Automated Reasoning”. In: Fifth IEEE International Conference on Software Engineering and Formal Methods. 2007, pp. 7–14. isbn: 978- 0-7695-2884-7.
[25] Edsger W. Dijkstra. A Discipline of Programming. Upper Saddle River, NJ, USA: Prentice Hall, 1976. isbn: 013215871X.
[26] Edsger W. Dijkstra. “Guarded commands, nondeterminacy and formal derivation of programs”. In: Communications of the ACM 18 (8 Aug. 1975), pp. 453–457. issn: 0001-0782. doi: 10.1145/360933.360975.
[27] E. Allen Emerson. “The Beginning of Model Checking: A Personal Perspective”. In: 25 Years of Model Checking. Vol. 5000. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2008, pp. 27–45. doi: 10.1007/978-3-540-69850-0_2.
[28] Christian Engel et al. KeY Quicktour for JML. Oct. 6, 2010. url: http://www.key-project.org/case_studies/.
[29] Escher Technologies. Escher C Verifier datasheet. 2011. url: http: //www.eschertech.com/papers/index.php.
[30] Escher Technologies. Escher C Verifier Reference Manual. 2011. url: http://www.eschertech.com/product_documentation/ ecvReference/eCv_Manual.html.
[31] Escher Technologies. Escher C Verifier website. 2011. url: http: //www.eschertech.com/products/ecv.php.

[32] Escher Technologies. Perfect Developer for Critical Systems datasheet. 2011. url: http://www.eschertech.com/papers/index.php.
[33] Escher Technologies. Perfect Developer website. 2011. url: http: //www.eschertech.com/products/perfect_developer.php.
[34] Escher Technologies. Product Announcement. 2011. url: http://www. eschertech.com/products/announcements/2011may04.pdf.
[35] Escher Technologies. Safety-critical software. 2011. url: http://www. eschertech.com/products/safety.php.
[36] Escher Technologies. Universities using PD in teaching. 2011. url: http://www.eschertech.com/educational/universities_using. php.
[36] Ingo Feinerer. “Formal Program Verification: a Comparison of Selected Tools and Their Theoretical Foundations”. MA thesis. Technische Universita ̈t Wien, 2005.
[37] Ingo Feinerer and Gernot Salzer. “A Comparison of Tools for Teaching Formal Software Verification”. In: Formal Aspects of Computing 21.3
(May 2009), pp. 293–301. doi: 10.1007/s00165-008-0084-5.
[38] Robert W Floyd. “Assigning meanings to programs”. In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19 (1967), pp. 19–32.
[39] Formal Verification Group. CBMC website. 2011. url: http://www. cs.cmu.edu/~modelcheck/cbmc/.
[41]Formal Verification Group. CPROVER Manual. 2011. url: http: //www.cprover.org/cprover-manual/.
[42]Formal Verification Group. CPROVER website. 2011. url: http: //www.cprover.org/.
[43]Gerhard Gentzen. “Untersuchungen u ̈ber das logische Schließen I”. In: Mathematische Zeitschrift 39 (2 1934), pp. 176–210.
[44]David Gries. The Science of Programming. Springer, 1981. isbn: 038790641X.
[45]David Harel, Jerzy Tiuryn, and Dexter Kozen. Dynamic Logic. Cam- bridge, MA, USA: MIT Press, 2000. isbn: 0262082896.
[46]C. A. R. Hoare. “An axiomatic basis for computer programming”. In: Communications of the ACM 12 (10 Oct. 1969), pp. 576–580. issn: 0001-0782. doi: 10.1145/363235.363259.
[47] Michael Huth and Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (second edition). Cambridge University Press, 2004. isbn: 052154310X. url: http://pubs.doc.ic.ac.uk/ logic-computer-science-second/.
[48] ISO/IEC 9899:1999 Cor. 3:2007(E). Programming languages – C, WG14 N1256. Geneva, Switzerland: International Organization for Standardization, 2007. url: http://www.open-std.org/jtc1/sc22/wg14/www/standards.
[49] Bart Jacobs. VeriFast website. Katholieke Universiteit Leuven. 2011.
url: http://people.cs.kuleuven.be/~bart.jacobs/verifast/.
[50]Bart Jacobs and Frank Piessens. The VeriFast Program Verifier. Technical Report CW-520. Department of Computer Science, Katholieke Universiteit Leuven, Aug. 2008. url: http://www.cs.kuleuven.be/ publicaties/reports/cw/CW520.abs.html.
[51]Bart Jacobs and Frank Piessens. VeriFast Reference Manual. Jan. 14, 2011.
[52]Bart Jacobs, Jan Smans, and Frank Piessens. “A Quick Tour of the VeriFast Program Verifier”. In: Programming Languages and Systems. Vol. 6461. Lecture Notes in Computer Science. Springer Berlin / Hei- delberg, 2010, pp. 304–311. doi: 10.1007/978-3-642-17164-2_21.
[53]Bart Jacobs, Jan Smans, and Frank Piessens. The VeriFast Pro- gram Verifier: A Tutorial. Nov. 17, 2010. url: http://people.cs. kuleuven.be/~bart.jacobs/verifast/.
[54]Bart Jacobs et al. “VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java”. In: NASA Formal Methods. Vol. 6617. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2011, pp. 41– 55. doi: 10.1007/978-3-642-20398-5_4.
[55]Stanisl􏰁aw Ja ́skowski. “On the rules of suppositions in formal logic”. In: Studia Logica 1 (1934), pp. 5–32.
[56]Karlsruhe Institute of Technology. KeY changelog. Oct. 1, 2011. url: http://www.key-project.org/download/CHANGELOG.
[57]Karlsruhe Institute of Technology. KeY known issues. Oct. 1, 2011. url: http://www.key-project.org/download/KnownIssues.txt.
[58]Karlsruhe Institute of Technology. KeY website. 2011. url: http: //www.key-project.org/.
[59] JamesC.King.“Symbolicexecutionandprogramtesting”.In:Commu- nications of the ACM 19 (7 July 1976), pp. 385–394. issn: 0001-0782. doi: 10.1145/360248.360252.
[60] Daniel Kroening, Edmund Clarke, and Karen Yorav. “Behavioral Con- sistency of C and Verilog Programs Using Bounded Model Checking”. In: Proceedings of DAC 2003. ACM Press, 2003, pp. 368–371. isbn: 1-58113-688-9.
[61] Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes: the Automata-Theoretic Approach. Princeton University Press, 1994. isbn: 9780691034362. url: http://books.google.com/ books?id=iB5066RPRxsC.
[62] Laboratoire de Recherche en Informatique. Why website. 2011. url: http://why.lri.fr/.
[63] Daniel Larsson and Wojciech Mostowski. “Specifying Java Card API in OCL”. In: Electronic Notes in Theoretical Computer Science 102
(Nov. 2004), pp. 3–19. issn: 1571-0661. doi: 10.1016/j.entcs.2003. 09.001.
[64] Claude March ́e and Yannick Moy. Jessie Plugin Tutorial. Frama-C version: Carbon, Jessie plugin version: 2.28. 2010. url: http://frama- c.com/download.html.
[65] Bertrand Meyer. Object-Oriented Software Construction. 2nd ed. Pren- tice Hall, 1997. Chap. 11. isbn: 0-13-629155-4.
[66] Microsoft Research. Boogie website. 2011. url: http://research. microsoft.com/en-us/projects/boogie/.
[67] Microsoft Research. VCC website. 2011. url: http://vcc.codeplex. com/.
[68] MISRA. Guidelines for the Use of the C Language in Critical Systems. MISRA, 2004. isbn: 0952415623.
[69] MISRA. MISRA website. 2009. url: http://www.misra.org.uk/ MISRAHome/WhatisMISRA/tabid/66/Default.aspx.
[70] S. Owre, J. M. Rushby, and N. Shankar.“PVS: A Prototype Verification System”. In: 11th International Conference on Automated Deduction (CADE). Vol. 607. Lecture Notes in Artificial Intelligence. Saratoga, NY, USA: Springer-Verlag, June 1992, pp. 748–752. url: http://www. csl.sri.com/papers/cade92-pvs/.
[71] S. Owre et al. PVS System Guide. 2001. url: http://pvs.csl.sri. com/documentation.shtml.

[72] Sam Owre. Prototype Verification System website. SRI International.
2011. url: http://pvs.csl.sri.com/.
[73] Sam Owre and Natarajan Shankar. “Writing PVS Proof Strategies”. In: Design and Application of Strategies/Tactics in Higher Order Log- ics (STRATA 2003). NASA Conference Publication CP-2003-212448. Hampton, VA, USA: NASA Langley Research Center, Sept. 2003, pp. 1–15.
[74] John C. Reynolds. “Separation Logic: A Logic for Shared Mutable Data Structures”. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. LICS ’02. Washington, DC, USA: IEEE Computer Society, 2002, pp. 55–74. isbn: 0-7695-1483-9.
[75] Peter H. Schmitt and Benjamin Weiß.“Inferring Invariants by Symbolic Execution”. In: Proceedings, 4th International Verification Workshop (VERIFY’07). Vol. 259. CEUR Workshop Proceedings. CEUR-WS.org, 2007, pp. 195–210.
[76] Sun Microsystems. Virtual Machine Specification. Java Card Platform, Version 2.2.2. 2005. url: http://java.sun.com/javacard/specs. html.
[77] Technische Universita ̈t Berlin, Institut fu ̈r Softwaretechnik und The- oretische Informatik. Verifikation von C Programmen in der Praxis. 2011. url: http://www.swt.tu-berlin.de/menue/studium_und_ lehre/lehrveranstaltungen/vcc/.
[78] Verisoft XT consortium. Verisoft XT website. 2011. url: http://www. verisoftxt.de/.
[79] Fr ́ed ́eric Vogels et al. “Annotation Inference for Separation Logic Based Verifiers”. In: Formal Techniques for Distributed Systems. Vol. 6722. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2011, pp. 319–333. doi: 10.1007/978-3-642-21461-5_21.
[80] Ju ̈rgenWinkler.FregeProgramProverwebsite.Friedrich-Schiller- Universita ̈t Jena. 2009. url: http://psc.informatik.uni-jena. de/fpp/fpp-main.htm.
[81] Ju ̈rgen Winkler. “The Frege Program Prover”. In: 42. Internationales Wissenschaftliches Kolloquium, Technische Universita ̈t Ilmenau, Band 1. 1997, pp. 116–121.

reference on 2-37

[ANSI 89] [Anderson 80]
[Bell 72] [Canaday 69]
[Corbato 62] [Cox 86]
References
American National Standards Institute, American National Standard for Information Systems—Programming Language C, X3.159-1989.
B. Anderson, ‘Type syntax in the language C: an object lesson in syntactic innova- tion,’ SIGPLAN Notices 15 (3), March, 1980, pp. 21-27.
J. R. Bell, ‘Threaded Code,’ C. ACM 16 (6), pp. 370-372.
R. H. Canaday and D. M. Ritchie, ‘Bell Laboratories BCPL,’ AT&T Bell Laborato-
ries internal memorandum, May, 1969.
F. J. Corbato, M. Merwin-Dagget, R. C. Daley, ‘An Experimental Time-sharing Sys- tem,’ AFIPS Conf. Proc. SJCC, 1962, pp. 335-344.
B. J. Cox and A. J. Novobilski, Object-Oriented Programming: An Evolutionary
Ritchie Development of C 15
[Gehani 89] [Jensen 74]
[Johnson 73] [Johnson 78a] [Johnson 78b] [Johnson 79a]
[Johnson 79b]
[Kernighan 78] [Kernighan 81] [Lesk 73] [MacDonald 89] [McClure 65] [McIlroy 60] [McIlroy 79] [Meyer 88] [Nelson 91] [Organick 75] [Richards 67] [Richards 79] [Ritchie 78] [Ritchie 84] [Ritchie 90] [Sethi 81]
Approach, Addison-Wesley: Reading, Mass., 1986. Second edition, 1991.
N. H. Gehani and W. D. Roome, Concurrent C, Silicon Press: Summit, NJ, 1989.
K. Jensen and N. Wirth, Pascal User Manual and Report, Springer-Verlag: New York, Heidelberg, Berlin. Second Edition, 1974.
S. C. Johnson and B. W. Kernighan, ‘The Programming Language B,’ Comp. Sci. Tech. Report #8, AT&T Bell Laboratories (January 1973).
S. C. Johnson and D. M. Ritchie, ‘Portability of C Programs and the UNIX System,’ Bell Sys. Tech. J. 57 (6) (part 2), July-Aug, 1978.
S. C. Johnson, ‘A Portable Compiler: Theory and Practice,’ Proc. 5th ACM POPL Symposium (January 1978).
S. C. Johnson, ‘Yet another compiler-compiler,’ in Unix Programmer’s Manual, Sev- enth Edition, Vol. 2A, M. D. McIlroy and B. W. Kernighan, eds. AT&T Bell Labora- tories: Murray Hill, NJ, 1979.
S. C. Johnson, ‘Lint, a Program Checker,’ in Unix Programmer’s Manual, Seventh Edition, Vol. 2B, M. D. McIlroy and B. W. Kernighan, eds. AT&T Bell Laboratories: Murray Hill, NJ, 1979.
B. W. Kernighan and D. M. Ritchie, The C Programming Language, Prentice-Hall: Englewood Cliffs, NJ, 1978. Second edition, 1988.
B. W. Kernighan, ‘Why Pascal is not my favorite programming language,’ Comp. Sci. Tech. Rep. #100, AT&T Bell Laboratories, 1981.
M. E. Lesk, ‘A Portable I/O Package,’ AT&T Bell Laboratories internal memoran- dum ca. 1973.
T. MacDonald, ‘Arrays of variable length,’ J. C Lang. Trans 1 (3), Dec. 1989, pp. 215-233.
R. M. McClure, ‘TMG—A Syntax Directed Compiler,’ Proc. 20th ACM National Conf. (1965), pp. 262-274.
M. D. McIlroy, ‘Macro Instruction Extensions of Compiler Languages,’ C. ACM 3 (4), pp. 214-220.
M. D. McIlroy and B. W. Kernighan, eds, Unix Programmer’s Manual, Seventh Edi- tion, Vol. I, AT&T Bell Laboratories: Murray Hill, NJ, 1979.
B. Meyer, Object-oriented Software Construction, Prentice-Hall: Englewood Cliffs, NJ, 1988.
G. Nelson, Systems Programming with Modula-3, Prentice-Hall: Englewood Cliffs, NJ, 1991.
E. I. Organick, The Multics System: An Examination of its Structure, MIT Press: Cambridge, Mass., 1975.
M. Richards, ‘The BCPL Reference Manual,’ MIT Project MAC Memorandum M- 352, July 1967.
M. Richards and C. Whitbey-Strevens, BCPL: The Language and its Compiler, Cam- bridge Univ. Press: Cambridge, 1979.
D. M. Ritchie, ‘UNIX: A Retrospective,’ Bell Sys. Tech. J. 57 (6) (part 2), July-Aug, 1978.
D. M. Ritchie, ‘The Evolution of the UNIX Time-sharing System,’ AT&T Bell Labs. Tech. J. 63 (8) (part 2), Oct. 1984.
Ritchie, ‘Variable-size arrays in C,’ J. C Lang. Trans. 2 (2), Sept. 1990, pp.
R. Sethi, ‘Uniform syntax for type expressions and declarators,’ Softw. Prac. and Exp.11 (6), June 1981, pp. 623-628.
A. Snyder, A Portable Compiler for the Language C, MIT: Cambridge, Mass., 1974.[Snyder 74]
J. E. Stoy and C. Strachey, ‘OS6—An experimental operating system for a small computer. Part I: General principles and structure,’ Comp J. 15, (Aug. 1972), pp. D. M. 81-86. 117-124. [Stoy 72]
B. Stroustrup, The C++ Programming Language, Addison-Wesley: Reading, Mass., 1986. Second edition, 1991.[Stroustrup 86]
C. P. Thacker, E. M. McCreight, B. W. Lampson, R. F. Sproull, D. R. Boggs, ‘Alto: A Personal Computer,’ in Computer Structures: Principles and Examples, D. Sieworek, C. G. Bell, A. Newell, McGraw-Hill: New York, 1982.[Thacker 79]
C* Programming Guide, Thinking Machines Corp.: Cambridge Mass., 1990.[Thinking 90]
K. Thompson, ‘Bon—an Interactive Language,’ undated AT&T Bell Laboratories internal memorandum (ca. 1969).[Thompson 69]
A. van Wijngaarden, B. J. Mailloux, J. E. Peck, C. H. Koster, M. Sintzoff, C. Lindsey, L. G. Meertens, R. G. Fisker, ‘Revised report on the algorithmic language Algol 68,’ Acta Informatica 5, pp. 1-236.[Wijngaarden 75]

reference on 2-38

[1] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL version 1.5, Implementation in Carbon-20110201, February 2011. http://frama-c.com/acsl.html.
[2] Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL, ANSI/ISO C Speci􏰀cation Language, February 2011. Vesion 1.5. http://frama-c.com/acsl.html.
[3] Patrice Chalin. Reassessing JML's logical foundation. In Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP'05), Glasgow, Scotland, July 2005.
[4] Patrice Chalin. A sound assertion semantics for the dependable systems evolution veri- fying compiler. In Proceedings of the International Conference on Software Engineering (ICSE'07), pages 23-33, Los Alamitos, CA, USA, 2007. IEEE Computer Society.
[5] Loïc Correnson, Pascal Cuoq, Armand Puccetti, and Julien Signoles. Frama-C User Manual, February 2011. http://frama-c.com.
[6] Pascal Cuoq and Virgile Prevosto. Frama-C's value analysis plug-in, February 2011. http: //frama-c.com/value.html.
[7] International Organization for Standardization (ISO). The ANSI C standard (C99). http: //www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf.
[8] Brian Kernighan and Dennis Ritchie. The C Programming Language (2nd Ed.). Prentice- Hall, 1988.
[9] Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA 2000 Companion, Minneapolis, Minnesota, pages 105-106, 2000.

reference on 3-11

Safety-Critical Software Development Using Automatic Production Code Generation

1. IEC 61508-3:1998. International Standard IEC 61508 Functional safety of electrical/electronic/ programmable electronic safety-related systems – Part 3: Software requirements. 1st edition, 1998
2. ISO/WD 26262:2005. Road vehicles - Functional safety: Working Draft, 2005
3. MISRA-C:2004. The Motor Industry Software Reliability Association: Guidelines for the use of the C language in critical systems. 2004
4. HIS Working Group Software Test: Gemeinsames Subset der MISRA C Guidelines. Version 2.0, 2006
5. MathWorks Automotive Advisory Board: Controller Style Guidelines for Production Intent Development Using MATLAB, Simulink, and Stateflow. Version 1.00, 2001
6. Andreas Bärwald: IEC 61508 & MISRA C - The Benefits of Utilising IEC 61508 and MISRA C for Automotive Applications. 1st IEE Automotive Electronics Conference, London, UK, 2005
7. Mirko Conrad, Heiko Dörr: Deployment of Model- based Software Development in Safety-related Applications - Challenges and Solutions Scenarios. Proc. Modellierung 2006, Innsbruck, Austria, 2006, LNI Vol P-82, p. 245-254
8. Tom Erkkinen, Damon Hachmeister: Checking Code and Models in Production Environments. MATLAB Digest, July 2003
9. Matthias Findeis, Ilona Pabst: Functional Safety in the Automotive Industry, Process and methods. VDA Winter meeting 2006
10. Ekkehard Pofahl: The application of IEC 61508 in the automotive industry. 2005
11. Jim Tung: Enhanced Test and Verification Capabilities Using Model-Based Design. In: J. R. Pimentel (Ed.): Safety-Critical Automotive Systems, SAE International, 2006 (SAE paper 2006-01-1445)
12. MathWorks Connection Program, Teamcenter for System Engineering, www.mathworks.com/products/connections/product _main.html?prod_id=729
13. MathWorks Connection Program, Polyspace Desktop,
    www.mathworks.com/products/connections/product
    _main.html?prod_id=665
14. Real-Time Workshop® Embedded Coder User’s Guide. The MathWorks Inc, Version 4, 2006

ref. on 3-4

Unexcitability analysis of SEus affecting the routing structure of SRAM-based FPGAs

1. R. Baumann. Radiation-induced Soft Errors in Advanced Semiconductor Technologies. IEEE Transactions on Device and Materials Reliability, 5(3):305 -- 316, September 2005.Google ScholarCross Ref
   S. Bensalem, V. Ganesh, Y. Lakhnech, C. Munoz, S. Owre, H. Rueß, J. Rushby, V. Rusu, H. Saidi, N. Shankar, E. Singerman, and A. Tiwari. An Overview of SAL. In Proceedings of the Fifth NASA Langley Formal Methods Workshop (LFM 2000), pages 187--196, 2000.Google Scholar
   C. Bernardeschi, L. Cassano, and A. Domenici. SEU-X: a SEu Un-uXecitbility prover for SRAM-FPGAs. In Proceedings of the 18th IEEE International On-Line Testing Symposium (IOLTS2012), June 2012. Google ScholarDigital Library
   C. Bernardeschi, L. Cassano, A. Domenici, and L. Sterpone. Accurate Simulation of SEUs in the Configuration Memory of SRAM-based FPGAs. In Proceedings of the IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems (DFT 2012), 2012. Google ScholarDigital Library
   European Committee for Electrotechnical Standardization (CENELEC). EN 50129: Railway applications - Communications, signaling and processing systems - Safety related electronic systems for signaling, February 2003.Google Scholar
   P. Graham, M. Caffrey, J. Zimmerman, D. E. Johnson, P. Sundararajan, and C. Patterson. Consequences and Categories of SRAM FPGA Configuration SEUs. In Proceedings of the 6th Military and Aerospace Applications of Programmable Logic Devices (MAPLD'03), September 2003.Google Scholar
   International Atomic Energy Agency (IAEA). NS-G-1.3: Instrumentation and Control Systems Important to Safety in Nuclear Power Plants, 2002.Google Scholar
   International Organization for Standardization (ISO). 26262--5: Road vehicles - Functional safety - Part 5. Product development: hardware level, December 2009.Google Scholar
   I. Kuon, R. Tessier, and J. Rose. FPGA Architecture: Survey and Challenges. Foundations and Trends Electronic Design Automation, 2(2):135--253, Feb. 2008. Google ScholarDigital Library
   D. Long, M. Iyer, and M. Abramovici. FILL and FUNI: Algorithms to Identify Illegal States and Sequential Untestable Faults. ACM Transaction on Design Automation of Electronic Systems, 5(3):632--657, 2000. Google ScholarDigital Library
   J. Raik, H. Fujiwara, R. Ubar, and A. Krivenko. Untestable Fault Identification in Sequential Circuits Using Model-Checking. In Proceedings of the 17th Asian Test Symposium (ATS'08), pages 21--26, 2008. Google ScholarDigital Library
   J. Raik, A. Rannaste, M. Jenihhin, T. Viilukas, R. Ubar, and H. Fujiwara. Constraint-Based Hierarchical Untestability Identification for Synchronous Sequential Circuits. In Proceedings of the 16th European Test Symposium (ETS'11), pages 147--152, 2011. Google ScholarDigital Library
   J. Raik, R. Ubar, A. Krivenko, and M. Kruus. Hierarchical Identification of Untestable Faults in Sequential Circuits. In Proceedings of the 10th Euromicro Conference on Digital System Design Architectures, Methods and Tools (DSD'07), 2007. Google ScholarDigital Library
   M. Rebaudengo, M. Sonza Reorda, and M. Violante. A new functional fault model for FPGA application-oriented testing. In Proceedings of the 17th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems (DFT 2002), pages 372 -- 380, 2002. Google ScholarDigital Library
   K. Rozier. Linear Temporal Logic Symbolic Model Checking. Computer Science Review, 5(2):163 -- 203, 2011. Google ScholarDigital Library
   D. Tille and R. Drechsler. A Fast Untestability Proof for SAT-based ATPG. In Proceedings of the 12th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS'09), pages 38--43, 2009. Google ScholarDigital Library
   M. Violante, N. Battezzati, and L. Sterpone. Reconfigurable Field Programmable Gate Arrays for Mission-Critical Applications. Springer Science & Business Media, 2011.Google Scholar

ref. 3-6

[BR07] J. Bowen, S. Reeves. Formal Models for Informal GUI Designs. Electronic Notes
in Theoretical Computer Science 183:57–72, 2007.
[HBWM10] A. Hinze, J. Bowen, Y. Wang, R. Malik. Model-driven GUI & interaction design
using emulation. In Sukaviriya et al. (eds.), EICS. Pp. 273–278. ACM, 2010.
[HME09] A. Hinze, Y. Michel, L. Eschner. Event-based Communication for Location-based
Service Collaboration. In Bouguettaya and Lin (eds.), ADC. CRPIT 92, pp. 127–
136. Australian Computer Society, 2009.
[HMM06] A. Hinze, P. Malik, R. Malik. Interaction design for a mobile context-aware system
using discrete event modelling. In Estivill-Castro and Dobbie (eds.), ACSC.
CRPIT 48, pp. 257–266. Australian Computer Society, 2006.
[HVB09] A. Hinze, A. Voisard, G. Buchanan. Tip: Personalizing Information Delivery in a
Tourist Information System. Journal of IT & Tourism 11(3):247–264, 2009.
[PIM] PIMed. An editor for presentation models and presentation interaction models.
Available from: http://www.cs.waikato.ac.nz/Research/fm/PIMed.html.
[Ree05] G. Reeve. A Refinement Theory for mCharts. PhD thesis, The University of
Waikato, 2005.

ref.3-7

Modelling user manuals of modal medical devices and learning from the experience
Bowen, J., and Reeves, S. Formal models for informal GUI designs. In 1st International Workshop on Formal Methods for Interactive Systems, Macau SAR China, 31 October 2006, vol. 183, Electronic Notes in Theoretical Computer Science, Elsevier (2006), 57--72. Google ScholarDigital Library
Caesarea Medical Electronics. Niki T34 syringe pump instruction manual. ref. 100-090SS Edition (2008).Google Scholar
Campos, J., and Harrison, M. Modelling and analysing the interactive behaviour of an infusion pump. ECEASST 11 (2001).Google Scholar
Derrick, J., and Boiten, E. Refinement in Z and Object-Z: Foundations and Advanced Applications. Formal Approaches to Computing and Information Technology. Springer, May 2001. Google ScholarDigital Library
Engineering and Physical Sciences Research Council. CHI+MED: Multidisciplinary computer-human interaction research for the design and safe use of interactive medical devices, epsrc reference: Ep/g059063/1, 2011.Google Scholar
Henson, M. C., Deutsch, M., and Reeves, S. Z Logic and Its Applications. Springer: Monographs in Theoretical Computer Science. An EATCS Series, 2008, 489--596.Google Scholar
ISO/IEC 13568. Information Technology - Z Formal Specification Notation - Syntax, Type System and Semantics, first ed. Prentice-Hall International series in computer science. ISO/IEC, 2002.Google Scholar
PIMed, http://sourceforge.net/projects/pims1/?source=directory.Google Scholar
ProB, http://www.stups.uni-dusseldorf.de/prob, 2012.Google Scholar
Reeve, G. A Refinement Theory for μCharts. PhD thesis, The University of Waikato, 2005.Google Scholar
Thimbleby, H., Blandford, A., Cauchi, A., Curzon, P., Eslambolchilar, P., Furniss, D., Gimblett, A., Huang, H., Lee, P., Li, Y., Masci, P., Oladimeji, P., Rjakomar, A., and Rukšėnas, R. Comparing actual practice and user manuals: A case study based on programmable infusion pumps. In Proceedings ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS): Engineering Interactive Computing Systems for Medicine and Health Care, ACM (2011), 59--64.Google Scholar
Thimbleby, H., and Ladkin, P. From logic to manuals again. IEE Proceedings - Software 144, 3 (1997), 185--192.Google Scholar
Woodcock, J., and Davies, J. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996. Google ScholarDigital Library

ref. 3-8

Design Patterns for Models of Interactive Systems

[1] E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns: Elements of Reusable Object-oriented Software. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 1995.
[2] P. Hudak, The Haskell School of Expression. Cambridge University Press, 2000.
[3] J. Bowen and S. Reeves, “Formal models for user interface design artefacts,” Innovations in Systems and Software Engineering, vol. 4, no. 2, pp. 125–141, 2008.
[4] ——, “UI-design driven model-based testing,” Innovations in Systems and Software Engineering, vol. 9, no. 3, pp. 201 – 215, 2013.
[5] I. Bayley and H. Zhu, “Formal specification of the variants and be- havioural features of design patterns,” Journal of Systems and Software, vol. 83, no. 2, pp. 209 – 221, 2010.
[6] “PIMed, http://sourceforge.net/projects/pims1/?source=directory.”
[7] “PVSio-web, https://github.com/thehogfather/pvsio-web.”
[8] “Design Patterns, http://en.wikipedia.org/wiki/design patterns.”
[9] J. Bowen and S. Reeves, “Modelling safety properties of interactive medical systems,” in Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, ser. EICS ’13. New York, NY, USA: ACM, 2013, pp. 91–100.

[10] Engineering and Physical Sciences Research Council, “CHI+MED: 162.
Multidisciplinary computer-human interaction research for the design and safe use of interactive medical devices, EPSRC reference: EP/G059063/1,” 2011. [Online]. Available: http://gow.epsrc.ac.uk/ ViewGrant.aspx?GrantRef=EP/G059063/1
[11] P. Masci, Y. Zhang, P. L. Jones, P. Oladimeji, E. D’Urso, C. Bernarde- schi, P. Curzon, and H. Thimbleby, “Combining pvsio with stateflow,” in NASA Formal Methods - 6th International Symposium, NFM 2014, Houston,TX, USA, April 29 - May 1, 2014. Proceedings, 2014, pp. 209– 214.
[12] P. Masci, Y. Zhang, P. L. Jones, P. Curzon, and H. W. Thimbleby, “Formal verification of medical device user interfaces using PVS,” in Fundamental Approaches to Software Engineering - 17th International Conference, FASE 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, 2014, pp. 200–214.
[13] J. Bowen and S. Reeves, “A simplified Z semantics for presentation interaction models,” in FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, 2014, pp. 148–
[14] “PVS, http://pvs.csl.sri.com.”
[15] “Agda, http://en.wikipedia.org/wiki/agda (programming language).”
[16] “Idris, http://www.idris-lang.org.”
[17] “PVSio, http://shemesh.larc.nasa.gov/people/cam/pvsio/.”
[18] G. Reeve, “A refinement theory for μcharts,” Ph.D. dissertation, The University of Waikato, 2005.
[19] ISO/IEC 13568, Information Technology—Z Formal Specification Notation—Syntax, Type System and Semantics, 1st ed., ser. Prentice- Hall International series in computer science. ISO/IEC, 2002.
[20] S. Stepney, F. Polack, and I. Toyn, “Patterns to guide practical refactor- ing: examples targetting promotion in z,” in ZB2003: Third International Conference of B and Z Users, Turku, Finland, ser. LNCS, D. Bert, J. P. Bowen, S. King, and M. Walden, Eds., vol. 2651. Springer, 2003.
[21] H. Zhu and I. Bayley, “An algebra of design patterns,” ACM Trans. Softw. Eng. Methodol., vol. 22, no. 3, pp. 23:1–23:35, Jul. 2013. [Online]. Available: http://doi.acm.org/10.1145/2491509.2491517

ref. on 3-9

Formal Models for Informal GUI Designs

[1] ISO/IEC 13568. Information Technology—Z Formal Specification Notation—Syntax, Type System and
Semantics. Prentice-Hall International series in computer science. ISO/IEC, first edition, 2002.
[2] Judy Bowen. Formal specification of user interface design guidelines. Masters thesis, Computer Science
Department, University of Waikato, 2005.
[3] Judy Bowen and Steve Reeves. Formal refinement of informal GUI design artefacts. In Proceedings of
the Australian Software Engineering Conference (ASWEC’06), pages 221–230. IEEE, 2006.
[4] G. Calvary, J. Coutaz, and D. Thevenin. Supporting context changes for plastic user interfaces: A
process and a mechanism. In A. Blandford, J. Vanderdonckt, and P. Gray, editors, Joint Proceedings
of HCI’2001 and IHM’2001, pages 349–363. Springer-Verlag, 2001.
[5] Gaelle Calvary, Joelle Coutaz, and David Thevenin. A unifying reference framework for the development of plastic user interfaces. In EHCI ’01: Proceedings of the 8th IFIP International Conference on Engineering for Human-Computer Interaction, pages 173–192, London, UK, 2001. Springer-Verlag. [6] Francesco Correani, Giulio Mori, and Fabio Paterno. Supporting flexible development of multi-device
interfaces. In EHCI/DS-VIS, pages 346–362, 2004.
[7] Antony Courtney. Functionally modeled user interfaces. In Interactive Systems. Design, Specification,
and Verification. 10th International Workshop DSV-IS 2003, Funchal, Madeira Island (Portugal) J.
Joaquim, N. Jardim Nunes, J. Falcao e Cunha (ed.), pages 107–123. Springer Verlag Lecture Notes in
Computer Science LNCS, 2003.

[8] Adrien Coyette, St´ephane Faulkner, Manuel Kolp, Quentin Limbourg, and Jean Vanderdonckt.
Sketchixml: towards a multi-agent design tool for sketching user interfaces based on usixml. In
TAMODIA ’04: Proceedings of the 3rd annual conference on Task models and diagrams, pages 75–
82, New York, NY, USA, 2004. ACM Press.
[9] John Derrick and Eerke Boiten. Refinement in Z and Object-Z: Foundations and Advanced
Applications. Formal Approaches to Computing and Information Technology. Springer, May 2001.
[10] David J. Duke, Bob Fields, and Michael D. Harrison. A case study in the specification and analysis of
design alternatives for a user interface. Formal Asp. Comput., 11(2):107–131, 1999.
[11] D. F. Gieskens and J. D. Foley. Controlling user interface objects through pre and postconditions. In
Proc. of CHI-92, pages 189–194, Monterey, CA, 1992.
[12] A. Hussey, I. MacColl, and D. Carrington. Assessing usability from formal user-interface designs.
Technical Report TR00-15, Software Verification Research Centre, The University of Queensland, 2000.
[13] IFM05. http://www.win.tue.nl/ifm/, 2005.
[14] J. Landay. Silk: Sketching interfaces like krazy. In Human Factors in Computing Systems (Conference
Companion), ACM CHI ’96, Vancouver, Canada, April 13–18, pages 398 – 399, 1996.
[15] A. Paiva, N. Tillmann, J. Faria, and R. Vidal. Modeling and testing hierarchical GUIs. In D. Beauquier,
E. Borger, and A. Slissenko, editors, ASM05, pages 329–344. Universite de Paris, 2005.
[16] David L. Parnas. On the use of transition diagrams in the design of a user interface for an interactive
computer system. In Proceedings of the 1969 24th national conference, pages 379–385. ACM Press,
1969.
[17] F. M. Paterno, M.S. Sciacchitano, and J. Lowgren. A user interface evaluation mapping physical user actions to task-driven formal specification. In Design, Specification and Verification of Interactive Systems, pages 155—173. Springer Verlag, 1995. [18] Fabio Paterno. Task models in interactive software systems. Handbook of Software Engineering and
Knowledge Engineering, 2001.
[19] Fabio Patern`o. Towards a UML for interactive systems. In EHCI ’01: Proceedings of the 8th IFIP
International Conference on Engineering for Human-Computer Interaction, pages 7–18, London, UK,
2001. Springer-Verlag.
[20] G. E. Pfaff. User Interface Management Systems. Springer-Verlag New York, Inc., 1985.
[21] Beryl Plimmer and Mark Apperley. Computer-aided sketching to capture preliminary design. In
CRPIT ’02: Third Australasian conference on User interfaces, pages 9–12, Darlinghurst, Australia,
Australia, 2002. Australian Computer Society, Inc.
[22] Ben Shneiderman. Designing the User Interface: Strategies for Effective Human-Computer Interaction.
Addison Wesley Longman Inc, 3rd edition, 1998.
[23] Graeme Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.
[24] H. Thimbleby. Design of interactive systems. The Software Engineer’s Reference Book, 1990.
[25] Harold Thimbleby. User interface design with matrix algebra. ACM Trans. Comput.-Hum. Interact.,
11(2):181–236, 2004.
[26] NiklausWirth. Program development by stepwise refinement. Communications of the ACM, 14(4):221–
227, April 1971.
[27] J. Woodcock and J. Davies. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996.

ref 3-15

Reusing models and properties in the analysis of similar interactive devices

1. T. Amnell, G. Behrmann, J. Bengtsson, P.R. D’Argenio, A. David, A. Fehnker, T. Hune, B. Jeannet, K.G. Larsen, M.O. M ̈oller, P. Pettersson, C. Weise, and W. Yi. UP- PAAL - Now, Next, and Future. In F. Cassez, C. Jard, B. Rozoy, and M. Ryan, editors, Modelling and Verifica- tion of Parallel Processes, number 2067 in Lecture Notes in Computer Science Tutorial, pages 100–125. Springer– Verlag, 2001.
2. D. Arney, B. Kim, R. Jetley, P. Jones, I. Lee, A. Ray, O. Sokolsky, and Y. Zhang. Safety requirements for the generic patient controlled analgesia pump.
3. B. Braun Melsungen AG. B.Braun Infusomat Space User Manual. Technical report, B. Braun Melsungen AG, 34209 Melsungen, Germany, 2007.
4. L-A. Bligard and A-L. Osvalder. An analytical approach for predicting and identifying use error and usability problem. In A. Holzinger, editor, Proceedings of the 3rd Human-computer interaction and usability engineering of the Austrian computer society conference on HCI and usability for medicine and health care, number 4799 in Springer Lecture Notes in Computer Science, pages 427– 440. Springer-Verlag, 2007.
5. M. L. Bolton and E. J. Bass. Formally verifying human- automation interaction as part of a system model: limita- tions and tradeo↵s. Innovations in System and Software Engineering, 6(3):219–231, 2010.
6. M. L. Bolton, E. J. Bass, and R. I. Sininiceanu. Gen- erating phenotypical erroneous human behavior to eval- uate human-automation interaction using model check- ing. International Journal of Human-Computer Studies, 70:888–906, 2012.
7. M. L. Bolton, E.J. Bass, and R.I. Siminiceanu. Using formal verification to evaluate human-automation inter- action, a review. IEEE Transactions on Systems, Man, and Cybernetics, Part A: Systems and Humans, in press.
8. J. C. Campos. Minho HCI repository. http://hcispecs. di.uminho.pt, December 2012.
9. J. C. Campos and M. D. Harrison. Model checking in- teractor specifications. Automated Software Engineering, 8:275–310, 2001.
10. J. C. Campos and M. D. Harrison. Systematic analysis of control panel interfaces using formal tools. In N. Graham and P. Palanque, editors, Interactive systems: Design, Specification and Verification, DSVIS ’08, number 5136 in Springer Lecture Notes in Computer Science, pages 72–85. Springer-Verlag, 2008.
11. J. C. Campos and M. D. Harrison. Interaction engineer- ing using the IVY tool. In G. Calvary, T.C.N. Graham, and P. Gray, editors, Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Sys- tems, pages 35–44. ACM Press, 2009.
12. J. C. Campos and M.D. Harrison. Modelling and analysing the interactive behaviour of an infusion pump. Electronic Communications of the EASST, 5, 2011.
13. Jos ́e C. Campos and Michael D. Harrison. Formally Ver- ifying Interactive Systems: A Review. In M.D. Harrison and J.C. Torres, editors, Proceedings on the 4th Euro- graphics Workshop on Design, Specification and Verifi- cation of Interactive Systems (DSVIS), pages 119–134. Springer-Verlag, 1997.
14. Cardinal Health Inc. Alaris GP volumetric pump: direc- tions for use. Technical report, Cardinal Health, 1180 Rolle, Switzerland, 2006.
15. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An Open Source Tool for Symbolic Model Checking. In K. G. Larsen and E. Brinksma, editors, Computer-Aided Verification (CAV ’02), volume 2404 of Lecture Notes in Computer Science. Springer-Verlag, 2002.
16. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
17. L. de Moura. SAL: Tutorial. Technical report, SRI Inter- national, Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park, CA 94025, 2004.
18. A. Dix, J. Finlay, G. Abowd, and R. Beale. Human- Computer Interaction. Prentice Hall, 1993.
19. A. J. Dix. Formal Methods for Interactive Systems. Aca- demic Press, 1991.
20. G.Doherty,J.C.Campos,andM.D.Harrison.Resources for situated actions. In N. Graham and P. Palanque, edi- tors, Interactive systems: Design, Specification and Ver- ification, DSVIS ’08, volume 5136 of Springer Lecture Notes in Computer Science, pages 194–207. Springer- Verlag, 2008.
21. D. J. Duke and M. D. Harrison. Abstract interaction objects. Computer Graphics Forum, 12(3):25–36, 1993.
22. J. Fiadeiro, T. Maibaum, J. de Bakker, W. de Roever, and G. Rozenberg. Describing, structuring and imple- menting objects. In Foundations of Object-Oriented Lan- guages, number 489 in Springer Lecture Notes in Com- puter Science, pages 274–310. Springer-Verlag, 1991.
23. R. E. Fields. Analysis of erroneous actions in the de- sign of critical systems. PhD thesis, Department of Computer Science, University of York, Heslington, York, YO10 5DD, 2001.
24. US Food and Drug Administration. Infusion pump im- provement initiative. Technical report, Center for Devices and Radiological Health, April 2010.
25. M. Heymann and A. Degani. Formal analysis and auto- matic generation of user interfaces: Approach, methodol- ogy, and an algorithm. Human Factors: The Journal of the Human Factors and Ergonomics Society, 49(2):311– 330, 2007.
26. P. N. Johnson-Laird. Mental Models. Harvard University Press, 1983.
27. B. Kim, A. Ayoub, O. Sokolsky, I. Lee, P. Jones, Y. Zhang, and R. Jetley. Safety-assured development of the GPCA infusion pump software. In Proceedings of the ninth ACM international conference on Embedded soft- ware, EMSOFT ’11, pages 155–164, New York, NY, USA, 2011. ACM.
28. B. Kirwan and L. Ainsworth. A Guide to Task Analysis. Taylor and Francis, 1992.
29. R. Lane, N. A. Stanton, and D. Harrison. Applying hi- erarchical task analysis to medication administration er- rors. Applied Ergonomics, 37:669–679, 2006.
30. K. G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1–2):134–152, Oct 1997.
31. P. Masci, R. Rukˇse ̇nas, P. Oladimeji, A. Cauchi, A. Gim- blett, Y. Li, P. Curzon, and H. Thimbleby. On formalising interactive number entry on infusion pumps. ECEASST, 45, 2011.
32. J. Nielsen and R. Molich. Heuristic evaluation of user in- terfaces. In J. Chew and J. Whiteside, editors, ACM CHI Proceedings CHI ’90: Empowering People, pages 249– 256, 1990.
33. P. Oladimeji. Alaris simulation. http://cs.swan.ac.uk/ ~cspo/simulations, December 2012.
34. P. Oladimeji, H. Thimbleby, and A. Cox. Number entry and their e↵ects on error detection. In P. Campos et al., editors, Interact 2011, number 6949 in Springer Lecture Notes in Computer Science, pages 178–185. Springer- Verlag, 2011.
35. F. Patern`o and G. Faconti. On the Use of LOTOS to Describe Graphical Interaction. In A. Monk, D. Diaper, and M. D. Harrison, editors, People and Computers VII: HCI ’92 Conference, pages 155–174. BCS HCI Specialist Group, Cambridge University Press, 1992.
36. R. Ruksenas, J. Back, P. Curzon, and A. Blandford. Verification-guided modelling of salience and cognitive load. Formal Aspects of Computing, 21:541–569, 2009.
37. M. Ryan, J. Fiadeiro, and T. Maibaum. Sharing ac- tions and attributes in modal action logic. In The- oretical Aspects of Computer Software, volume 526 of Springer Lecture Notes in Computer Science, pages 569– 593. Springer-Verlag, 1991.
38. H. Thimbleby and P. Cairns. Reducing number entry errors: Solving a widespread, serious problem. Journal Royal Society Interface, 7(51):1429–1439, 2010.
39. H. Thimbleby and A. Gimblett. Dependable keyed data entry for interactive systems. ECEASST, 45, 2011.
40. H. Thimbleby. Interaction walkthrough: evaluation of
    safety critical interactive systems. In G. Doherty and A. Blandford, editors, Interactive Systems: Design, Spec- ification and Verification, number 4323 in Springer Lec- ture Notes in Computer Science, pages 52–66. Springer- Verlag, 2007.
41. H. Thimbleby. Press on: principles of interaction pro- gramming. MIT Press, 2007.
42. J. Zhang, T. R. Johnson, V. L. Patel, D. L. Paige, and T. Kuboseb. Using usability heuristics to evaluate pa- tient safety of medical devices. Journal of Biomedical Informatics, 36:23–30, 2003.

ref. 3-16

Modelling information resources and their salience in medical device design
[1] Altmann, E., and Trafton, J. Memory for goals: an activation-based model. Cognitive Science 26, 1 (2002), 39–83.
[2] Back, J., Cox, A., and Brumby, D. Choosing to interleave: human error and information access cost.
[3] Bolton, M. L., Bass, E. J., and Siminiceanu, R. I. Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking. International Journal of Human-Computer Studies 70 (2012), 888–906.
[4] Campos, J. C., Doherty, G., and Harrison, M. D. Analysing interactive devices based on information
resource constraints. International Journal of
Human-Computer Studies 72 (2014), 284–297.
[5] Campos, J. C., and Harrison, M. D. Interaction
engineering using the IVY tool. In Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, G. Calvary, T. Graham, and
P. Gray, Eds., ACM Press (2009), 35–44.
[6] Chi, E. H., Rosien, A., Supattanasiri, G., Williams, A., Royer, C., Chow, C., Robles, E., Dalal, B., Chen, J., and Cousins, S. The Bloodhound Project:
Automating discovery of web usability issues using the
TM
Infoscent simulator. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, CHI ’03, ACM (New York, NY, USA, 2003), 505–512.
[7] Cimatti, A., Roveri, M., Olivetti, E., Keighren, G., Pistore, M., Roveri, M., Semprini, S., and Tchaltsev, A. NuSMV 2.3 user manual. Tech. rep., ITC-IRST, Trento, Italy, 2007.
[8] Hutchins, E. Cognition in the Wild. MIT Press, 1994.
[9] John, B. E., Prevas, K., Salvucci, D. D., and
Koedinger, K. Predictive human performance modeling made easy. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, CHI ’04, ACM (New York, NY, USA, 2004), 455–462.
[10] Masci, P., Zhang, Y., Jones, P., Thimbleby, H., and Curzon, P. A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software. In 5th Workshop on Medical Cyber-Physical Systems,
V. Turau, M. Kwiatkowska, R. Mangharam, and
C. Weyer, Eds., vol. 36 of OpenAccess Series in Informatics (OASIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (Dagstuhl, Germany, 2014), 1–14.
[11] Monk, A., Curry, M., and Wright, P. Why industry doesn’t use the wonderful notations we researchers have given them to reason about their designs. In User-centred requirements for software engineering, D. Gilmore, R. Winder, and F. Detienne, Eds. Springer, 1991, 185–189.
[12] Mori, G., Paterno`, F., and Santoro, C. CTTE: Support for developing and analyzing task models for interactive system design. IEEE Transactions on Software Engineering 28, 8 (2002), 797–813.
[13] Nielsen, J. Heuristic Evaluation. In Usability Inspection Methods, J. Nielsen and R. Mack, Eds. John Wiley & Sons, Inc., 1994, ch. 2.
[14] Polson, P. G., Lewis, C., Rieman, J., and Wharton, C. Cognitive walkthroughs: a method for theory-based evaluation of user interfaces. International Journal of Man-Machine Studies 36, 5 (1992), 741–773.
[15] Ramos-Hernandez, D., Fleming, P., and Bass, J. A novel ob ject-oriented environment for distributed process control systems. Control Engineering Practice 13, 2 (2005), 213 – 230.
[16] Rukˇse ̇nas, R., Curzon, P., Blandford, A., and Back, J. Combining human error verification and timing analysis: a case study on an infusion pump. Formal Aspects of Computing (2013), 1–44.
[17] Rukˇse ̇nas, R., Curzon, P., and Harrison, M. D. Integrating formal predictions of interactive system behaviour with user evaluation. In Integrated Formal Methods, E. Johnsen and L. Petre, Eds., vol. 7940 of Springer Lecture Notes in Computer Science, Springer-Verlag (2013), 238–252.
[18] Suchman, L. Plans and Situated Actions: The Problem of Human Machine Interaction. Cambridge University Press, 1987.
[19] Teo, L.-H., John, B., and Blackmon, M. Cogtool-explorer: A model of goal-directed user exploration that considers information layout. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, CHI ’12, ACM (New York, NY, USA, 2012), 2479–2488.
[20] Wright, P., Fields, R., and Harrison, M. Analyzing human-computer interaction as distributed cognition: the resources model. Human-Computer Interaction 15, 1 (2000), 1–42.

ref. 3-17

Model checking interactor specifications

Abowd, G. D. , H.-M. Wang, and A. F. Monk: 1995, 'A formal technique for au-
tomated dialogue development'.
In: Proceedings of the First Symposium of
Designing Interactive Systems - DIS'95. ACM Press, pp. 219 226.
Atlee, J. M. and J. Gannon: 1993, 'State-Based Model Checking of Event-Driven
Systems Requirements'. IEEE Transactions on Software Engineering 19(1).
Bharadwaj, R. and C. L. Heitmeyer: 1999, 'Model Checking Complete Requirements
Specifications Using Abstractions'. Automated Software Engineering 6(1), 37 68.
Bodart, F. and J. Vanderdonckt (eds.): 1996, 'Design, Specification and Verification
of Interactive Systems '96', Springer Computer Science. Springer-Verlag/Wien.
Bolognesi, T. and E. Brinksma: 1987, 'Introduction to the ISO Specification
Language LOTOS'. Computer Networks and ISDN Systems 14(1), 25 59.
Bumbulis, P. , P. S. C. Alencar, D. D. Cowan, and C. J. P. Lucena: 1996, 'Validat-
ing Properties of Component-based Graphical User Interfaces'. In (Bodart and
Vanderdonckt, 1996), pp. 347 365.
Burch, J. R. , E. M. Clarke, and K. L. McMillan: 1990, 'Symbolic model checking:
1020 States and Beyond'. In: Proceedings of the Fifth Annual IEEE Symposium
on Logic In Computer Science. IEEE Computer Society Press, pp. 428—439.
Campos, J. C.: 1999, 'Automated Deduction and Usability Reasoning'. DPhil thesis,
Department of Computer Science, University of York.
Campos, J. C. and M. D. Harrison: 1997, 'Formally Verifying Interactive Systems:
A Review'. In (Harrison and Torres, 1997), pp. 109—124.
Campos, J. C. and M. D. Harrison: 1998, 'The role of verification in interactive
systems design'. In: P. Markopoulos and P. Johnson (eds.): Design, Specification and Verification of Interactive Systems '98, Springer Computer Science.
Springer-Verlag/Wien, pp. 155—170.
Campos, J. C. and M. D. Harrison: 1999, 'Using automated reasoning in the design of an audio-visual communication system'. In: D. J. Duke and A. Puerta
(eds.): Design, Specification and Verification of Interactive Systems '99, Springer
Computer Science. Springer-Verlag/Wien, pp. 167—188.
Chan, W., R. J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. D.
Reese: 1998, 'Model Checking Large Software Specifications'. IEEE Transactions
on Software Engineering 24(7), 498—520.
Cheaney, E.: 1991, 'ASRS Introduces...'. ASRS Direct,line (1)
http://asrs.arc.nasa.gov/directline.htm.
Clarke, E. and J. M. Wing: 1996, 'Tools and partial analysis'. ACM Computing
Surveys 28(4es), 116—es.
Clarke, E. M., E. A. Emerson, and A. P. Sistla: 1986, 'Automatic Verification of
Finite-State Concurrent Systems Using Temporal Logic Specifications'. ACM
Tmnsact,ions on Programming Languages and Systems 8(2), 244—263.
Clarke, E. M., O. Grumberg, and D. Peled: 1999, Model Checking. MIT Press.
de Roever, W.-P.: 1998, 'The Need for Compositional Proof Systems: A Survey'. In:
W.-P. de Roever, H. Langmaack, and A. Pnueli (eds.): Compositionality: The Significant Difference, Vol. 1536 of Lecture Notes in Computer Science. Springer,PP. 1-22.
Doherty, G., J. C. Campos, and M. D. Harrison: 2000, 'Representational Reasoning and Verification'. Formal Aspects of Computing 12(4), 260—277.
Duke, D., P. Barnard, J. May, and D. Duce: 1995, 'Systematic Development of the Human Interface'. In: Asia Pacific Software Engineering Conference. IEEE
Computer Society Press, pp. 313—321.
Duke, D. J. and M. D. Harrison: 1993, ' Abstract Interaction Objects'. Computer Graphics Forum 12(3), 25—36.
Dwyer, M. B. , V. Carr, and L. Hines: 1997, 'Model Checking Graphical User In terfaces Using Abstractions'. In: M. Jazayeri and H. Schauer (eds.): Software
Engineering — ESEC/FSE '97, No. 1301 in Lecture Notes in Computer Science. Springer, pp. 244—261.
Faconti, G. and F. Paternö: 1990, 'An Approach to the Formal Specification of the Components of an Interaction'. In: C. Vandoni and D. Duce (eds.): Eurographics '90. North-Holland, pp. 481—494.
Fiadeiro, J. and T. Maibaum: 1991, 'Temporal Reasoning over Deontic Specifica tions'. Journal of Logic and Computation 1 (3), 357—395.
Fields, B., N. Merriam, and A. Dearden: 1997, 'DMVIS: Design, Modelling and Validation of Interactive Systems'. In (Harrison and Torres, 1997), pp. 29—44.
Harrison, M., R. Fields, and P. C. Wright: 1996, 'The User Context and Formal Specification in Interactive System Design (invited paper)'. In: C. R. Roast and J. I. Siddiqi (eds.): Formal Aspects of the Human Computer Interface, electronic
Workshops in Computing. Springer-Verlag London.
Harrison, M. D. and J. C. Torres (eds.): 1997, 'Design, Specification and Verification of Interactive Systems '97', Springer Computer Science. Eurographics, Springer Verlag/Wien.
Heitmeyer, C., J. Kirby, and B. Labaw: 1998, 'Applying the SRC Requirements Method to a Weapons Control Panel: An Experience Report'. In: Proceedings of
the Second Workshop on Formal Methods in Software Practice (FIV"ISP '98). pp. 92-102.
Henzinger, T. A.: 1996, 'Some myths about formal verification'. ACM Computing Surveys 28(4es), 119—es.
Honeywell Inc.: 1988, 'SAS MD-80: Flight Management System Guide'. Honeywell Inc., Sperry Commercial Flight Systems Group, Air Transport Systems Division,
Leveson, N. G. and E. Palmer: 1997, 'Designing Automation to Reduce Operator Errors'. In: Proceedings of the IEEE Systems, Man, and Cybernetics Cordemnce.
Maims, J. A. et al.: 1992, 'Lite User Manual'. LOTOSPHERE consortium. Ref. Lo/WP2/N0034/V08.
McMillan, K. L.: 1993, Symbolic Model Checking. Kluwer Academic Publishers.
Monk, A. F. and M. B. Curry: 1994, 'Discount dialogue modelling with Action Simulator'. In: G. Cockton, S. W. Draper, and G. R. S. Weir (eds.): People and Computer IX - Proceedings of HCI'94. Cambridge University Press, pp. 327—338.
Nicola, R. D. , A. Fantechi, S. Gnesi, and G. Ristori: 1993, 'An action-based frame-work for verifying logical and behavioural properties of concurrent systems'.
Computer Networks and ISDN Systems 25(7), 761—778.
Palanque, P., F. Paternö, R. Bastide, and M. Mezzanote: 1996, 'Towards an inte-grated proposal for Interactive Systems design based on TLIM and IC(Y. In
(Bodart and Vanderdonckt, 1996), pp. 162—187.
Palmer, E.: 1995, Oops, it didn't arm." - A Case Study of Two Automation Surprises'. In: R. S. Jensen and L. A. Rakovan (eds.): Proceedings of the Eighth
International Symposium on Aviation Psychology. Columbus, Ohio, pp. 227—232.
Paternö, F. and M. Mezzanotte: 1995, 'Formal Analysis of User and System In teractions in the CERD Case Study'. Technical Report SN'I/WP48, Amodeus Project
Paternö, F. D.: 1995, 'A Method for Formal Specification and Verification of Inter active Systems'. Ph.D. thesis, Department of Computer Science, University of York.
Rushby, J.: 1999, 'Using Model Checking to Help Discover Mode Confusions and Other Automation Surprises'. In: (Pre-) Proceedings of the Workshop on Human Error, Sefety, and System Development (HESSD) 1999. Liöge, Belgium.
Ryan, M., J. Fiadeiro, and T. Maibaum: 1991, 'Sharing Actions and Attributes in Modal Action Logic'. In: T. Ito and A. R. Meyer (eds.): Theoretical Aspects of
Computer Software, Vol. 526 of Lecture Notes in Computer Science. Springer Verlag, pp. 569—593.
Sreemani, T. and J. M. Atlee: 1996, 'Feasibility of Model Checking Software Re-quirements: A Case Study'. In: Proceedings of the 11th Annual Conference on
Computer Assurance (COMPASS '96). pp. 77—88.
Stallman, R.: 1998, GNU Emacs Manual. Free Software Foundation, 13th edition.
Wall, L., T. Christiansen, and R. L. Schwartz: 1996, Programming Perl. O'Reilly
Associates, Inc., 2nd edition.
Woods, D. D., L. J. Johannesen, R. I. Cook, and N. B. Sartor: 1994, 'Behind Human Error: Cognitive Systems, Computers, and Hindsight'. State-of-the-Art Report SOAR 94-01. CSERIAC

ref. 3-19

Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example

1. Event-B and the Rodin Platform. http://www.event- b.org/.
2. The Generic Patient Controlled Analgesia Pump Hazard Analysis and Safety Requirements. http://rtg.cis.upenn.edu/gip.php3.
3. Medical Devices and the Public’s Health: The FDA 510(k) Clearance Process at 35 Years. Institute of Medicine, 2011.
4. B-Braun Melsungen AG. Perfusor Space and Accessory: Instruction for Use.
5. Bowen, J., and Reeves, S. Refinement for user interface designs. Formal Aspects of Computing 21, 6 (2009).
6. Degani, A. Taming HAL: Designing Interfaces Beyond 2001. Palgrave Macmillan, 2004.
7. Harrison, M., Campos, J., and Masci, P. Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering (2013), 1–17.
8. Kelly, T. Arguing safety – a systematic approach to managing safety cases. PhD thesis, Department of Computer Science, University of York, 1998.
9. Kim, B., Ayoub, A., Sokolsky, O., Lee, I., Jones, P., Zhang, Y., and Jetley, R. Safety-assured development of the GPCA infusion pump software. In Proceedings of the ninth ACM international conference on Embedded software, EMSOFT ’11, ACM (New York, NY, USA, 2011), 155–164.
10. Liu, G., Fukuda, T., Lee, C., Chen, V., Zheng, Q., and Kamae, I. Evidence-Based Decision-Making on Medical Technologies in China, Japan, and Singapore. Value in Health 12, Supplement 3, 0 (2009), S12–S17.
11. Masci, P., Ruksˇe ̇nas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., and Thimbleby, H. On formalising interactive number entry on infusion pumps. ECEASST 45 (2011).
12. Masci, P., Ruksˇe ̇nas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., and Thimbleby, H. The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. Innovations in Systems and Software Engineering (2013), 1–21.
13. Nielsen, J., and Molich, R. Heuristic evaluation of user interfaces. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, CHI ’90, ACM (New York, NY, USA, 1990), 249–256.
14. Owre, S., Rajan, S., Rushby, J., Shankar, N., and Srivas, M. PVS: Combining Specification, Proof Checking, and Model Checking. In Computer-Aided Verification, CAV
    ’96, no. 1102 in Lecture Notes in Computer Science, Springer-Verlag (1996), 411–414.
15. Owre, S., and Shankar, N. Theory Interpretations in PVS. Tech. Rep. SRI-CSL-01-01, Computer Science Laboratory, SRI International, Menlo Park, CA, 2001.
16. Rezazadeh, A., Evans, N., and Butler, M. Redevelopment of an Industrial Case Study Using Event-B and Rodin. In BCS-FACS Meeting - Formal Methods In Industry (December 2007).
17. Ryan, M., Fiadeiro, J., and Maibaum, T. Sharing actions and attributes in modal action logic. In Proceedings of the International Conference on Theoretical Aspects of Computer Software, TACS ’91, Springer-Verlag (London, UK, UK, 1991), 569–593.
18. Schoonmaker, M. The U.S. Approval Process for Medical Devices: Legislative Issues and Comparison with the Drug Model, March 2005. CSR Report for Congress.
19. Sorrel, S. Medical device development: U.S. and EU differences. Applied Clinical Trials Online (August 2006).
20. Thimbleby, H. Interaction walkthrough: evaluation of safety critical interactive systems. In Proceedings of the 13th international conference on Interactive systems: Design, specification, and verification, DSVIS’06, Springer-Verlag (Berlin, Heidelberg, 2007), 52–66.
21. Thimbleby, H. Press On: Principles of Interaction Programming. Mit Press, 2010.
22. Thimbleby, H., and Gimblett, A. User interface model discovery: Towards a generic approach. In Proceedings ACM SIGCHI Symposium on Engineering Interactive Computing Systems — EICS 2010, G. Doherty,
    J. Nichols, and M. D. Harrison, Eds., ACM (2010), 145–154.
23. US Food and Drug Administration. General Controls for Medical Devices, 2009.
24. US Food and Drug Administration. Learn if a Medical Device Has Been Cleared by FDA for Marketing, 2009.
25. US Food and Drug Administration. Premarket Notification (510k), 2009.
26. US Food and Drug Administration. Total Product Life Cycle: Infusion Pump - Premarket Notification [510(k)] Submissions - Draft Guidance, April 2010.
27. US Food and Drug Administration. FDA and Industry Actions on Premarket Approval Applications (PMAs): Effect on FDA Review Clock and Goals, October 2012.
28. Vadera, S. and Meziane, F. From English to formal specifications. The Computer Journal 37, 9 (1994).
29. Zuckerman, D., Brown, P., and Nissen, S. Medical device recalls and the FDA approval process. Archives of Internal Medicine 171, 11 (2011), 1006–1011.

ref.3-20

Using PVSio-web and SAPERE
[1] Developing pervasive multi-agent systems with
nature-inspired coordination. Pervasive and Mobile
Computing, 17, Part B:236 { 252, 2015. 10 years of
Pervasive Computing' In Honor of Chatschik
Bisdikian.
[2] Cardinal Health Inc. Alaris GP volumetric pump:
directions for use, 2006.
[3] F. L. De Angelis, J. L. Fernandez-Marquez, and
G. Di Marzo Serugendo. Self-composition of services
in pervasive systems: A chemical-inspired approach.
In Agent and Multi-Agent Systems: Technologies and
Applications, pages 37{46. Springer International
Publishing, 2014.
[4] J. M. Goldman. Medical Devices and Medical
Systems-Essential safety requirements for 5 equipment
comprising the patient-centric integrated clinical
environment 6 (ICE)-Part 1: General requirements
and conceptual model 7. ASTM International, 2008.
[5] M. D. Harrison, P. Masci, J. C. Campos, and
P. Curzon. Demonstrating that medical devices satisfy
user related safety requirements. In 4th International
Symposium on Foundations of Healthcare Information
Engineering and Systems (FHIES2014), 2014.
[6] A. King, D. Arney, I. Lee, O. Sokolsky, J. Hatcli, and
S. Procter. Prototyping closed loop physiologic control
with the medical device coordination framework. In
Proceedings of the 2010 ICSE Workshop on Software
Engineering in Health Care, pages 1{11. ACM, 2010.
[7] A. King, S. Procter, D. Andresen, J. Hatcli,
S. Warren, W. Spees, R. Jetley, P. Jones, and
S. Weininger. An open test bed for medical device
integration and coordination. In Software
Engineering-Companion Volume, 2009.
ICSE-Companion 2009. 31st International Conference
on, pages 141{151. IEEE, 2009.
[8] B. Larson, J. Hatcli, S. Procter, and P. Chalin.
Requirements specication for apps in medical
application platforms. In Proceedings of the 4th
International Workshop on Software Engineering in
Health Care, pages 26{32. IEEE Press, 2012.
[9] P. Masci, P. Oladimeji, P. Curzon, and H. Thimbleby.
Tool demo: Using PVSio-web to demonstrate software
issues in medical user interfaces. In 4th International
Symposium on Foundations of Healthcare Information
Engineering and Systems (FHIES2014), 2014.
[10] P. Masci, P. Oladimeji, P. Curzon, and H. Thimbleby.
PVSio-web 2.0: Joining PVS to Human-Computer
Interaction. In 27th International Conference on
Computer Aided Verication (CAV2015). Springer,
2015. Tool and application examples available at
http://www.pvsioweb.org.
[11] P. Masci, R. Ruks_enas, P. Oladimeji, A. Cauchi,
A. Gimblett, Y. Li, P. Curzon, and H. Thimbleby. The
benets of formalising design guidelines: A case study
on the predictability of drug infusion pumps.
Innovations in Systems and Software Engineering,
Springer-Verlag London, 2013.
[12] P. Masci, Y. Zhang, P. Jones, P. Curzon, and
H. Thimbleby. Formal Verication of Medical Device
User Interfaces Using PVS. In ETAPS/FASE2014,
17th International Conference on Fundamental
Approaches to Software Engineering, Berlin,
Heidelberg, 2014. Springer-Verlag.
[13] Masimo. Radical7 patient monitor: system overview.
http://www.masimo.com/rainbow/radical7.htm, 2015.
[14] C. Mu~noz. Rapid prototyping in PVS. Technical
Report NIA Report No. 2003-03,
NASA/CR-2003-212418, National Institute of
Aerospace, 2003.
[15] P. Oladimeji, P. Masci, P. Curzon, and H. Thimbleby.
PVSio-web: A tool for rapid prototyping device user
interfaces in PVS. In 5th International Workshop on
Formal Methods for Interactive Systems (FMIS2013),
2013.
[16] S. Owre, J. Rushby, and N. Shankar. PVS: A
Prototype Verication System. In 11th International
Conference on Automated Deduction (CADE), volume
607 of Lecture Notes in Articial Intelligence, pages
748{752, 1992.
[17] S. Procter and J. Hatcli. An
architecturally-integrated, systems-based hazard
analysis for medical applications. In Formal Methods
and Models for Codesign (MEMOCODE), 2014
Twelfth ACM/IEEE International Conference on,
pages 124{133. IEEE, 2014.
[18] S. Proctor, J. Hatcli, A. Fernando, and S. Weininger.
Using stpa to support risk management for
interoperable medical systems. 2015 STAMP
Workshop Presentations, 2015.
[19] S. Weininger, Y. J. Kim, J. Hatcli, V.-P. Ranganath,
and Robby. Integrated clinical environment device
model: Stakeholders and high level requirements. 2015.
[20] F. Zambonelli, A. Omicini, B. Anzengruber,
G. Castelli, F. L. DeAngelis, G. Di Marzo Serugendo,
S. Dobson, J. L. Fernandez-Marquez, A. Ferscha,
M. Mamei, S. Mariani, A. Molesini, S. Montagna,
J. Nieminen, D. Pianini, M. Risoldi, A. Rosi,
G. Stevenson, M. Viroli, and J. Ye. Developing
pervasive multi-agent systems with nature-inspired
coordination. Pervasive and Mobile Computing,
17:236{252, 2015. Special Issue \10 years of Pervasive
Computing" In Honor of Chatschik Bisdikian.
View publication

ref. 3-29

ABRAMS, M., PHANOURIOU, C., BATONGBACAL, A., WILLIAMS, S., AND SHUSTER, J. 1999. UIML: An
appliance-independent XML user interface language. In Proceedings of the 8th World Wide Web
Conference (WWW). Elseiver, 617–630.
BANDELLONI R., MORI, G., AND PATERNO’, F. 2005. Dynamic generation of migratory interfaces. In
Proceedings Mobile Human-Computer Interaction Conference. 83–90.
BLUMENDORF, M., LEHMANN, G., FEUDERSTACK, S., AND ALBRAYARK, S. 2008. Executable models for
human-computer interaction. In Proceedings of the XVth International Workshop on the Design,
Verification and Specification of Interactive Systems (DSVIS’08). 238–251.
CALVARY, G., COUTAZ, J., BOUILLON, L., FLORINS, M., LIMBOURG, Q., MARUCCI, L., PATERNO’, F., SANTORO,
C., SOUCHON, N., THEVENIN, D., AND VANDERDONCKT, J. 2002. The CAMELEON reference framework.
Deliverable 1.1, CAMELEON Project. http://www.w3.org/2005/Incubator/model-basedui/
wiki/Cameleon reference framework.
CHESTA, C., PATERNO, F., AND SANTORO, C. 2004. Methods and tools for designing and developing
usable multi-platform interactive applications. PsychNology J. 2, 1, 123–139.
CLERCKS, T., LUYTEN, K., AND CONIX, K. 2004. DynaMo-AID: A design process and a runtime architecture
for dynamic model-based user interface development. In Proceedings of the Working
Conference on Engineering for Human-Computer Interaction and International Workshop on Design
Specification and Verification of Interactive Systems (EHCI/DS-VIS). 77–95.
FOLEY, D. AND NOI SUKAVIRIYA, P. 1994. History, results, and bibliography of the user interface design
environment (UIDE), an early model-based system for user interface design and implementation.
In Proceedings of Design, Verification and Specification of Interactive Systems (DSVIS’94).
3–14.
JACOB, R., DELIGIANNIDIS, L., AND MORRISON, S. 1999. A software model and specification language
for non-WIMP user interface. ACM Trans. Comput.-Hum. Interact. 6, 1, 1–46.
JOHN, B. ANDKIERAS,D. 1996. TheGOMSfamily of analysis techniques: Comparison and contrast.
ACM Trans. Comput.-Hum. Interact. 3, 4, 320–351.
JOHNSON, P., WILSON, S., MARKOPOULOS, P., AND PYCOCK, J. 1993. ADEPT: Advanced design environment
for prototyping with task models. In Proceedings of the International Conference on
Human Computer Interaction and ACM Conference on Human Aspects on Computer Systems
(INTERCHI). 56.
HELMS, J. AND ABRAMS, M. 2008. Retrospective on UI description languages based on eight years’
experience with the user interface markup language (UIML). Int. J. Web Engin. Technol. 4, 2,
138–162.
LIN, J. AND LANDAY, J. 2008. Employing patterns and layers for early-stage design and prototyping
of cross-device user interfaces. In Proceedings of the 26th Annual SIGCHI Conference on Human
Factors in Computing Systems (CHI). 1313–1322.
MESKENS, J., VERMEULEN, J., LUYTEN, K., AND CONINX, K. 2008. Gummy for multi-device user interface
designs: Shape me, multiply me, fix me, use me. In Proceedings of the International Working
Conference on Advanced Visual Interfaces (AVI’08). 233–240.
LIMBOURG, Q., VANDERDONCKT, J., MICHOTTE, B., BOUILLON, L., AND L´OPEZ-JAQUERO, V. 2004.
USIXML: A language supporting multi-path development of user interfaces. In Proceedings
of the Working Conference on Engineering for Human-Computer Interaction and International
Workshop on Design Specification and Verification of Interactive Systems (EHCI/DS-VIS).
200–220.
MORI, G., PATERNO’, F., AND SANTORO, C. 2004. Design and development of multidevice user interfaces
through multiple logical descriptions. IEEE Trans. Softw. Engin. 30, 8, 507–520.
MYERS, B., HUDSON, S., AND PAUSCH, R. 2000. Past, present, future of user interface tools. ACM
Trans. Comput.-Hum. Interact. 7, 1, 3–28.
ACM Transactions on Computer-Human Interaction, Vol. 16, No. 4, Article 19, Publication date: November 2009.
19:30 • F. Paterno’ et al.
PATERNO’, F. 1999. Model-Based Design and Evaluation of Interactive Applications. Springer.
PATERNO’, F., SANTORO, C., M¨ANTYJ¨ARVI, J., MORI, G., AND SANSONE, S. 2008. Authoring pervasive
multimodal user interfaces. Int. J. Web Engin. Technol. 4, 2, 235–261.
PATERNO’, F., SANTORO, C., AND SCORCIA, A. 2008. Automatically adapting Web sites for mobile
access through logical descriptions and dynamic analysis of interaction resources. In Proceedings
of the Working Conference on Advanced Visual Interfaces (AVI). 260–267.
SALBER,D., ANIND, D., AND ABOWD,G. 1999. The context toolkit: Aiding the development of contextenabled
applications. In Proceedings of the SIGCHI Conference on Human Factors in Computing
Systems. 434–441.
SHAER, O., LELAND, N., CALVILLO-GAMEZ, E. H., AND JACOB, R. J. K. 2004. The TAC paradigm:
Specifying tangible user interfaces, Personal Ubiq. Comput. 8, 5, 359–369.
SOTTET, J., CALVARY, G., COUTAZ, J., AND FAVRE, J. 2007. A model-driven engineering approach for
the usability of plastic user interfaces. In Proceedings of the Working Conference on Engineering
Interactive Systems. 140–157.
VAN DERVEER,G., LENTING, B., ANDBERGEVOET,B. 1996. GTA: Groupware task analysis—Modelling
complexity. Acta Psychologica 91, 297–322.

related document

Safety and Security Rules for C
https://www.nccgroup.com/us/about-us/newsroom-and-events/blog/2018/july/safety-and-security-rules-for-C/

自己参照self reference

ソフトウェアFMEAを体系的に実施する出発点としてのMISRA-C株式会社ヴィッツ森川聡久株式会社ヴィッツ中野泰伸名古屋市工業研究所小川清

Misra cpp, cert cpp 2016 and RTL design style guide with HAZOP
https://www.slideshare.net/kaizenjapan/misra-cpp-cert-cpp-2016-with-rtl-design-style-guide

自己参照self reference＠qiita

MISRA C まとめ #include
https://qiita.com/kaizen_nagoya/items/f1a79a7cbd281607c7c9

C言語の#define文マクロをC++のTemplateか何かにする方法
https://qiita.com/kaizen_nagoya/items/20c3f5964cef1da037cb

C言語/C++に対する誤解、曲解、無理解、爽快。https://qiita.com/kaizen_nagoya/items/3f3992c9722c1cee2e3a

＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞

document history

ver. 0.01 初稿 20200811
ver. 0.02 add URL and its references 20200812
ver. 0.03 add references. 20200814
ver. 0.04 誤植訂正 20200816
ver. 0.05 補正 20220905