Over the past few decades, advanced methods have been developed for the analysis of digital systems using mathematical reasoning, i.e., formal logic. These methods are supported by sophisticated software tools that can be used to perform analysis far beyond what is practically achievable using “paper and pencil” analysis. In December 2011, RTCA published RTCA DO 178C along with a set of technical supplements including RTCA DO 333 which provides guidance on the use of formal methods towards the certification of airborne software. Such methods have the potential to reduce the cost of verification by using formal analysis instead of conventional test-based methods to produce a portion of the verification evidence required for certification. Formal methods can also be used to find problems earlier in the development process – for example, while the requirements are being developed rather than during system integration when the cost of re-working the requirements and design is much higher.
CSL is doing advanced R&D projects that aim to improve the client’s capability to develop critical systems. Current R&D initiatives include the use of formal methods in accordance with RTCA DO 333 (Formal Methods Supplement to DO-178C and DO-278A).
Some of the services CSL offers:
- Model checking
- Formal specification
- Automated reasoning