Given a space of possible RADON models (in a dynamic situation, new devices such as robotic assistants may be added/taken away), the tool could verify that any RADON model in the space complies with a set of hard constraints

[marklaw]

From D2.1 (Companion)

ID	R-T4.1-11
Section	WP4: Modelling Environment Requirements
Type	FUNCTIONAL_SUITABILITY
User Story	As a QoS Engineer/Operations Engineer, I want to be able to guarantee that in a dynamic situation, where new devices are being continually added and taken away, these dynamic changes are guaranteed not to cause my RADON model to violate my hard constraint.
Requirement	Given a space of possible RADON models (in a dynamic situation, new devices such as robotic assistants may be added/taken away), the tool could verify that any RADON model in the space complies with a set of hard constraints.
Extended Description	This computation may take place offline.
Priority	Could have
Affected Tools	VT
Means of Verification	Proof of soundness and completeness. This constitutes proving that any violating RADON model within the space will be found (completeness) and that if a RADON model in the space is reported to be violating, it does indeed violate at least one hard constraint (soundness).
Dependency	R-T4.1-1, R-T4.1-2, R-T4.1-3

[marklaw]

@gcasale Similarly to RT4.1-5, I have downgraded the "means of verification". Again, if this is an issue, I can change it back.

[gcasale]

What was it before?