Welcome to the web pages of the

Formal Techniques Industrial Association (ForTIA)

A joint undertaking by
Formal Methods Europe (FME) and
CoLogNET: Network of Excellence in Computational Logic

Administrative Information

• The ForTIA members
• The ForTIA board
• Our charter
• Our bylaws
• Our Annual General Meetings

Events

• ForTIA Industry Day at FM'08 on 28 May 2008, Holiday Club Turku, Finland
• ForTIA Industry Day at FM'06 on 23 August 2006, McMaster University, Hamilton, Ontario, Canada
• ForTIA Industry Day at FM'05 on 20 July 2005, University of Newcastle Upon Tyne, Newcastle, UK

Literature

• Ten Commandments of Formal Methods ...Ten Years Later by Jonathan Bowen and Mike Hinchey, reflecting on 10 years of progress since their well-known "Ten Commandments" paper was published. To be found in the January 2006 issue of IEEE Computer.
• Interesting articles published in IEEE Spectrum Sep 2005 discussing the issue of software project failure:
  • The Exterminators by Philip E. Ross: A small British firm shows that software bugs aren't inevitable
  • Why Software Fails by Robert N. Charette: We waste billions of dollars each year on entirely preventable mistakes

Preface

This web site introduces ForTIA, the Formal Techniques Industrial Association. ForTIA is an association of industrial organisations who use and/or supply tools, ideas and services in the area of formal techniques. Formal techniques are explained on page 5 of this web site. This web site also lists the founding members of ForTIA.

An increasing number of small to medium sized IT companies are providing design and consultancy services based on the use of formal techniques. The customers for these designs and services are, often large scale, IT consumers or producers. The techniques may be applied to the development of software, hardware, or composite systems. These companies can thus be characterised by their use of a variety of formal techniques, both established and emerging, and by their close collaboration with the formal techniques segment of academia. At the same time, the numbers of staff in this segment of academia, interested in teaching and researching formal techniques, are growing.

These two partners, industrial and academic, have a mutual benefit. The academic partners thrive on the collaboration in being challenged to new achievements. They therefore have a strong interest in the prosperity of the industrial partners. The industrial partners in turn need strong academic groups in order to recruit increasing numbers of highly professional software engineer cum computer scientist staff.

Yet students can remain unconvinced of the utility of courses in formal techniques, believing that big IT industry does not use them.

ForTIA is an association of industrial companies, comprising both suppliers and, above all, users, of formal techniques. Its aim is not just one of mutual benefit and information sharing, although we certainly hope that will happen. ForTIA should actively work to ensure that good tools and techniques are researched, developed and deployed. But it should be recognised that the field of formal techniques is not yet completely mature. They should not be oversold or presented as a panacea. The utility of formal techniques will be far more effectively demonstrated by successful projects and tools that use them. This should be an emphasis of the association.

To put it another way, actions speak louder than words!

Dines Bjørner

Formal Methods

Formal methods are mathematical approaches to software and system development which support the rigorous specification, design and verification of computer systems. The use of notations and languages with a defined mathematical meaning enable specifications, that is statements of what the proposed system should do, to be expressed with precision and without ambiguity. The properties of the specifications can be deduced with greater confidence and replayed to the customers, often uncovering facets implicit in the stated requirements which they had not realised. In this way a more complete requirements validation can take place earlier in the life-cycle, with subsequent cost savings.

Designs, likewise expressed in a language with a mathematically defined meaning, can be methodically derived from the specifications so as to provably possess all their properties. Several levels of specification and/or design may be produced, each derived from and fulfilling the properties of its predecessor. This process is known as refinement or reification - to reify is to make something into ‘a thing’ or more concrete. The lower levels of design will typically use language structures which are closer to those found in the programming language in which the software is implemented. This final reification step can be proved correct only if the implementation language has a formally defined meaning, or semantics. This is the case with an increasing number of languages (Ada, Pascal and Modula-2 are examples) and the formal semantics definitions of some languages have now started to be incorporated in their international standard definitions. Even if the implementation language does not have a written definition of its formal semantics, one can justifiably have greater confidence in the correctness of the implementation if the step from the lowest level of design to the implementation is clear, visible and detailed.

After an initial training period, using formal methods rarely costs more than using conventional methods in a development, provided the formal method has been sensibly integrated into the organisation’s current development life-cycle. The usual experience is that costs are greater and time-scales longer during the earlier stages of the life-cycle, but are more than compensated by lower costs and shorter time-scales in the later stages of the development. There is no evidence that the resulting implementations are any less efficient in time or space; indeed, there is some empirical evidence showing the reverse.

Formal methods are principles, procedures and practices of software and systems development that are based on formal techniques. Formal techniques, in turn, are means of abstractly modelling the products in a process. The process may be software or systems development, or hardware development, or other parts of an engineering life-cycle such as reverse engineering or maintenance. Indeed, formal techniques can and have been used in other processes such as devising and analysing organisational procedures e.g. the rules for rest periods taken by long distance lorry drivers, and deriving user manuals for technical equipment.

Examples of formal techniques and some associated tools are: Z, B, VDM, HOL, ProofPower, EVES, Isabelle, J@T, KVEST and UniTESK, SPARK Ada, LOTOS, RAISE.

.

Preparation, printing and distribution of a predecessor or this web site, was partially funded by the 5th EU/IST Framework Programme of the European Commission, Contract Reference IST-2001-33123: CoLogNET: Network of Excellence in Computational Logic