Quality assurance - Catching bugs by formal verification
Please note that applications are closed for this course for the duration of autumn semester 2020.
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.
- 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
At the end of the course any participant should be able to:
- Understand the differences between algorithmic and deductive verification
- Formalise requirements in temporal logic or predicate logic
- Model functional and timing behavior of reactive systems
- Apply formal verification tools (such as UPPAAL and variants) to check properties of models
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
- 120 credits, of which 80 credits in engineering or informatics, including at least 30 credits in computer science or software development.
- In addition, English course A/English course 6 is required.
You can also apply for the course and get your eligibility evaluated based on knowledge acquired in other ways, such as work experience, other studies etc.
Course title in Swedish
Kvalitetssäkring - Upptäcka fel genom formell verifiering
After submitting your electronic application, the next step is to submit documentation to demonstrate your eligibility for the course you have applied for. In order to document your eligibility, you must provide your high school diploma and university transcript and proof of your English language proficiency.
To meet the entry requirements for this course you need to have previous academic qualifications (university studies). You will find the specific entry requirements above.
No academic qualifications?
If you do not have the formal academic qualifications needed for a specific course, you can apply for the course and get your eligibility evaluated based on knowledge acquired in other ways, such as work experience, other studies etc. This is also known as a validation of prior learning.
Recognition of prior learning means the mapping out and assessment of an individual's competence and qualifications, regardless how, where or when they were acquired – in the formal education system or in some other way in Sweden or abroad, just recently or a long time ago.
If you think your knowledge and competences will qualify you for this course, you will need to upload th following with your application:
- CV with description of your educational and professional background. Your CV must describe your knowledge and competences in relation to the entry requirements.
- If you refer to work experience, you need to upload an Employers certificate.
If we need more information, we will contact you.
The courses are part of the Prompt project where MDH offers courses at master's level. The courses are given online without physical meetings and are flexible in time and space so that they can be combined with professional life.For companies that want to collaborate on competence development