In our latest deliverable ‘D4.1 Constraint Definition Language’, Mark Law and Alessandra Russo from Imperial College London presented the Constraint Definition Language (CDL) and its associated Verification Tool (VT) as a set of tools for the specification of requirements, constraints and desired properties, and the relevant assurance that development complies with these requirements.
As they mention in this report, CDL is used to express functional and non-functional requirements on a RADON model, by providing built-in definitions of common runtime issues. However, this language is flexible enough to allow users to define their own elements.
Furthermore, VT is able to check whether a selected RADON model conforms to a given CDL specification. Subsequently, this tool can suggest potential corrections in the RADON models to rectify any detected inconsistencies with the expressed constraints that could eventually raise issues at runtime.
In the current prototype of this set of verification solutions, CDL can support encoding pre and post conditions of functions, as well as defining hard constraints with respect to security and performance requirements. We are now in the phase of extending CDL by introducing predicates that would be able to represent such hard constraints in the form of policies. In the next release of our tool, CDL will also be able to express architectural pattern constraints.
In the same sense, VT currently is invoked through a command line prototype that can solve CDL specifications, with emphasis on hard constraints, race conditions, loops, and deadlocks. As the CDL language is developed further, the verification tool will be able to address policy specifications and it will be optimized to respond to the issues raised in the respective repository in real-time.
In the next period, our team expects to proceed with a full-scale validation of the verification tool and the cases that this tool can be used for compliance with CDL policies.
You can read the deliverable D4.1 Constraint Definition Language here.