The key to the success of a software project is to model its
behavior at the early stages of development, regardless of the
programming language used. Such an early analysis allows one
to detect the most costly requirement and design errors before
the implementation phase, i.e. coding and testing, begin.

One method toward that goal is to take an existing language and
extend its capabilities by including some trappings of formal
methods - assertions, annotations etc. This is the philosophy of
 Spark , an Ada-based system for software development,
analysis and even formal proof. It has to be kept in mind,
however, that this approach does not allow one to model the
design using Abstract Data Types (ADT):
SPARK is positively a programming language level design system.

There are several notations that support high level of data abstraction
(e.g., Z, B, C, VDM). However, it has been recognized that it
is essential for the success of a formal method to be supported
by tools. For that reason in the Lab we use the Vienna Definition
Method Specification Language(VDM-SL), which has the most
extensive software support.

To learn more about formal methods in Software Engineering visit
the following sites:

• Center for Software Reliability - latest news on VDM.

• Formal Methods - latest news on formal methods.

• Formal Methods Europe - The European experience

• Courses - Courses on Formal Methods worldwide.

• Formal Methods at NC A&T - A VDM-SL Toolbox course on formal methods at North Carolina A&T State University.