since it ultimately concerns the problem constructing abstracted formal representations of an informal concrete problem domain, and such an abstraction step is not amenable to formal proof. However, it is possible to validate a specification by proving “challenge” theorems concerning properties that the specification is expected to exhibit. If correct, these theorems reinforce the specifier's understanding of the specification and its relationship with the underlying problem domain. If not, the specification probably needs to be changed to better reflect the domain understanding of those involved with producing (and implementing) the specification. Formal methods of software development are not widely used in industry. Most companies do not consider it cost-effective to apply them in their software development processes. This may be for a variety of reasons, some of which are: Time High initial start up cost with low measurable returns Flexibility A lot of software companies use agile methodologies that focus on flexibility. Doing a formal specification of the whole system up front is often perceived as being the opposite of flexible. However, there is some research into the benefits of using formal specifications with "agile" development Complexity They require a high level of mathematical expertise and the analytical skills to understand and apply them effectively A solution to this would be to develop tools and models that allow for these techniques to be implemented but hide the underlying mathematics Limited scope They do not capture properties of interest for all stakeholders in the project They do not do a good job of specifying user interfaces and user interaction Not cost-effective This is not entirely true, by limiting their use to only core parts of critical systems they have shown to be cost-effective Other limitations: Isolation Low-level ontologies Poor guidance Poor separation of concerns Poor tool feedback Paradigms Formal specification techniques have existed in various domains and on various scales for quite some time. Implementations of formal specifications will differ depending on what kind of system they are attempting to model, how they are applied and at what point in the software life cycle they have been introduced. These types of models can be categorized into the following specification paradigms: History-based specification behavior based on system histories assertions are interpreted over time State-based specification behavior based on system states series of sequential steps, (e.g. a financial transaction) languages such as Z, VDM or B rely on this paradigm Transition-based specification behavior