Verification and Validation
How we do it...
Today, unwound non-linear models are unwound manually to perform formal verification. Analysis is usually inconclusive.
Rapide models can be used for both verification and validation. While there are not uniformly adopted definitions of these terms, we will use the US National Institute of Standards and Technology. Their definition is “(verification) the process of determining (proof or evaluation) whether the requirements for a system or component are complete and correct, the products of each development phase fulfill the requirements or conditions imposed by the previous phase, and (validation) the final system or component complies with specified requirements.”
- DARPA funded a Stanford University team to create an architecture definition language (ADL) that could be applied for formal verification. This research led to the formation of Rapide pattern language, which has a semantics based on causally related events.
- The key is that our software based on Rapide can read a state machine. Rules for correlation are no longer needed.
- DADA-X platform checks the execution of distributed concurrent systems, applications and smart contracts for anomalous behavior using non-linear models.
What is the difference between verification and validation?
Verification is a test of a system to prove (formal verification) or evaluate (informal verification) that it meets all its specified requirements. In the case of formal verification, the emphasis is on proof. Rapide’s modeling language permits declarative specification of behaviors of a system, and those specifications have a formal basis that facilitates proving properties of the system with theorem provers. This is complemented with a simulation capability that allows the models to be run through the various scenarios to ensure the behavior doesn’t violate constraints. Simulation enables evaluation of the models against the specified requirements. Both theorem provers and simulation can be used to prove and evaluate that the model satisfies its requirements.
Validation is used to ensure a system operates in a way that satisfies its requirements. In this case, we use Rapide’s mapping functionality to validate the system’s behavior against the model. The underlying behavior of the system is encoded as events that are mapped to the verified model. The system’s behavior is thereby viewed through the lens of the verified model, such that any behaviors that violate the model indicate that the underlying system’s behavior has violated the system specifications.
We have extended Java for causality. Our Rapide compiler code is J2EE compliant! We compile UML into J2EE code to run on any JVM. The code does verification and validation for any system or smart contract.