The UofO LOTOS Project
The LMC Tool
LMC stands for LOTOS Model Checker.
In a nutshell, LMC is a tool that assists the user in
ensuring that the specification under test holds expected properties
specified by formulas that are verfified against the symbolic tree
genereted from the specification by SELA.
Implementation Issues
LMC is not integrated in XEludo yet,
but a standalone version is available with
documentation. The syntax of LMC expressions
is described.
Papers
See Brahim Ghribi Master Thesis
LOTOS Model Checker
for more details, as Postscript documents
Part#1
,
Part#2
and
Part#3.
Examples
A
scenario
exemplifies the use of LMC.
lotos-mgr@csi.uottawa.ca