**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

Concept# Formal specification

Summary

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. 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.
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.
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
A good specification will have:
Constructability, manageability and evolvability
Usability
Communicability
Powerful and efficient analysis
One of the main reasons there is interest in formal specifications is that they will provide an ability to perform proofs on software implementations.

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (16)

Related people (1)

Related concepts (17)

Related courses (2)

Related lectures (98)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

AR-362: Theory of urbanism

Le cours de Théorie de l'Urbanisme traite des modèles, projets et techniques de l'urbanisme entre XVIIIe et XXIe siècle, en mettant en relation discours théorique et projet, texte et image. Le projet

Refinement (computing)

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. In formal methods, program refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete (low-level) executable program. Stepwise refinement allows this process to be done in stages. Logically, refinement normally involves implication, but there can be additional complications.

Correctness (computer science)

In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm (i.e., for each input it produces an output satisfying the specification). Within the latter notion, partial correctness, requiring that if an answer is returned it will be correct, is distinguished from total correctness, which additionally requires that an answer is eventually returned, i.e.

Z notation

The Z notation ˈzɛd is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general. In 1974, Jean-Raymond Abrial published "Data Semantics". He used a notation that would later be taught in the University of Grenoble until the end of the 1980s. While at EDF (Électricité de France), working with Bertrand Meyer, Abrial also worked on developing Z. The Z notation is used in the 1980 book Méthodes de programmation.

Memory Model

Explores the formalization of memory models and their crucial role in program optimization.

Kernel Integrity and Real-Time Systems

Explores kernel integrity, system security, and real-time system verification, emphasizing the importance of proving critical properties for building secure and timely systems.

Formal Verification Course Introduction

Introduces the formal verification course by the instructor, who encourages students to enjoy writing proofs.

Verifying real-time systems goes beyond the verification of functional properties: it also requires the checking of real-time properties. This makes traditional contract-frameworks partially inept for

2014The hardware complexity of modern machines makes the design of adequate programming models crucial for jointly ensuring performance, portability, and productivity in high-performance computing (HPC).

Can we guess the destinations of attendees in a music festival from Bluetooth traces collected by 10 people with smartphones used as antennas? This project analyzes an existing dataset of Bluetooth tr

2013