The verification tool should be able to check for the existence of potential race conditions and/or execution loops and related deadlocks that could happen

marklaw commented 4 years ago

From D2.1 (Companion)

ID	R-T4.1-7
Section	WP4: Modelling Environment Requirements
Type	FUNCTIONAL_SUITABILITY
User Story	As a QoS Engineer/Operations Engineer I want to test RADON model for existence of race conditions and/or execution loops.
Requirement	The verification tool should be able to check for the existence of potential race conditions and/or execution loops and related deadlocks that could happen.
Extended Description	For instance different operators receiving requests for different actions regarding the same patient or which require sharing of resources of robotic assistants. In the case that such events can occur, the tool should provide an example trace as explanation.
Priority	Should have
Affected Tools	VT
Means of Verification	Formal proof of the soundness and completeness of the verification algorithm
Dependency	R-T4.1-1, R-T4.1-2, R-T4.1-3

marklaw commented 3 years ago

@gcasale I propose that this should be closed, as we showed the CDL could do this in D4.1

gcasale commented 3 years ago

We can close only if the requirement is completed, is the version in D4.1 final?

radon-h2020 / radon-verification-tool