1
Download User Manual: Model Checking - Software and Systems Engineering
Transcript
Validas Model Checking for AutoFOCUS Figure 16: Encoding Panel 5.5 MSC The MSC panel allows to configure the generation of counter examples (see Figure 17). The following options can be set: • Generation of MSCs can be controlled (note that in some cases identical MSCs can be generated, e.g. if only one component is checked) o Black-box MSC: is a MSC that shows the selected component as a black box (only from outside) page 22
