Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Software Disasters and Successes: Verification Impact and Transition Systems

Description

This lecture covers the impact of software verification through examples of disasters like the Ariane 5 rocket explosion and successes such as Airbus control software verification. It introduces transition systems, explaining states, transition relations, and reachability checking algorithms.

Official source

Ontological neighbourhood

Theoretical computer science

Theory of computation: Automata theory

Related concepts (24)

Finite-state machine

A finite-state machine (FSM) or finite-state automaton (FSA, plural: automata), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time. The FSM can change from one state to another in response to some inputs; the change from one state to another is called a transition. An FSM is defined by a list of its states, its initial state, and the inputs that trigger each transition.

Finite-state transducer

A finite-state transducer (FST) is a finite-state machine with two memory tapes, following the terminology for Turing machines: an input tape and an output tape. This contrasts with an ordinary finite-state automaton, which has a single tape. An FST is a type of finite-state automaton (FSA) that maps between two sets of symbols. An FST is more general than an FSA. An FSA defines a formal language by defining a set of accepted strings, while an FST defines relations between sets of strings.

Deterministic finite automaton

In the theory of computation, a branch of theoretical computer science, a deterministic finite automaton (DFA)—also known as deterministic finite acceptor (DFA), deterministic finite-state machine (DFSM), or deterministic finite-state automaton (DFSA)—is a finite-state machine that accepts or rejects a given string of symbols, by running through a state sequence uniquely determined by the string. Deterministic refers to the uniqueness of the computation run.

Nondeterministic finite automaton

In automata theory, a finite-state machine is called a deterministic finite automaton (DFA), if each of its transitions is uniquely determined by its source state and input symbol, and reading an input symbol is required for each state transition. A nondeterministic finite automaton (NFA), or nondeterministic finite-state machine, does not need to obey these restrictions. In particular, every DFA is also an NFA. Sometimes the term NFA is used in a narrower sense, referring to an NFA that is not a DFA, but not in this article.

Disaster

A disaster is a serious problem occurring over a period of time that causes widespread human, material, economic or environmental loss which exceeds the ability of the affected community or society to cope using its own resources. Disasters are routinely divided into either "natural disasters" caused by natural hazards or "human-instigated disasters" caused from anthropogenic hazards. However, in modern times, the divide between natural, human-made and human-accelerated disasters is difficult to draw.

Related lectures (30)

Disasters, Successes, and Inductive Invariants

Explores software disasters, successful verifications, transition systems, and invariants in systems.

Finite Automata: Basics

Introduces the basics of finite automata, including deterministic and non-deterministic types, regular expressions, and acceptance criteria.

Regular Expressions (Recap)

Covers the fundamentals of regular expressions and includes exercises on defining languages.

Universal Source Coding

Covers the Lempel-Ziv universal coding algorithm and invertible finite state machines in information theory.

Regular Expressions to Automata