The challenge
Introducing new capability for vehicles, aircraft, autonomous systems, etc typically requires considerable time and money as the software needs to be built, verified, iterated, rebuilt, (repeat), go through a safety assessment, rebuild (repeat, etc) until eventually it gets into service. Most initiatives in software focus on the softer people-oriented process aspects (such as ‘agile’, ‘Dev Sec Ops’, etc)that fail to tackle the fundamental problem and that is ease of verification starting with requirements and finishing with binary. All human based activities (e.g. review and test) are subjective and are therefore error prone and are costly in terms of time and money. The real kicker is the production of evidence to satisfy the safety (and security) processes such as DO-178C.Wouldn’t it be good if the vast majority of the uncertainty could be removed throughout the software life cycle enabling embedded software systems to be released to service much more rapidly than at present?
USE OF AUTOMATIC FORMAL PROOF
Building upon human based verification processes that were originally used for support to the Release to Service for the Typhoon, D-RisQ has spent considerable time developing accessible verification processes that remove most of the need for review and test at every stage of the software development life cycle. The techniques are currently focused on embedded real-time control systems such as those found in equipment that moves e.g. control surfaces, moveable arms, high integrity decision making systems and may have mode or state logic systems. The uncertainty of standard processes is removed by use of tools that enable developers to write sound, verifiable ,unambiguous, complete, consistent requirements. In trials of this one technology, a set of existing well written requirements were transposed to our technologies and it was found that 12% had significant problems; note that this was early stages of the development process, so iteration was highly likely. The next stage is to assure a design written in the off-the-shelf tool called Simulink. We automatically translate the design to a mathematical language along with the requirements for the design and can therefore automatically prove that the design does or does not implement the requirements. In independent blind seeded trials, the technology has been shown to be 80% faster(in one instance 8 days to became 1). Once this stage is passed, everything becomes largely automatic with independent verification of autocode and shortly the independent verification of the compiled code. All this is undertaken with the explicit intent of meeting internationally recognised software safety standards such asDO-178C (for aerospace).
The initial software development cycle can be significantly reduced and more importantly, iteration or modification becomes extremely rapid. In one project a significant modification to safety critical code was needed; this was produced and put into trials in less than 2 weeks elapsed time (NB only about 16 hours actual work). The techniques are designed for use by typical software engineers. Our requirements tools are often now used by 15 year old interns. There is little adaptation to well known processes, with the adoption of requirements, design and coding standards being the small change and a change to emphasis on getting well written requirements (system and software). The emphasis is on compliance to standards, the application of automation and the verifiable nature brought by automation. It left shifts understanding of the software development process.
Privacy Policy | Terms & Conditions
Drisq Ltd 2024. All rights reserved. Design by Design in the Shires