Search For:

Displaying 1-10 out of 10 total
Heterogeneous Aviation Safety Cases: Integrating the Formal and the Non-formal
Found in: 2012 17th International Conference on Engineering of Complex Computer Systems (ICECCS)
By Ewen Denney,Ganesh Pai,Josef Pohl
Issue Date:July 2012
pp. 199-208
We describe a method for the automatic assembly of aviation safety cases by combining auto-generated argument fragments derived from the application of a formal method to software, with manually created argument fragments derived from system safety analysi...
Perspectives on software safety case development for unmanned aircraft
Found in: 2012 42nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)
By Ewen Denney,Ganesh Pai,Ibrahim Habli
Issue Date:June 2012
pp. 1-8
We describe our experience with the ongoing development of a safety case for an unmanned aircraft system (UAS), emphasizing autopilot software safety assurance. Our approach combines formal and non-formal reasoning, yielding a semi-automatically assembled ...
Towards Measurement of Confidence in Safety Cases
Found in: Empirical Software Engineering and Measurement, International Symposium on
By Ewen Denney,Ganesh Pai,Ibrahim Habli
Issue Date:September 2011
pp. 380-383
Safety cases capture a structured argument linking claims about the safety of a system to the evidence justifying those claims. However, arguments in safety cases tend to be predominantly qualitative. Partly, this is attributed to the lack of sufficient de...
A Verification-Driven Approach to Traceability and Documentation for Auto-Generated Mathematical Software
Found in: Automated Software Engineering, International Conference on
By Ewen Denney, Bernd Fischer
Issue Date:November 2009
pp. 560-564
Automated code generators are increasingly used in safety-critical applications, but since they are typically not qualified, the generated code must still be fully tested, reviewed, and certified. For mathematical and engineering software this requires rev...
Generating Code Review Documentation for Auto-Generated Mission-Critical Software
Found in: Space Mission Challenges for Information Technology, IEEE International Conference on
By Ewen Denney, Bernd Fischer
Issue Date:July 2009
pp. 394-401
Model-based design and automated code generation are increasingly used at NASA to produce actual flight code, particularly in the Guidance, Navigation, and Control domain. However, since code generators are typically not qualified, there is no guarantee th...
Annotation Inference for Safety Certification of Automatically Generated Code (Extended Abstract)
Found in: Automated Software Engineering, International Conference on
By Ewen Denney, Bernd Fischer
Issue Date:September 2006
pp. 265-268
<p>Automated code generation is an enabling technology for model-based software development and promises many benefits, including higher quality and reduced turn-around times. However, the key to realizing these benefits is generator correctness: not...
Adding Assurance to Automatically Generated Code
Found in: High-Assurance Systems Engineering, IEEE International Symposium on
By Ewen Denney, Bernd Fischer, Johann Schumann
Issue Date:March 2004
pp. 297-299
Code to estimate position and attitude of a spacecraft or aircraft belongs to the most safety-critical parts of flight software. The complex underlying mathematics and abundance of design details make it error-prone and reliable implementations costly. Aut...
The Synthesis of a Java Card Tokenization Algorithm
Found in: Automated Software Engineering, International Conference on
By Ewen Denney
Issue Date:November 2001
pp. 43
We describe the development of a Java bytecode optimisation algorithm by the methodology of program extraction. We develop the algorithm as a collection of proofs and definitions in the Coq proof assistant, and then use Coq?s extraction mechanism to automa...
Generating customized verifiers for automatically generated code
Found in: Proceedings of the 7th international conference on Generative programming and component engineering (GPCE '08)
By Bernd Fischer, Ewen Denney
Issue Date:October 2008
pp. 1-8
Program verification using Hoare-style techniques requires many logical annotations. We have previously developed a generic annotation inference algorithm that weaves in all annotations required to certify safety properties for automatically generated code...
Software certificate management (SoftCeMent'05)
Found in: Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering (ASE '05)
By Bernd Fischer, Dieter Hutter, Ewen Denney, Mark Jones
Issue Date:November 2005
pp. 463-463
The goal of this workshop is to explore new technologies, underlying principles, and general methodologies for supporting software certificate management. Software certification demonstrates the reliability, safety, or security of software systems in such ...