We describe the graphical description techniques, their underlaying semantics and the validation techniques that have been applied to the FM99 example; furthermore we sketch the model and discuss the validation results we have obtained. AUTOFOCUS is the modelling tool, and the Quest environment connects the model to a broad spectrum of validation tools, including model checkers (SMV, SATO), theorem provers (VSE) and test tools (CTE). © 2000 BCS.
CITATION STYLE
Slotosch, O. (2000). Modelling and validation: AutoFocus and quest. Formal Aspects of Computing, 12(4), 225–227. https://doi.org/10.1007/s001650070017
Mendeley helps you to discover research relevant for your work.