|
|
|
|
 |
|
|||||||||||||||||||||||||||||||||||||
 |
1. Scope
This document is aimed at those who have decided that it would be a good idea for their project or organisation to use a formal method, but are not sure what steps to take next: which formal method or which kind of formal method will be best for their purposes.
In order to result in a successful outcome, choosing a formal method requires the same approach as any other technical decision. First, one needs to be clear about one's objectives and to know what are the technical, organisational and management constraints. Then one may focus on the characteristics of a formal method which will meet those objectives and constraints. Finally a method can be selected which most closely conforms to, and whose tools, experience and support most closely conforms to those characteristics. This guide is a framework which, we hope, will help you to construct for yourself a decision process tailored to your own application and organisation. The sections which follow consist of possible aims, criteria, characteristics and needs. Considering whether each of these applies should help to focus on and define the objectives, constraints and other criteria particular to an application and organisation which form the context of a choice of formal method, i.e. your application and that part of your organisation which will be using a proposed formal method. The bulleted points, which can be treated as a set of questions for you to ask yourselves, are a guide only; they can be extended or modified according to each individual organisational and technical environment. What is important is to establish and define that environment as clearly as possible before proceeding to make a selection. The purpose of the questions is to help the user organisation to determine appropriate criteria. Accordingly, the questions are grouped into some principal categories in the following sections:
Software and system quality, consistency and integrity can be improved by formalising different products and processes in the development cycle. Are the reasons you want to apply formal techniques:
An application, dissociated from the organisation which is to supply a software system for it, has three kinds of intrinsic characteristics. The first is the "phenomenological model" of the application. This is the mathematics used by the scientific theory of the application to explain its phenomena. For example, the phenomenological model of ballistics and civil engineering is classical mechanics, and that of telephony is traffic and switching theory. The second characteristic is dependent on the first and is the computational model of the application. This relates to the high-level structure of the computations which can reflect and model a specific system within the application domain which obeys the principles defined by the scientific model. The third characteristic of the application relates to the physical and societal environment in which the built system will reside: whether it is embedded, safety-related, cost-critical etc.
Different applications will be acceptable to their customers and users for differing reasons. You may find it insightful to give a weighting to the following features, which are very general and can be extended:
If it is very important that the system should function correctly, the motivation for using formal methods will be strongest, because correctness is the most immediate effect of a formal development. But using formal methods frequently results in software which is better structured and designed, which can in turn produce better performance and less arbitrariness in the user interface.
Different formal methods are supported to different degrees by literature, courses, documented experience and tools. The accessibility of these affect the ease with which a newcomer can use a method. Furthermore different methods can be based on different mathematical paradigms and these may be more or less familiar to an organisation's existing staff. For example, driving a mathematical proof engine is generally regarded as needing more mathematical skill than simply formulating a formal description. So it is useful to list the needs and skill levels of the developers in the organisation who are going to work on the project in question and match those with the user oriented support of any considered method and tool.
To adopt a formal method successfully, an organisation needs to have already a reasonably well-developed software engineering discipline. Not to do so would be like a restaurant trying to deliver advanced recipes from a disorganised, unhygienic kitchen: a delicious meal might sometimes result, but one could not rely on it (and the customers might occasionally fall ill!). If the team or organisation does not yet have a reasonable level of engineering discipline and in-house working standards, it is best to address those issues before more technical ones such as the use of formal methods.
It is going to be much easier to adopt a formal method if the staff have some existing knowledge and understanding of the underlying principles, or have used a formal method already. If this is not the case, a training programme should be designed.
If a formal method is being adopted for the first time, a budget and schedule need to be made for training activity. The use of experienced consultants to guide the first-time use of the method is also advisable.
If a very high degree of confidence is required in the correctness of your software end-product, it may be desirable to choose a method whose support tools enable proofs of correctness.
All methods involve a language with which to express a formal description. Different languages are biased to varying degrees as to the level of abstraction at which they can support discourse. One may categorise these levels of abstraction as follows:
One should choose a method and language whose capability best supports the part of the development process where formalisation is going to be most beneficial.
The languages within different methods will generally, if expressing functionality of the software at either specification or design level, allow the expression of different kinds of computation. These largely need to match the computational model of the application. One classification of these models is the following:
Most formal methods are now supported by tools, but the tools vary in their capabilities, maturity, degree of commercial support, ease of use, etc. Browsing through the FMEInfRes tools database should provide a good indication of the availability of tools. Tools vary in their maturity; it will be fairly clear from the database entry whether the tool is used industrially and on what scale. As well as the "Availability" and "Usage and Applicability" sections, the "Number of Installations" will give an indication of this. However, visitors to the database should be aware that different tool suppliers operate in different customer situations and have different ways of estimating the number of installations. A widely used free tool supplier may count the number of downloads from their FTP site. This may be a substantially greater number than the number of tools in serious use. Another may count the number of paid-for user or site licences. Also, not all suppliers have yet provided us with their number of installations. The entry for the tool gives an indication of how the number of installations is assessed, but for full and up-to-date information on any tool one should visit the tool's own site and consult the contact point.
Some tool suppliers, developers of existing applications and other systems and software houses provide training and consultancy on the use of formal methods.
To find accounts of existing experience, visit the Applications Database at this site. Also, there are comprehensive accounts of experience in [1].
|
|||||||||||||||||||||||||||||||||||||
 |
||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||
|
© copyright 2004 | Formal Methods Europe |
||||||||||||||||||||||||||||||||||||||
Choosing