Publication

A Formal Specification for a Real-Time Train Controller

2001
Student Projects

Abstract

We give a formal specification for a real-time controller for trains that operate on the Italian railway network. The controller will control train movements and is part of a larger system destined to guarantee safety with respect to dangers originating from train traffic in the railway network. Based on an informal specification document from the Italian railway company, we construct a simple state-based model and formalise it in terms of the property-based specification language TRIO. The obtained specification being formal, we are able to perform certain verifications on it, such as checking its satisfiability and verifying correctness of refinement steps.

Official source

https://infoscience.epfl.ch/entities/publication/5a4e8184-854b-4042-92e5-e25dbe3e6868

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.

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

2001
Student Projects

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/5a4e8184-854b-4042-92e5-e25dbe3e6868

About this result

Related concepts (26)

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.

Specification (technical standard)

A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard. There are different types of technical or engineering specifications (specs), and the term is used differently in different technical contexts. They often refer to particular documents, and/or particular information within them. The word specification is broadly defined as "to state explicitly or in detail" or "to be specific".

Game controller

A game controller, gaming controller, or simply controller, is an input device or input/output device used with video games or entertainment systems to provide input to a video game. Input devices that have been classified as game controllers include keyboards, mouses, gamepads, and joysticks, as well as special purpose devices, such as steering wheels for driving games and light guns for shooting games. Controllers designs have evolved to include directional pads, multiple buttons, analog sticks, joysticks, motion detection, touch screens and a plethora of other features.