Information Technology Reference
In-Depth Information
large parts of the industry [78]. Such a bi-directional link with developed for VDM-
Tools to support interaction with the Rose UML tool. The effort/insight balance is
improved by linkage between informal and formal tools. However the links do not
simply have to be with classical software design tools. For example, integration
with a continuous time simulator is a promising vehicle for collaboration between
systems and software engineers [79], both working in different, but both formal,
spheres.
Combination with Development Environments:
Companies have development en-
vironments that must be used for for integrating the final system. It is also likely
that the implementation derived from a formal model will need to be integrated
with code that is developed differently (e.g. for existing GUI or legacy code). Here
the effort/insight balance is affected by the ease of doing this kind of integration.
Features for combining existing code with a formal model may prove valuable [80],
as may facilities for combining with a GUI interface [81].
3.5
Past and Future for Formal Methods Tools
Tools for formal modelling and analysis have come a long way since work began on
VDM-SL parsers, but competition with conventional tools is hard. In the 1980s tools
for formal specification were mainly limited to basic static checks for syntax- and type-
correctness. At that time it was even possible to write PhD thesis about general formal
methods tool support [82]. The 1990s saw an increase in the range of tools exploiting
more of the formal semantics, in particular interpreters, code generators, test case gener-
ators, model checking and proof support. In addition many of the tools had support for
combining formal models with informal, usually graphical, notations. At present, we
conjecture that none of the formal methods tools are as highly featured as the leading
industrial software development tools.
Open source platforms with potentially closed-source plug-ins offer a promising ap-
proach for delivering tools with the capabilities that we have discussed [83,24]. If this
can be achieved tool builders will not have to start from scratch whenever tool support
is to be developed for a new notation. Ideally, different views or parts of a system could
be described in different formalisms and verification of properties could be performed
by a variety of theorem provers in a compositional way. However, before this becomes
a reality there are major theoretical challenges on semantic integration that must be
addressed.
Our own experience with VDMTools and the Overture initiative leads us to want to
address several areas:
-
Co-simulation as an extension of executable specification and the use of interpreters
for control applications in embedded real-time systems.
-
Modelling faults and experimenting with alternative fault detection and tolerance
mechanisms inside formal models.
-
User-guided proof for gaining deep insight at a higher level than conventional the-
orem provers.
Search WWH ::
Custom Search