1
Download User Manual: Model Checking - Software and Systems Engineering
Transcript
Validas Model Checking for AutoFOCUS o Component MSCs: for every verified component a black-box MSC and for every component with a structure a MSC with internal messages are generated if this option is chosen o Basic MSC is a MSC with all atomic components in the verified system • Generation of MSC elements allows to select the generated elements in the counter examples. State and local variable information can be added to MSC in all steps, or only if the values change. page 23
