Automating verification

CAESAR

Discover more

KAPTURE®

Discover more

Modelworks®

Discover more

Clawz®

Discover more

FEVER®

Coming Soon

Automating verification VIDEO

Automating verification with the power of formal methods

Simplicity is prerequisite for reliability

The principle adopted in the development of the D-RisQ tools is that no specialist skills would be in order to use the D-RisQ tools.

The aim is to achieve verification at the press of a button and hence be accessible to all software engineers. Enabling the adoption of good engineering practice to avoid error introduction, use of requirements, design and coding standards and ensuring compliance to internationally recognised software standards underpins every aspect of D-RisQ tools.

Kapture®

Kapture enables a user to write software requirements in a clear concise verifiable manner. It enables the early discovery of requirements issues before the expense of design, code and verification.

Kapture: Getting the right software requirements early in the software life cycle.

Discover more

Modelworks®

Modelworks enables the automatic verification of designs in Simulink and Stateflow. Modelworks shows that the design encapsulates the verifiable requirements written in Kapture or shows where is does not.

Modelworks: Getting the design right early in the software life cycle.

Discover more

CLAWZ®

CLawZ enables the automatic independent verification of C source code generated from Simulink®/Stateflow® models. Should the autocoder have made a mistake, it will show where in the code the issue lies and relate it to the original design.

CLawZ: Automating source code verification.

Discover more

COMING SOON

CAESAR

Capturing and Assuring System Requirements.

The start of all software development is a set of customer requirements. Typically, these are System Requirements and only give basic details of what the behaviour is expected at a system level.

CAESAR enables the clear, unambiguous, consistent development of system requirements. These attributes are needed in order to be able to accurately communicate the need to software developers and system validators as well as to any other stakeholders, such as regulators.

CAESAR will link to Kapture to enable not only a trace function but also refinement checks.

CAESAR: Getting the right system requirements early in the development life cycle.

Discover more

COMING SOON

FEVER

The automatic verification of Executable Object Code.

Verifying that the binary or Executable Object Code is correct with respect to the source code from which it has been compiled is a typically lengthy process requiring many tests.

Proving that binary satisfies the original source code automatically is the job for FEVER. This includes the functional code written in the C𝄬 coding standard as well as the associated build code such as library files.

Discover more

Free to Access C Coding Standard

It is the primitive nature of the C programming language, which makes it so flexible and powerful, that also makes it difficult to assure programs written in it. D-RisQ has developed a coding standard called C𝄬 which is an implementation of MISRA-C coding guidelines.

The purpose of thisguide is so that software developers and managers can learn how to use a subset of C, called C♭, for critical systems.

It presents an abstract syntax for the C♭ language along with a particular instance of a concrete syntax from a family of possible concrete syntaxes. A narrative with examples illustrating language constructs is given. To access this standard please contact D-RisQ.

Software products

AUTOMATING VERIFICATION

CAESAR

read more

KAPTURE®

read more

Modelworks®

read more

Clawz®

read more

FEVER®

read more

Automating verification with the power of formal methods

Simplicity is prerequisite for reliability

Kapture®

Modelworks®

CLAWZ®

CAESAR

FEVER

Free to Access C Coding Standard

WANT TO REDUCE THE COST OF EMBEDDED SOFTWARE DEVELOPMENT? CONTACT US TODAY TO FIND OUT MORE