Coursera

System Validation (3): Requirements by modal formulas (Coursera)

Offered by EIT Digital,
System Validation (3): Requirements by modal formulas (Coursera)

System Validation is the field that studies the fundamentals of system communication and information processing. It allows automated analysis based on behavioural models of a system to see if a system works correctly. We want to guarantee that the systems does exactly what it is supposed to do. The techniques put forward in system validation allow to prove the absence of errors. It allows to design embedded system behaviour that is structurally sound and as a side effect enforces you to make the behaviour simple and insightful. This means that the systems are not only behaving correctly, but are also much easier to maintain and adapt.

Class Deals by MOOC List - Click here and see Coursera's Active Discounts, Deals, and Promo Codes.

’Requirements by modal formulas' is the third course that shows you how to specify requirements for the automata in order to establish the correct relation between the requirements and the behaviour of the system.
Reading material: J.F. Groote and M.R. Mousavi. Modeling and analysis of communicating systems. The MIT Press, 2014.

Syllabus

WEEK 1
Basic modal formulas
In this module you learn how to specify requirements on behaviour. First Hennessy-Milner logic is explained, which is subsequently extended with fixed-points. Using this logic you will be able to formally characterise virtually any behavioral property on the behavior of software. This varies from simple properties such as a system is free from deadlocks, to complex properties such as "in a warehouse the controllers will instruct all the robots such that my ordered item will appear for certain within finite time at the output".

WEEK 2
Advanced modal formulas
This module elaborates on modal formulas. It shows how to use data in the formulas which makes modelling of complex properties much easier. Furthermore, it shows how fairness properties can be modelled in the framework using nested fixed point operators. The last lectures introduce parameterised boolean equation systems and boolean equation systems as important technology to establish that a modal formula is valid for a particular specified behaviour.

Go to Class
MOOC List is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

Related Courses

An Introduction to Interactive Programming in Python (Part 2) (Coursera) Coursera
Rice University

An Introduction to Interactive Programming in Python (Part 2) (Coursera)

CS: Software Engineering CS: Programming

This two-part course is designed to help students with very little or no computing background learn the basics of building simple interactive applications. Our language of choice, Python, is an easy-to learn, high-level computer language that is used in many of the computational courses offered on Coursera. To make learning Python easy, we have developed a new browser-based programming environment that makes developing interactive applications in Python simple.

Jun 15th 2026
4 Weeks
Game Programming Python
Details
System Validation (Canvas Network) Canvas Network
Halmstad University

System Validation (Canvas Network)

Security & Networking

Anyone who has ever designed an embedded system or a communication protocol involving several components executing simultaneously knows that such software is inherently susceptible to bugs. Typical problems include race conditions, deadlocks, and unexpected interplay between different components. The parallel nature of these systems makes it notoriously hard to detect such bugs using testing (timing, e.g., plays a crucial role). This course is designed to provide an introduction to the problems that arise in the design of such systems. It provides ways to model such systems and reason about them.

Self Paced
Self-Paced
Embedded Systems System Validation
Details
Java for Android (Coursera) Coursera
Vanderbilt University

Java for Android (Coursera)

CS: Software Engineering CS: Programming

This MOOC teaches you how to program core features and classes from the Java programming language that are used in Android, which is the dominant platform for developing and deploying mobile device apps. In particular, this MOOC covers key Java programming language features that control the flow of execution through an app (such as Java’s various looping constructs and conditional statements), enable access to structured data (such as Java's built-in arrays and common classes in the Java Collections Framework, such as ArrayList and HashMap), group related operations and data into classes and interfaces (such as Java's primitive and user-defined types, fields, methods, generic parameters, and exceptions), customize the behavior of existing classes via inheritance and polymorphism (such as subclassing and overriding virtual methods).

Jun 16th 2026
4 Weeks
Programming Java Android
Details
Python Data Structures (Coursera) Coursera
University of Michigan

Python Data Structures (Coursera)

CS: Software Engineering CS: Programming

This course will introduce the core data structures of the Python programming language. We will move past the basics of procedural programming and explore how we can use the Python built-in data structures such as lists, dictionaries, and tuples to perform increasingly complex data analysis. This course will cover Chapters 6-10 of the textbook “Python for Everybody”. This course covers Python 3.

Jun 15th 2026
5-12 Weeks
Programming Python Semantics
Details
Advanced Algorithms and Complexity (Coursera) Coursera
University of California, San Diego,Higher School of Economics - HSE University

Advanced Algorithms and Complexity (Coursera)

CS: Software Engineering CS: Theory

You've learned the basic algorithms now and are ready to step into the area of more complex problems and algorithms to solve them. Advanced algorithms build upon basic ones and use new ideas. We will start with networks flows which are used in more typical applications such as optimal matchings, finding disjoint paths and flight scheduling as well as more surprising ones like image segmentation in computer vision.

Jun 15th 2026
5-12 Weeks
Algorithms Data Structures Machine Learning
Details
Introduction to Web Development (Coursera) Coursera
University of California, Davis

Introduction to Web Development (Coursera)

CS: Software Engineering CS: Programming

This course is designed to start you on a path toward future studies in web development and design, no matter how little experience or technical knowledge you currently have. The web is a very big place, and if you are the typical internet user, you probably visit several websites every day, whether for business, entertainment or education. But have you ever wondered how these websites actually work? How are they built? How do browsers, computers, and mobile devices interact with the web? What skills are necessary to build a website? With almost 1 billion websites now on the internet, the answers to these questions could be your first step toward a better understanding of the internet and developing a new set of internet skills.

Jun 15th 2026
5-12 Weeks
Programming HTML Javascript
Details
Cloud Computing Concepts: Part 2 (Coursera) Coursera
University of Illinois at Urbana-Champaign

Cloud Computing Concepts: Part 2 (Coursera)

CS: Software Engineering CS: Theory

Cloud computing systems today, whether open-source or used inside companies, are built using a common set of core techniques, algorithms, and design philosophies—all centered around distributed systems. Learn about such fundamental distributed computing "concepts" for cloud computing. Some of these concepts include: Clouds, MapReduce, key-value stores, Classical precursors, Widely-used algorithms, Classical algorithms, Scalability, Trending areas, And more!

Jun 15th 2026
5-12 Weeks
Programming Cloud Algorithms
Details
Java Programming: Arrays, Lists, and Structured Data (Coursera) Coursera
Duke University

Java Programming: Arrays, Lists, and Structured Data (Coursera)

CS: Software Engineering CS: Programming

Build on the software engineering skills you learned in “Java Programming: Solving Problems with Software” by learning new data structures. Use these data structures to build more complex programs that use Java’s object-oriented features. At the end of the course you will write an encryption program and a program to break your encryption algorithm.

Jun 15th 2026
4 Weeks
Programming Java Cryptography
Details
System Validation: Automata and behavioural equivalences (Coursera) Coursera
EIT Digital

System Validation: Automata and behavioural equivalences (Coursera)

CS: Design & Product

Have you ever experienced software systems failing? Websites crash, calendar not synchronising, or even a power blackout. Of course you have! But did you know that many of these errors are the result of communication errors either within a system or between systems? Depending on the system, the impact of software failures can be huge, even resulting in massive economic damage or loss of lives. Software, and in particular the communication between software-intensive systems, is very complex and very difficult to get right. However, we _need_ dependability in the systems we use, directly or indirectly, to support us in our everyday lives.

Jun 1st 2026
3 Weeks
Automata Embedded Systems System Validation
Details