Steam Boiler Exemplar

CASE STUDY

DrisQ Tools and Development Process
D-risq - Caesar image

System Requirements, Validation and Verification - System Kapture

The Abrial specification is used as the basis for the development of a set of System Requirements Allocated to Software (SRATS).  We used System Kapture, which exploits structured English in easy to use templates.  The use of a tool to write clear, concise, unambiguous SRATS enables an exploration of desired properties and crucially, to show absence of undesired behaviour.  There is a ‘requirements standard’ adhered to as a by-product of the use of this technology, which means that a user focuses on the important aspects of requirements.  This provides a robust base upon which to develop the software, with the bulk of the effort dedicated to evolving the SRATS.

Certification Credit

For DO-178C/DO-333, there are no objectives to be met.  However, without a good set of SRATS it is very difficult to develop good software.  System Kapture assists in the development of a sound basis from which to develop ‘certifiable’ software.

D-risq - Kapture image

Software Requirements and Verification – Kapture®

The next step is to develop a software specification in Software High Level Requirements, again using a structured English approach in Kapture®. This is a tool that has formal semantics in the background and complies with a requirements standard encapsulated within the tool.  We showed that we can prove that these software requirements implement the SRATS.

Certification Credit

If Kapture is used in conjunction with System Kapture, then the table below gives a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the use of the tools.

DrisQ DO-333 Objectives Table

Extract from DO-333 Annex A Table FM.A-3 (including use of System Kapture)

Design and Verification - Modelworks®

A design has been undertaken in a subset of Simulink®/Stateflow® and compliance with a standard is checked. Then an automatic independent proof is undertaken using Modelworks® to show that the graphical design correctly implements the requirements, or to show where it does not.

Certification Credit

The table below gives a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the use of Modelworks.

DrisQ DO-333 Objectives Table

Extract from DO-333 Annex A Table FM.A-4

D-risq - Clawz image

Source Code and Verification – CLawZ®

By using an autocoder, the production of source code is a matter of a few seconds and is automatically checked for compliance to a coding standard. It is then automatically and independently verified using the formal proof in CLawZ® to show that the code correctly implements the design or to highlight issues.

Certification Credit

The table below gives a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the use of CLawZ®.

DrisQ DO-333 Objectives Table

Extract from DO-333 Annex A Table FM.A-5

D-risq - Fever image

Executable and Verification – FEVER®

The final part of the development discussed is the verification of the Executable Object Code (EOC), again through the use of formal proof embedded in our forthcoming FEVER® tool.   By bringing all the tools together, we also show how to achieve an equivalent to ‘coverage’ of both requirements and code structure, thus significantly reducing effort.

Tool Qualification

The certification claims are based upon use of DO-333, the Formal Methods Supplement to DO-178C.  This also includes tool qualification that users would have to undertake to DO-330, the Tool Qualification guidance for Aerospace.  Certification and tool qualification is discussed in each of the relevant stages.

Although every tool has its limitations and, some are still in development, our Toolsuite tackles numerous software development challenges. It empowers developers to quickly create verified software functionality, boosting productivity, accelerating time-to-market, and cutting costs.

Certification Credit

The tables below give a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the future use of FEVER®.

DO-333, section FM.6.7.f gives options for the verification activities of EOC.  In our case we have used formal models for the HLR, design, source code and of the EOC.  It is in this context that claims for certification credit may be made meeting; see the diagram below which shows the transitivity of proof.

DrisQ DO-333 Certification credit

We are therefore effectively undertaking a ‘complementary analysis’ which shows that the translation of the source to EOC is correct; that is, the desired properties of the source code are preserved.  The tables below give a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the use of FEVER®:

DrisQ DO-333 Objectives Table

Extract from DO-333 Annex A Table FM.A-6

Noting the transitivity of proof, the table below is a summary of the Objectives expected to be met by the full use of the Toolsuite:

DrisQ DO-333 Objectives Table

Extract from DO-333 Annex A Table FM.A-7

For further information get in touch with us today via email or telephone.

Need help with control system software? Contact us today to find out more

Get in touch
D-Risq - Logo