Hi everyone,
I am getting back to my first question regarding the automatic generation of validation scenarios. Let specify the requirements of a system using logical conditions (>, <, =, <=, >=, etc.) on properties (force, velocity, etc.) combined using logical operators (and, or, xor, etc.), and each requirement owns a Boolean assertion function. When this assertion is false, the requirement is not satisfied. For instance, the elements contained in the green rectangle of the attached diagram is the model of the requirement "When the temperature is greater than 5 °C, the pressure shall be greater than 50 Pa" (simplified model since I am only using real signals). In the blue rectangle it is a validation scenario. When we specify a system-of-interest, there are hundreds of such requirements with more or less complicated logical structures. Thus, the automated generation of validation scenarios is of interest to validate that we have specified the right system before designing the system right. As you explained in your previous post, we can use Mathematica to generate random stimulus, but to be exhaustive we need to generate many uniformly distributed random stimulus that cover the entire range of allowed values. The simulation of such models is the only way to provide some evidence that the specification is not only complete (all scenarios are covered) but also consistent (no contradiction or redundancy between requirements). Tools like Simulink Design Verifier have an engine for finding counter-examples of proofs with basic data types (although in practice domains can be more complicated) using Bounded Model Checking, K-Induction rule and SAT solver. Does Wolfram offers such a capability?
Attachments:
