Software certification demonstrates the reliability, safety, or security of software systems in such a way that it can be checked by an independent authority with minimal trust in the techniques and tools used in the certification process itself. It can build on existing validation and verification (V&V) techniques but introduces the notion of explicit software certificates, which contain all the information necessary for an independent assessment of the demonstrated properties. One such example is proof-carrying code (PCC) which is an important and distinctive approach to enhancing trust in programs. It provides a practical framework for independent assurance of program behaviour; especially where source code is not available, or the code author and user are unknown to each other.
The workshop will address theoretical foundations of logic-based software certification as well as practical examples and work on alternative application domains. Here "certificate" is construed broadly, to include not just mathematical derivations and proofs but also safety and assurance cases, or any formal evidence that supports the semantic analysis of programs: that is, evidence about an intrinsic property of code and its behaviour that can be independently checked by any user, intermediary, or third party. These guarantees mean that software certificates raise trust in the code itself, distinct from and complementary to any existing trust in the creator of the code, the process used to produce it, or its distributor.
In addition to the contributed talks, the workshop will feature two invited talks.
Formal methods can be applied to many of the development and verification activities required for civil avionics software. RTCA/DO-178B, Software Considerations in Airborne Systems and Equipment Certification, gives a brief description of using formal methods as an alternate method of compliance with the objectives of that standard.Despite this, the avionics industry at large has been hesitant to adopt formal methods, with few developers have actually used formal methods for certification credit.Why is this so, given the volume of evidence of the benefits of formal methods? This presentation will explore some of the challenges to using formal methods in a certification context and describe the effort by the Formal Methods Subgroup of RTCA SC-205/EUROCAE WG-71 to develop guidance to make the use of formal methods a recognized approach.
All papers should describe original work that has not been published elsewhere. Submissions will be fully reviewed and the symposium proceedings will appear as a NASA Conference Publication. Authors of selected papers will then be invited to submit extended versions to a special issue of the journal Higher Order and Symbolic Computation.
Additional material intended for the referees but not for publication in the final version may be placed in a clearly marked appendix that is not included in the page limit.
Papers should be submitted through the following link: http://www.easychair.org/conferences/?conf=pcc09
Proceedings will be made available in electronic format as a technical report. There will be a follow-up special issue of the Higher Order and Symbolic Computation on the topics of proof-carrying code and software certification (more details will be announced at the workshop).