Formal specification

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. 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 predict

About this result

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 (41)

Related publications

Related people

Related units

Related concepts (15)

Related concepts

Related courses (12)

Related courses

Related lectures (18)

Related lectures

Pedestrian Destinations in Paléo Music Festival from Bluetooth Traces

Elisaveta Kondratieva

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 traces from Paléo music festival in Nyon, Switzerland. The goal of the project is to follow Paléo festival attendees using collected Bluetooth traces and analyze specifications of the collected data in terms of precision and results, to predict attendees behaviour and crowd movement. The data was collected on July 24th, 2010 by ten agents scanning for visible Bluetooth devices. The methodology for tracing Paléo festival attendees is a Bayesian approach derived by Danalet et al. [2012].

2013

Decentralized in-order execution of a sequential task-based code for shared-memory architectures

Charly Nicolas Lucien Castes

The 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). Sequential task-based programming models paired with advanced runtime systems allow the programmer to write a sequential algorithm independently of the hardware architecture in a productive and portable manner, and let a third party software layer -the runtime system- deal with the burden of scheduling a correct, parallel execution of that algorithm to ensure performance. Many HPC algorithms have successfully been implemented following this paradigm, as a testimony of its effectiveness. Developing algorithms that specifically require fine-grained tasks along this model is still considered prohibitive, however, due to per-task management overhead [1], forcing the programmer to resort to a less abstract, and hence more complex "task+X" model. We thus investigate the possibility to offer a tailored execution model, trading dynamic mapping for efficiency by using a decentralized, conservative in-order execution of the task flow, while preserving the benefits of relying on the sequential taskbased programming model. We propose a formal specification of the execution model as well as a prototype implementation, which we assess on a shared-memory multicore architecture with several synthetic workloads. The results show that under the condition of a proper task mapping supplied by the programmer, the pressure on the runtime system is significantly reduced and the execution of fine-grained task flows is much more efficient.

IEEE COMPUTER SOC2022

Contracts for Real-Time, Safety Critical Systems

Chandrakana Nandi

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 checking real-time programs. This is a major problem because the failure of real-time and safety critical systems can have serious consequences. This thesis presents a solution to this problem by incorporating Design by Contract (annotating programs with function pre and post conditions) to such systems. The main contribution of this thesis is the development of a contract framework for cyclic real-time control applications written in C++. The contract framework allows the users to specify both functional and temporal properties for the applications. A novel approach of empirical cumulative distribution function (cdf ) based statistical inference is used for dynamically estimating temporal constraints and incorporating them in future contracts. The thesis also illustrates the use of Real-time Logic (RTL) for formal specification of the temporal properties. For evaluating our methodology, we have integrated it to a component-based framework called FASA (Future Automation System Architecture) developed at ABB Corporate Research for writing hard real time control applications. Experiments show that this contract framework can be smoothly integrated to existing control applications thereby increasing their reliability while having a acceptable overhead (less than 10%) on the performance.

2014

Formal methods

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 f

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal sp

Programming language

A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer

CS-322: Introduction to database systems

This course provides a deep understanding of the concepts behind data management systems. It covers fundamental data management topics such as system architecture, data models, query processing and optimization, database design, storage organization, and transaction management.

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into the new web standard for portable binaries called WebAssembly ( https://webassembly.org/ )

CH-353: Introduction to electronic structure methods

Repetition of the basic concepts of quantum mechanics and main numerical algorithms used for practical implementions. Basic principles of electronic structure methods:Hartree-Fock, many body perturbation theory, configuration interaction, coupled-cluster theory, density functional theory.