Formal specification

Last updated

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. [1] [2] These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information. [3]

Contents

Motivation

In each passing decade, computer systems have become increasingly more powerful and, as a result, they have become more impactful to society. Because of this, better techniques are needed to assist in the design and implementation of reliable software. Established engineering disciplines use mathematical analysis as the foundation of creating and validating product design. Formal specifications are one such way to achieve this in software engineering reliability as once predicted. Other methods such as testing are more commonly used to enhance code quality. [1]

Uses

Given such a specification, it is possible to use formal verification techniques to demonstrate that a system design is correct with respect to its specification. This allows incorrect system designs to be revised before any major investments have been made into an actual implementation. Another approach is to use probably correct refinement steps to transform a specification into a design, which is ultimately transformed into an implementation that is correct by construction.

It is important to note that a formal specification is not an implementation, but rather it may be used to develop an implementation. Formal specifications describe what a system should do, not how the system should do it.

A good specification must have some of the following attributes: adequate, internally consistent, unambiguous, complete, satisfied, minimal. [3]

A good specification will have: [3]

One of the main reasons there is interest in formal specifications is that they will provide an ability to perform proofs on software implementations. [2] These proofs may be used to validate a specification, verify correctness of design, or to prove that a program satisfies a specification. [2]

Limitations

A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “correct with respect to a given specification”. Whether the formal specification correctly describes the problem to be solved is a separate issue. It is also a difficult issue to address 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. [4] This may be for a variety of reasons, some of which are:

Other limitations: [3]

Paradigms

Formal specification techniques have existed in various domains and on various scales for quite some time. [6] 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. [2] These types of models can be categorized into the following specification paradigms:

In addition to the above paradigms, there are ways to apply certain heuristics to help improve the creation of these specifications. The paper referenced here best discusses heuristics to use when designing a specification. [6] They do so by applying a divide-and-conquer approach.

Software tools

The Z notation is an example of a leading formal specification language. Others include the Specification Language (VDM-SL) of the Vienna Development Method and the Abstract Machine Notation (AMN) of the B-Method. In the Web services area, formal specification is often used to describe non-functional properties [7] (Web services quality of service).

Some tools are: [4]

See also

Related Research Articles

<span class="mw-page-title-main">Computer science</span> Study of computation

Computer science is the study of computation, information, and automation. Computer science spans theoretical disciplines to applied disciplines.

In computer science, static program analysis is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution in the integrated environment.

In software engineering and computer science, abstraction is the process of generalizing concrete details, such as attributes, away from the study of objects and systems to focus attention on details of greater importance. Abstraction is a fundamental concept in computer science and software engineering, especially within the object-oriented programming paradigm. Examples of this include:

The Vienna Development Method (VDM) is one of the longest-established formal methods for the development of computer-based systems. Originating in work done at the IBM Laboratory Vienna in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language—the VDM Specification Language (VDM-SL). It has an extended form, VDM++, which supports the modeling of object-oriented and concurrent systems. Support for VDM includes commercial and academic tools for analyzing models, including support for testing and proving properties of models and generating program code from validated VDM models. There is a history of industrial usage of VDM and its tools and a growing body of research in the formalism has led to notable contributions to the engineering of critical systems, compilers, concurrent systems and in logic for computer science.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

A programming paradigm is a relatively high-level way to structure and conceptualize the implementation of a computer program. A programming language can be classified as supporting one or more paradigms.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

A modeling language is any artificial language that can be used to express data, information or knowledge or systems in a structure that is defined by a consistent set of rules. The rules are used for interpretation of the meaning of components in the structure of a programming language.

A domain-specific language (DSL) is a computer language specialized to a particular application domain. This is in contrast to a general-purpose language (GPL), which is broadly applicable across domains. There are a wide variety of DSLs, ranging from widely used languages for common domains, such as HTML for web pages, down to languages used by only one or a few pieces of software, such as MUSH soft code. DSLs can be further subdivided by the kind of language, and include domain-specific markup languages, domain-specific modeling languages, and domain-specific programming languages. Special-purpose computer languages have always existed in the computer age, but the term "domain-specific language" has become more popular due to the rise of domain-specific modeling. Simpler DSLs, particularly ones used by a single application, are sometimes informally called mini-languages.

Agile software development is the mindset for developing software that derives from values agreed upon by The Agile Alliance, a group of 17 software practitioners in 2001. As documented in their Manifesto for Agile Software Development the practitioners value:

Refinement is a generic term of computer science that encompasses various approaches for producing correct computer programs and simplifying existing programs to enable their formal verification.

Architecture description languages (ADLs) are used in several disciplines: system engineering, software engineering, and enterprise modelling and engineering.

The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.

Behavior-driven development (BDD) involves naming software tests using domain language to describe the behavior of the code.

Knowledge-based engineering (KBE) is the application of knowledge-based systems technology to the domain of manufacturing design and production. The design process is inherently a knowledge-intensive activity, so a great deal of the emphasis for KBE is on the use of knowledge-based technology to support computer-aided design (CAD) however knowledge-based techniques can be applied to the entire product lifecycle.

Naked objects is an architectural pattern used in software engineering. It is defined by three principles:

In software engineering, a software development process or software development life cycle (SDLC) is a process of planning and managing software development. It typically involves dividing software development work into smaller, parallel, or sequential steps or sub-processes to improve design and/or product management. The methodology may include the pre-definition of specific deliverables and artifacts that are created and completed by a project team to develop or maintain an application.

In information technology a reasoning system is a software system that generates conclusions from available knowledge using logical techniques such as deduction and induction. Reasoning systems play an important role in the implementation of artificial intelligence and knowledge-based systems.

<span class="mw-page-title-main">Dansk Datamatik Center</span> Danish software research and development centre

Dansk Datamatik Center (DDC) was a Danish software research and development centre that existed from 1979 to 1989. Its main purpose was to demonstrate the value of using modern techniques, especially those involving formal methods, in software design and development.

Protocol engineering is the application of systematic methods to the development of communication protocols. It uses many of the principles of software engineering, but it is specific to the development of distributed systems.

References

  1. 1 2 Hierons, R. M.; Bogdanov, K.; Bowen, J. P.; Cleaveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.; Harman, M.; Kapoor, K.; Krause, P.; Lüttgen, G.; Simons, A. J. H.; Vilkomir, S. A.; Woodward, M. R.; Zedan, H. (2009). "Using formal specifications to support testing". ACM Computing Surveys . 41 (2): 1. CiteSeerX   10.1.1.144.3320 . doi:10.1145/1459352.1459354. S2CID   10686134.
  2. 1 2 3 4 5 Gaudel, M.-C. (1994). "Formal specification techniques". Proceedings of 16th International Conference on Software Engineering. pp. 223–227. doi:10.1109/ICSE.1994.296781. ISBN   978-0-8186-5855-6. S2CID   60740848.
  3. 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 Lamsweerde, A. V. (2000). "Formal specification". Proceedings of the conference on the future of Software engineering - ICSE '00. pp. 147–159. doi:10.1145/336512.336546. ISBN   978-1581132533. S2CID   4657483.
  4. 1 2 3 4 Sommerville, Ian (2009). "Formal Specification" (PDF). Software Engineering. Retrieved 3 February 2013.
  5. 1 2 3 Nummenmaa, Timo; Tiensuu, Aleksi; Berki, Eleni; Mikkonen, Tommi; Kuittinen, Jussi; Kultima, Annakaisa (4 August 2011). "Supporting agile development by facilitating natural user interaction with executable formal specifications". ACM SIGSOFT Software Engineering Notes. 36 (4): 1–10. doi:10.1145/1988997.2003643. S2CID   2139235.
  6. 1 2 van der Poll, John A.; Paula Kotze (2002). "What design heuristics may enhance the utility of a formal specification?". Proceedings of the 2002 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology. SAICSIT '02: 179–194. ISBN   9781581135961.
  7. ↑ S-Cube Knowledge Model: Formal Specification
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.