Software engineers charged with writing code for embedded systems are likely to benefit from the use of CLawZ®. The automatic generation and subsequent automatic independent verification of the resultant source code assists engineers in achieving high quality software with fewer iterations. This cuts costs and lowers the project risk for project managers as well as enabling regulators to understand the detailed operation of the software.
CLawZ® is being used on internal projects such as our autonomous systems projects and will shortly be made available to external developers. Although CLawZ® can be used in isolation to prove autocode, significantly more benefit is gained when it is used in conjunction with Kapture® and Modelworks® leading to much lower costs of development. The projects D-RisQ are planning to use CLawZ® on include highly assured decision making for autonomous vehicles in air, maritime and sub-surface. The sub-set of C (C-♭) is an implementation of MISRA-C that has formal semantics produced and verified by D-RisQ; and is available request.