Identification and elicitation of critical properties is the initial and essential step in the verification process; however, there is no well-defined and generally accepted process to follow.
we employed a combination of approaches in an attempt to be thorough and to understand which approaches were most helpful To do this effectively, we collaborated closely with the SAFM domain experts to identify the set of properties for model checking. Working closely with those who had intimate knowledge of the requirements, design, code, and existing testing infrastructure saved a lot of time and effort.
We then classified those properties in terms of their criticality and importance as well as their general applicability (generic properties such as “no divide by zeros” or “no overflows/underflows”) versus their particular relevance to SAFM (application-specific properties; for example, “the value of the time step shall be between the values … and …”).
Generic properties can be formulated and understood by those who do not have any application-specific domain knowledge. Model checkers such as SPIN and Java PathFinder are able to detect violations of many such properties by default or by the user setting one or more configuration options.
In contrast, specifying application-specific properties is more challenging. As their name suggests, they often require intimate understanding of the system under analysis. Therefore this information is best formulated and captured by or in close collaboration with the original requirements engineers, designers, and developers who have such domain-specific knowledge.
Even with intimate knowledge of the system, the process of identifying the properties of interest is usually not straightforward. These properties must make sense and be the right ones to use for verification of the system. You may also need to further constrain a property or widen its applicability. They must be specified, developed, validated & verified in the same way as any other software artifact.