Information Technology Reference
In-Depth Information
Fitzgerald spent most of the following ten years in academia working with the
aerospace industry and, for a couple of years, in a start-up company, Transitive. Larsen,
by contrast, spent most of his time in industry at IFAD and Systematic, recently joining
academia at the Engineering College of Aarhus. IFAD, the company that developed the
original VDM tools [22], sold the technology on to the major Japanese company CSK
[23]. The tools remain under very active support and development today. The new Over-
ture initiative [24] is developing an open-source tools platform and plug-ins to deliver
at least the same functionality as the rather more monolithic VDMTools.
VDM today is a well-established formal method based on the ISO standardised
specification language VDM-SL [12] and its object-oriented extension VDM++ [25].
Further extensions have provided facilities for description and analysis of distributed
real-time embedded systems [26,27,28], including explicit modelling of alternative sys-
tem architectures and deployment of functionality to computation and communication
resources.
We have reported elsewhere on the current state of VDM's tools and given data on
industrial applications [10]. However, it is worth briefly reviewing a leading current
application as an indication of how VDM is used today. FeliCa Networks Inc.
2
has
been developing a next generation mobile integrated circuit chip, based on a contactless
card technology developed and promoted by Sony [29]. The specification development
process was carried out in three phases:
1. Writing an informal definition of the requirements in Japanese (383 pages).
2. Creating UML diagrams based on this document.
3. Modelling the system in VDM++ with over 100kLOC of VDM++ (677 pages).
Validation of the VDM++ model involved over 10 million tests. During phases 1 and 2
reviews found only 93 contradictions and faults in requirements and specifications in
total. In phase 3, 162 faults were found through the process of writing and reviewing
the VDM++ model. In addition 116 faults were found by executing the formal model in
VDMTools. Finally, an extra 69 faults were found by combining the evaluation team and
the specification writing teams in reviews. The discovery of these faults are all examples
of insight gained by the formulation of the abstract model and the analysis on it. No
refinement or formal verification has taken place, but the use of formal modelling has
been viewed by the company as a considerable success, so balance of effort and insight
seems to have been appropriate. The FeliCa development team included more than 50
people and the three year project has been completed on time, which is remarkable in
itself. The product is produced in high volume, with potentially high recall costs in case
of defects. By the end of November 2006 more than one million chips had been shipped.
3
A Tools Viewpoint
Developing and maintaining good industry-strength tool support is extremely time con-
suming. The formal methods community has spread its effort over many different for-
malisms. For the developers of the large number of specialised tools, integration with
2
www.felicanetworks.co.jp
Search WWH ::
Custom Search