LOEWE: A LOTOS engineering workbench

Abstract

LOEWE is an integrated tools environment for the specification, analysis, and implementation of communication software. Although primarily based on the formal description technique LOTOS, LOEWE additionally offers multiple, semantically equivalent representations of a given protocol specification. Each format is specially adapted to support specific tool functionality: processes are used for simulation and compilation, fast state space exploration is performed on extended finite state machines, and labelled transition graphs are used for system verification. LOEWE currently contains a LOTOS syntax and static semantic verifier, a generator of extended finite state machines with associated interactive state exploration tools, a temporal logic verifier, a compiler to generate C code from LOTOS behavior expressions, a translator of LOTOS abstract data type operations to a set of LISP functions, and a graphical trace analyzer of LOTOS process interactions. © 1993.