Formal methods & Tools |
MoTor stands for the MoDeST Tool Environment. MoTor is aimed at providing a means to analyse and evaluate MoDeST specifications. MoDeST is a specification language we recently developed. It provides a wide spectrum of modeling concepts, possesses rigid, process-algebra style semantics, and yet provides modern and flexible specification constructs.
MoDeST specifications constitute a coherent starting-point to analyse distinct system characteristics with various techniques, e.g., model checking to assess functional correctness and discrete-event simulation to establish the system's reliability. Analysis results thus refer to the same system specification, rather than to different (and potentially incompatible) specifications of system perspectives like in UML. With MoDeST we take a single formalism, multisolution approach.
Currently we have two backends for the tool one providing a basic First State Next State interface and one that can generate modules for the Möbius modeling environment. Via the latter it is possible to do discrete event simulation of MoDeST specifications.