WANT TO AVOID EXPENSIVE UNIT TEST BY AUTOMATICALLY PROVING THAT THE AUTO-GENERATED SOURCE CODE IMPLEMENTS THE DESIGN? TRY CLawZ®.
The manual generation of code is inevitably fraught with errors leading to expensive re-work. Even if code is automatically generated, unit test is required to demonstrate that the code is error free and further tests have to show that it implements the software design. CLawZ® avoids the time and cost of undertaking unit test because it automatically proves that the automatically generated code correctly, completely and accurately implements a design expressed in Simulink/Stateflow.
CLawZ® achieves this through a few steps focused on verifiability and conformance to standards. Firstly, CLawZ® ensures that the Simulink/Stateflow design conforms to the Design Standard for the subset of Simulink/Stateflow. Once this automatic check is complete, it is then possible to use an off-the-shelf autocoder to produce code which is then automatically checked for compliance to the Coding Standard. This Coding Standard is a subset of C that is an implementation of MISRA-C. The sub-set is called C-♭ and has a set of independently proven formal semantics for use in programme proof.
D-RisQ has designed CLawZ® in a user friendly way so that should the proof fail, it will show exactly where in the code the issue lies and align it with the specific area in the design that has the issue. CLawZ® also provides the evidence to support certification to meet the demands of regulated industries.
When CLawZ® is used in conjunction with D-RisQ’s Kapture® and Modelworks® tools, the chain of evidence proves that the source code correctly, completely and accurately implements the software requirements. Indeed, the Design Standard for Modelworks® is the same as the Design Standard for CLawZ®. This allows software engineers the time to concentrate on optimising the operation of the software. Because the code generation and verification are automatic, it means the focus is where it should be, on the requirements and then on the design. D-RisQ is using CLawZ® on various projects, notably for highly assured decision making for autonomous vehicles in air, maritime and sub-surface as well as in nuclear decommissioning.
In order to make the application code run, other software is needed in order to build the run-time. This non-application code or ‘glueware’ such as libraries and drivers, is typically off-the-shelf or hand coded by the developer. The checker for the compliance to the C-♭ subset is available for use as a stand-alone tool for this type of code. The advantages being that all the code, application and non-application, can be in accordance with this very useful, deterministic subset of C. The coding standard for C-♭, which has an abstract and concrete syntax as well as formal semantics produced and verified by D-RisQ, is available on request.
Privacy Policy | Terms & Conditions
Drisq Ltd 2023. All rights reserved. Design by Design in the Shires
