Static analysis is often complemented with dynamic analysis, including simulation-based testing or testing of the system of component under consideration. Analysis of software provides a means to understand software correctness and optimization.
The term “static analysis” covers a wide range of techniques that bring different levels of formality and mathematical rigour to the problem. Safety standards such as IEC 61508 and DO-178B identify a number of specific static analysis techniques ranging from independent code review to formal methods such as correctness proofs and model checking.
Adelard have extensive experience both in development and research of static and dynamic analysis techniques and in their application as part of safety justifications. We can select combinations of techniques to achieve the desired level of confidence in the reliability of a system, producing an analysis programme based on static analysis and device testing. This work often complements a development process assessment.
Some of our recent work for our clients include:
- applying model checkers (e.g., NuSMV, SPIN, SAL and Uppaal) to problems in software, hardware and requirements engineering
- using tools such as PolySpace, Safer C Toolset and QA C++ to support static integrity analysis
- formal correctness proofs and other types of advanced analysis using Frama-C
- simulation-based testing of smart devices using LDRA and VectorCast
- testing and developing testing specifications for smart devices, including temperature transmitters, pressure transmitters, boilers and alarms
We have active research projects pioneering static analysis and developing our own bespoke tools, some of which are available as open source software. We have a particular interest in taking techniques traditionally associated with the highest integrity classes (for example, formal correctness proofs) and finding innovative ways to make them cost-effective for systems with a more moderate safety claim.
Successful application of formal methods requires specialised and competent computer scientists. Adelard staff hold PhDs in this area and have research relationships with world class universities.
Please feel free to contact us directly to discuss your requirements.