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

Lecture

Timing and Performance Analysis: Model Checking

Description

This lecture by the instructor from Aalborg University in Denmark covers timing and performance analysis using model checking, including tasks such as WCET analysis and schedulability analysis. It also discusses experimental results, multiple objective scheduling, and a case follow-up on the TERMA system.

Official source

Related concepts (32)

Model checking

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash). In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language.

Automata theory

Automata theory is the study of abstract machines and automata, as well as the computational problems that can be solved using them. It is a theory in theoretical computer science. The word automata comes from the Greek word αὐτόματος, which means "self-acting, self-willed, self-moving". An automaton (automata in plural) is an abstract self-propelled computing device which follows a predetermined sequence of operations automatically. An automaton with a finite number of states is called a Finite Automaton (FA) or Finite-State Machine (FSM).

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

Rate-monotonic scheduling

In computer science, rate-monotonic scheduling (RMS) is a priority assignment algorithm used in real-time operating systems (RTOS) with a static-priority scheduling class. The static priorities are assigned according to the cycle duration of the job, so a shorter cycle duration results in a higher job priority. These operating systems are generally preemptive and have deterministic guarantees with regard to response times. Rate monotonic analysis is used in conjunction with those systems to provide scheduling guarantees for a particular application.

Pareto efficiency

Pareto efficiency or Pareto optimality is a situation where no action or allocation is available that makes one individual better off without making another worse off. The concept is named after Vilfredo Pareto (1848–1923), Italian civil engineer and economist, who used the concept in his studies of economic efficiency and income distribution. The following three concepts are closely related: Given an initial situation, a Pareto improvement is a new situation where some agents will gain, and no agents will lose.

Related lectures (31)

Stochastic Hybrid Systems

Explores time-determinator model checking, U-Pool scheduling, worst-case execution time analysis, and statistical model checking for cyber-physical systems.

MicroC/OS-II: Real-Time Kernel Overview

Provides an overview of MicroC/OS-II, a real-time kernel with multitasking capabilities and deterministic functions, covering topics such as task management, kernel, and intertask communication.

Automated Testing: Fuzzing and Sanitization

Explores fuzzing, bug oracles, code reviews, and automated testing techniques, emphasizing the importance of sanitization in detecting faults.

Automated Reasoning: Formal Verification with LISA

Explores formal verification using the LISA proof assistant and the OCBSL Equivalence Checker.

Efficient Safety-Critical Systems