A Validation Environment for LOTOS
Brahim Ghribi, Luigi Logrippo · 1993
This paper presents a set of mutually integrated tools that have been developed at the University of Ottawa for the validation of LOTOS specifications. This set includes a step-by-step interactive executor, similar to HIPPO [vE89], but with additional features related to those of SMILE [EW92], a behavior graph generator having features similar to those of LOLA [QFP88], and a CTL model checker. We show how the features of the toolkit can be used to validate specifications, with emphasis on the use of the model-checker.