ABSTRACT:
We propose a semantics-based approach, Metro, to generate analyzers
automatically from the description of notations' semantics. In Metro, the
semantics of a notation are defined and fed into a model compiler together
with a specification in that notation. A transition-relation for the
specification is generated automatically, which can be checked using many
automatic analysis tools (e.g., model checkers). However, the semantics of
many model-based notations (e.g., statecharts and process algebras) are
complex and formalizing their semantics can be challenging and
error-prone.
                                                                                
To ease the effort required to define the semantics, we have
developed an operational semantics template that captures the common
behaviour of different notations and parameterizes notations' distinct
behaviours. We have also identified seven well-used composition operators
and defined the semantics of these operators separately, as relations that
constrain how components can execute concurrently, and communicate and
synchronize with each other by exchanging events and data. By separating a
notation's step-semantics from its composition and concurrency operators,
we simplify the definitions of both. We have used our template to capture
the essential semantics of basic transition systems, CSP, CCS, basic
LOTOS, a subset of SDL88, and a variety of statecharts notations.