ASD
What's inside the ASD:Suite
Verum has invented a patented technology for designing and mathematically verifying the correctness and completeness of behaviourally complex software systems. This technology is called Analytical Software Design (ASD).
The result is a technology that allows designs of complex software systems to be modelled and mathematically verified for completeness and correctness to specification before a single line of code has been written.The ASD:Suite:
Is a software engineering tool for:
|
Guarantees:
|
Provides:
|
Is a paradigm shift:
|
How ASD works
The process starts by capturing the requirements and behaviour of a component in an ASD model. This is then used to automatically generate a formal model which is checked for design errors, which are corrected in the ASD model. The result is an ASD model which is precise, complete, traceable and correct. Source code is automatically generated directly from this verified model. Uniquely, ASD guarantees equivalence between the generated source code and the formally verified model as shown in the “ASD triangle”:
Underlying technology
ASD was invented by Guy Broadfoot, one of Verum’s co-founders, who combined two existing technologies from industry and the University of Oxford. The result is a model-based component technology supported by a toolset for constructing industrial scale systems from verified components. ASD models use Sequence-Based Specifications technology to specify both interfaces and designs of components, thereby ensuring mathematical completeness of the ASD models in the sense that in every state, the consequences of all stimuli are specified; if a stimulus is not allowed or expected in a given state, then it is explicitly specified as illegal.
The specifications are traceable to the original requirements and remain completely accessible to critical stakeholders. This allows them to play a key role in validating the ASD models and retain control over them. At the same time, ASD models provide the rigor and precision necessary for the formal verification. The Sequence-Based Specifications were extended to support non-determinism for the purposes of specifying interface behaviour.
The formal models are based on the process algebra CSP invented at the University of Oxford. The verification of these formal models is done using the Failures Divergence Refinement model-checker tool and ensures that a design satisfies its functional requirements, and that a design is free from race conditions with its used interfaces, and free from dead-locks and live-locks. The compositional property of CSP refinement provides the necessary scalability for industrial size systems: rather than verifying complete systems, a system is verified component by component in such a way that the composition of all these components together is guaranteed to work properly.
Once all components have been verified and are defect free by model-checking, the source code can be automatically generated from the ASD models. The source code can be easily integrated in a configuration management and/or build environment.
A paradigm shift
ASD allows software architects and designers to build behaviourally complex software systems and verify them before a single line of code has been written. This changes the focus of software development from coding and testing to requirements, architecture, and design.
Get in touch
For more information or a product demonstration contact us.
 |
+31-40-2359090 |
 |
+31-40-2359099 |
 |
info@verum.com |
 |
Location |
