Introduction

Software was introduced in Aircraft industry in 70’s. Companies found it was much easier and less costly to replace hardware components with software that could copy the same functionality. So the testing became more challenging because it involved now both the hardware as well as the software components. The Radio Technical Commission for Aeronautics and European organization of civil aviation merged their ideas to produce common certification criteria that resulted in the creation of DO-178. Among the various objectives of RTCA some of them are to ensure the safety and reliability of the airborne systems, developing guidelines for use by a regulatory authority, etc. In 1985, the original document was updated and revised – leading to DO-178A and ED-12A. In 1989 RTCA and EUROCEA began the next revision which had a requirement based testing instead of model based testing. The final document of DO-178B was released in 1992.After 15 years of use of DO178B a committee was set up to make new standards and it was known as DO-178C. This essay discusses on industry standard formal verification procedures in Safety Critical Application based on RTCA-DO 178C. The rest of the essay discusses the difference between DO-178B and DO-178C from formal methods point of view, verification activities mandated by DO-178C, functional contracts in compliance requirements, Air bus example of formal verification of functional properties, Dassault-Aviation example of formal verification of robustness and at end this essay gives the importance of formal verification procedures in ensuring quality of safety critical systems.

Differences between DO-178B and DO-178C

According to Formal methods point of view, DO178C had the model based development and verification supplement which applied to both the hardware and software architectures. Formal Methods Supplement of DO-178C and DO-278A identifies the additions, modifications and substitutions to DO-178C and DO-278A objectives when formal methods are used as part of a software lifecycle. DO-178C removes explicit reference to the use of formal methods as an alternative method to satisfy DO-178C objectives, but instead cites the use of assurance cases to provide adequate confidence and evidence that a product or process satisfies its requirements. DO-178C defines an assurance case as a technique in which arguments are explicitly given to link the evidence to the claims of compliance with the system safety objectives. Software tool qualification which supplements the development tool and verification tool which are replaced by three qualification criteria which determine the applicable Tool Qualification Level (TQL) is removed in DO-178C, but it is provided in a domain-independent, external document. Some of the differences apart from the formal methods point of view are like known issues regarding the errors and inconsistencies in DO178B were addressed, the Annexure A of DO178C contains each activities and their objective, identification  and verification for correctness of Level A object code, some of the decision gaps were addressed in DO178C, modified coverage and decision coverage were changed to support masking and short circuit, Section 12 was impacted, since the planned supplements more completely address specific techniques and many more.

Verification activities mandated by DO178C

Some of the verification activities mandated by DO178C are as follows.DO332 of DO178C states that the test cases should ensure that the class constructors should properly initialize the state of their objects. In cases where inheritance with method overriding and dynamic dispatch are used, verification activities should be done to ensure that all type substitutions are safe and that each class pass the same verification testing as their parent types. It also stresses to verify the dynamic memory allocation and verification activities must show that the dynamic memory management is good to reference ambiguity, fragmentation starvation, de-allocation starvation, memory exhaustion, premature de-allocation, lost updates, stale references, and unbounded allocation or de-allocation times. It should be verified that there is sufficient memory to accommodate the maximum storage required. The memory must be verified to successfully allocate memory for every request as long as there is sufficient free memory. It also said to verify the parent class and child class, memory leaks, parameterized types, type conversions, exceptions etc. Annex D also discusses activities for verification of traceability, structural coverage, component-based development, memory management, and timing for object-oriented programs.

Function contracts in compliance requirements:

Mostly the verification in DO178 is based on both high level (HLR) and low level requirement (LLR) [20].For both the types the DO178 require compliance and robustness verification. Compliance requirement focus on programs intended nominal behaviour. .For formal verification of these requirements the requirements are expressed in a formal language .The high level requirement can be expressed as a temporal logic to check that the error state is never reached. The Java Pathfinder tool used at NASA and the Aorai plug-in of Frama-C implement this technique. LLR can also be expressed as a logic function contract where it consists of two Boolean expressions: a precondition to specify input constraints and a postcondition to specify output constraints. Contracts can be executed as runtime assertions, interpreted as logic formulas by analysis tools. Then, formal analyses can be used to check that the code implements these formal contracts. Formal analyses can help check for the absence of runtime errors like reading uninitialized data, accessing out of bound array elements, dereferencing null pointer, numeric overflows and so on.

Airbus example of formal verification of functional properties:

As per [20] in Airbus, unit proof was used to verify functional properties to test for parts testing. Unit proof is a process comprising three steps. An engineer expresses LLRs formally as dataflow constraints, and as preconditions and post conditions in first-order logic, during the development process’s detailed design activity. An engineer writes a module to implement the desired functionality .The C language is used for this purpose. An engineer gives the C module’s formal requirements and the module itself to a proof tool. This activity is performed for each C function of each C module. An engineer first defines the proof environment, and then the tool automatically generates the data and control flows from the C code. The engineer then verifies these flows against the data and control flows defined during the design phase. Next, the tool attempts to prove that the C code correctly implements the functional properties defined during the design phase. Finally, the engineer analyses the proof results. The theorem-proving tool is integrated into the standard process management tool, so that this proof process is entirely automated and supported during maintenance. Verification is done at the source level instead of the binary level; also the object code was verified to check the compilers authenticity. Within this development cycle, HLRs are expressed informally, so integration verification is done via testing, which includes verification of timing aspects and hardware related properties. Each requirement is expressed as a property, each property is formally proved exhaustively, and every assumption made for formal verification is verified. Completeness of the set of requirements is verified. A theorem-proving tool was used to verify that the formal contract defined in the design phase specifies behaviour for all possible inputs. Then manually the formal contracts were verified. The data flow verification was done. Except for unreachable code (which can’t be executed), all the executable code is formally verified against LLRs. Airbus had used formal verification to replace the low level testing activities like normal range and robustness testing.

Dassault-Aviation example of formal verification of robustness:

At Dassault- Aviation, formal verification techniques were used to replace robustness testing by applying it to flight control software. C source code is automatically generated which includes data flows and state diagrams. A set of assertions is used to be met in both normal and abnormal input condition on the C source code. The robustness assertions which have some properties are applied on the model and then it is propagated to generate C code. At software modelling level a set of design rule were used and a custom checker were used to verify them. Static analysers were used to mechanize the analysis through formal proof which used Frama-C platform with Frama C value analysis plugin and Frama –C’s WP plugin and a set of automated theorem provers [20]. During verification process, once the integrated flight control software is sufficiently stable, a static analysis expert, with help of a model expert, use to perform the  formal robustness verification .It took roughly a person’s month effort  to set up the Frama-C analysis script and to tune any manually added assertions. Then the model verifiers autonomously replay and update the analysis until some algorithmic change in the model requires re-verification. A manual peer reviews of the set of assertions and also ensures that robustness requirements are complete.

Importance of formal verification procedures in ensuring quality of safety critical systems:

While concluding it will be good to say the importance of formal verification in ensuring quality of safety critical systems. The use of formal techniques in the production of systems should be viewed as a means of delivering enhanced quality rather than establishing correctness. Formal methods can be used at different levels of

assurance for the software developed by such methods. At a basic level, they may simply be used for specification of the system to be designed. The development process itself may be informal, but benefits are still gained since many bugs can be removed by formalizing and discussing the system at an early stage. Proofs may be undertaken to confirm properties of the system that are required or assumed to be true. The next level of use is to apply formal methods to the development process, using a set of rules or a design calculus that allows stepwise refinement of the specification to an executable program like VDM. Checking the process by computer reduces the possibility of error, although it never eliminates it since the program that does the checking may itself be incorrect. Formal methods were developed as a branch of computer science in order to reason more scientifically about software. Formal methods increase the safety and decrease the cost and it also allows rigorous analysis. Such analyses can verify useful properties such as consistency, deadlock-freedom, satisfaction of high level requirements, or correctness of a proposed design. Capturing requirements as formal specifications is good as it provides a simple validation. Formalized requirements prevent misunderstandings that lead to error introduction. As development proceeds, compliance can be continually checked using a formal analysis to ensure that errors have not been introduced. A further advantage of using formal methods at the requirements level is the ability to derive or refine from these requirements the code itself, thus ensuring that no errors are introduced at this stage. Last but not the least formal methods reduces cost of a software ,since the cost of error to fix it in later stage of development is higher than the one caught at early stage so formal methods are used starting from the beginning of the development.

References

[1] Alicendra,C.et al.,”Formalization and Validation of Safety-Critical Requirements”,Creative Common Arts.

[2] Antti,J.,et al.,(1998)”Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools”,1998,Dagasthul,Germany.

[3] Brown,D.,et al.,(2010)”Guidance for Using Formal Methods in a Certification Context”,May 2010.

[4] Decision and Information Analysis, Goizueta Business School(2001),”Model Checking – A Rigorous and Efficient Tool for E-Commerce Internal Control and Assurance”,17 September 2001,W.Wang,et al.

[5] Department of Computing, Imperial College London (2003),”Model-based Verification of Web Service Compositions”,2003,F.Howard,et al.

[6] Department of Computing, University of Surrey, Guildford, UK (2007),”An Automatic Test Case Generation Framework for Web Services”,3 september 2007,Z.Yongyan,Z.Jiong,K.Paul.

[7] Georgia, M.K.,et al.(2009)”Model-driven development of composite context-aware web applications”,27 March 2009,Software and Service Engineering Laboratory, Technological Education Institute of Piraeus, Dept. of Electronic Computing Systems, Petrou Ralli & Thivon 250, 12244 Athens, Greece

[8] Hoyt, L.,(2012)”Transitioning to RTCA DO-178C/DO-278A:A Business Manager Brief”,August 2012,Foliage

[9] Huth,M.,Ryan,M.,(2004)”LOGIC IN COMPUTER SCIENCE”,Second Edition,2004,Cambridge University Press

[10] Jamal,B.et al.,(2013)”Symbolic model checking composite Web services using operational and control behaviors”,2013,Concordia University.

[11] Laurent,P.et al.,”DO-178C/ED-12C versus DO-178B/ED-12B Changes and Improvements”,September 2012,ACG Solutions.

[12] Maddireddy,S.R.,”The Impact of RTCA DO-178C on Software Development”,Cognizant

[13] Melissa,K.(2009)”A formal verification approach of conversations in composite web”,August 2009,Concordia University

[14] NASA Ames Research Center, Moffett Field, CA 94035, USA (2010),”Linear Temporal Logic Symbolic Model Checking”,29 June 2010,Y.R.Kristin.

[15] Raman,K.,et al.(2006)”Verification and Validation of Web Service Compositions “,27 June  2006,DIT, University of Trento, Italy.

[16]Roberto,C. et al.“NuSMV 2.5 Tutorial”, First Edition, FBK publisher

[17] School of Computing,University of Utah ,”Model Checking Web Services”,Shrigondekar,Amit.,De Silva,L.,Thulasinathan,A.

[18] Stephen A.J.,”Certification of Safety-Critical Software Under DO-178C and DO-278A”,NASA Ames Research Center, Moffett Field, CA, 94035

[19] Wlad,J.,(2012)”Architectural Trends in Avionics Systems: Multi-core and DO-178C”,April 2012,Aerospace and Defense FAA DER Systems and Software.

[20] Xian,F.(2004)”Formal Specification and Verification of Asynchronously Communicating Web Services”,September 2004,UNIVERSITY of CALIFORNIA.

[21]Yanick,M. et al.(2013) “Testing or Formal Verification: DO-178C Alternatives

and Industrial Experience”,2013,IEEE computer society

[22] Zoltan,T.H.(2007)”Model Checking – A Rigorous and Efficient Tool for Preventing E-business Failures”,August 2007,THE UNIVERSITY OF TEXAS AT AUSTIN

[23] 21st International Joint Conference on Artificial Intelligence (IJCAI)(2009),”Behavioral Description Based Web Service Composition Using Abstraction and refinement”,2009,H.Kil,et al.