[Prev][Next][Index]
Larch and OOA
Dear Keith:
I am on the Larch interest mailing list and I saw your query to Jim Horning.
I previously worked for BCS several years ago and I am very happy to hear
that your group is pursuing the possibilities of using formal specification
languages.
The Software Engineering Research Group at Michigan State University
has been working for the past several years on building techniques
and tools to support the use of formal methods for software engineering.
There are two tools that we have built that might be of specific interest
to you.
Recently, we completed the definition of formal syntax and semantics
for the object oriented modeling notation known as OMT (by Rumbaugh and
company). As you may already know, the OMT notation comprises three
diagramming techniques: object model (OOA/OOD), functional model (DFDs), and
dynamic model (statecharts). We have spent significant energies in
capturing formal semantics for the object models. The objective of the
project is to allow users to capture requirements information using
diagrams and to generate the corresponding formal specifications (within
reason) using our tool. Currently, we have an algebraic formalization
of the object model. Our tool is built such that it is grammar-based. That
is, the semantics of the object models are algebraic, in nature, and we
can decide which specific algebraic syntax we wish to use by supplying
the appropriate grammar to the system. Currently, we have targeted Larch as the language because of the existing tool support.
The second utility that might be of interest is a Larch Development Environment
(LDE) that we have built based on the original tools (syntax checkers, provers)
developed by Horning, Guttag, and others. LDE is graphics-based environment
for building Larch specifications, including a graphical browser of existing
traits, access to syntax checking and prover, easy generation of
sort, dependency, lookup of referenced traits,