Quality assurance - Catching bugs by formal verification
Mälardalen University
Startdatum:
Slutdatum:
Studietakt: 25 %
Publicerad utbildningskatalog
Quality assurance - Catching bugs by formal verification
Utbildningsinformation från den publicerade källan. Utbildningen och dess tidsbundna tillfällen hålls åtskilda.
Utbildningsfakta
Kod: DVA468
The aim of the course is to introduce the participants into methods and tools for verifying systems that need to react to external stimuli. The methods use system models with precise formal semantics and will span model-checking as well as deductive verification. A set of simple examples as well as real-world applications will be used throughout the course to illustrate the methods and their tool support. The objective of the course is to understand the underpinning theories of formal verification, and learn how to apply tool support in order to verify system models. About this course This course consists of lectures and assignments that will teach the participants the basics of formal verification, differences between techniques, as well as their potential applicability to real-world systems. The course will cover both discrete as well as timed systems, and will show the application of techniques on some prototype examples from industry. Course modules: * Basic concepts of formal modeling: automata models, formalisation of system properties * Automated verification of formal models: model-checking, deductive verification * Application of tools to formal models and code Related industrial challenges addressed in the course * Uncover at early design stages potential trouble-spots/errors in design * Provide design-space exploration automated support * Increase assurance of future implementations
Behörighet
120 credits, of which 80 credits in engineering or informatics, including at least 30 credits in computer science or software development. In addition, Swedish course B/Swedish course 3 and English course A/English course 6 are required. For courses given entirely in English, exemption is made from the requirement in Swedish course B/Swedish course 3.
Utbildningstillfällen
Varje tillfälle har egna datum och villkor. Avslutade tillfällen behålls som historik och innebär inte att en ny ansökan är öppen.
Källa och uppdatering
Hämtad: .
Publicerad: .
Visa källversion
Publiceringsversion: 8e217193-f5fa-4778-b085-a4521fd03e8d
Kontrollsumma: 1b0dc54c0fc8a359f83ba9dc8f9d468479ce432de4c03bce3b8b33dd67fe3f6c
Senast ändrad enligt källan: 2025-03-14T10:56:29