The official website of the MISRA association https://www.misra.org.uk/ has many freely available resources about MISRA-C, some of which can be downloaded after registering on the MISRA Bulletin Board at https://www.misra.org.uk/forum/ (like the set of examples from MISRA-C:2012 document which includes the one-line description of all guidelines).
The following documents are available freely:
- MISRA Compliance 2016: Achieving compliance with MISRA coding guidelines, 2016, which explains the rationale and process for compliance, including a thorough discussions of acceptable deviations
- MISRA C:2012 - Amendment 1: Additional security guidelines for MISRA C:2012, 2016, which contains 14 additional guidelines focusing on security. This is a minor addition to MISRA-C, that we did not feel we needed to discuss further in this book.
The main MISRA-C:2012 document is available at a small cost from the MISRA webstore.
PRQA is the company at the origin of the first version of MISRA-C, and they have been very involved in every version since then. Their webpage http://www.prqa.com/coding-standards/misra/ contains many resources about MISRA-C: product datasheets, white papers, webinars, trainings.
PRQA Resources Library at http://info.prqa.com/resources-library?filter=white_paper has interesting feely available white papers on MISRA-C and the use of static analyzers:
- an introduction to MISRA-C:2012 at http://info.prqa.com/misra-c-2012-whitepaper-evaluation-lp
- The Myth of Perfect MISRA Compliance at http://info.prqa.com/myth-of-perfect-misra-compliance-evaluation-lp, providing background information on the use and limitations of static analyzers for checking MISRA-C compliance
ISO standardized in 2013 a set of 45 rules focused on security, available in the C Secure Coding Rules document. A draft is freely available at http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1624.pdf
MISRA association published in 2018 a document MISRA C:2012 - Addendum 2: Coverage of MISRA C:2012 against ISO/IEC TS 17961:2013 "C Secure" mapping ISO rules to MISRA-C:2012 guidelines, available freely from https://www.misra.org.uk/
The e-learning website https://learn.adacore.com/ contains a freely available interactive course on SPARK.
The SPARK User's Guide is available at http://docs.adacore.com/spark2014-docs/html/ug/
The SPARK Reference Manual is available at http://docs.adacore.com/spark2014-docs/html/lrm/
A student-oriented textbook on SPARK is Building High Integrity Applications with SPARK by McCormick and Chapin, published by Cambridge University Press. It is sold online by Amazon and many others.
For a historical account of the evolution of SPARK technology and its use in industry, see the article Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK by Chapman and Schanda, at http://proteancode.com/keynote.pdf
The website https://www.adacore.com/sparkpro is a portal for up-to-date information and resources on SPARK. AdaCore blog at https://blog.adacore.com/ frequently hosts posts on the latest evolutions of SPARK.
The document AdaCore Technologies for Cyber Security presents the usage of AdaCore's technology to prevent or mitigate the most common security vulnerabilities in software. See: https://www.adacore.com/books/adacore-tech-for-cyber-security
The document AdaCore Technologies for CENELEC EN 50128:2011 presents the usage of AdaCore's technology in conjunction with the CENELEC EN 50128:2011 standard. It describes in particular where the SPARK technology fits best and how it can best be used to meet various requirements of the standard. See: https://www.adacore.com/books/cenelec-en-50128-2011
The document AdaCore Technologies for DO-178C/ED-12C similarly presents the usage of AdaCore's technology in conjunction with the DO-178C/ED-12C standard, and describes in particular the use of SPARK in relation with the Formal Methods supplement DO-333/ED-216. See: https://www.adacore.com/books/do-178c-tech
About MISRA-C and SPARK¶
The blog post at https://blog.adacore.com/misra-c-2012-vs-spark-2014-the-subset-matching-game reviews the 27 undecidable rules in MISRA-C:2012 and describes how SPARK addresses them.
The white paper A Comparison of SPARK with MISRA C and Frama-C at https://www.adacore.com/papers/compare-spark-misra-c-frama-c compares SPARK to MISRA-C and to the formal verification tool Frama-C for C programs.