This repository comprises material collected and constructed during the course System Validation and Testing (Formal Verification), as taught at Open Universiteit as part of my Master of Software Engineering.
This repository comprises material collected and constructed during the course System Validation and Testing (Formal Verification), as taught at Open Universiteit as part of my Master of Software Engineering.
The following books, scientific articles and other references where used and are being referred to from other parts in this repository.
| Article/Book | Authors | Comments |
|---|---|---|
| Timed Automata | Alur | A survey of the theory of timed automata, 2003 |
| A theory of timed automata | Alur, Dill | |
| Model Checking | Clarke | Textbook used in the course |
| Model-Checking for Real-Time Systems | Larsen, Pettersson, Yi | Creators of UPPAAL, 2005 |
| An introduction to timed automata | Patricia Bouyer | Presentation |
| Model Checking Real-Time Systems - Patricia Bouyer | Patricia Bouyer, Uli Fahrenberg, Kim Larsen, Nicolas Markey, Joël Ouaknine, James Worrell | Article on which the presentation An introduction to timed automata was based |
| An introduction to bisimulation and coinduction | Davide Sangiorgi | jkjkj |
| UPPAAL Tutorial | UPPAAL | Contains a summary of timed automata |
| Youtube CTL* video | Model Checking | Good visual explanation of the concepts of CTL* |
| Youtube CTL video | Model Checking | Good visual explanation of the concepts of CTL |
| Logic in computer science | M. Huth & M. Ryan | Book about logic-based verification |
| Fairness in CTL | JP. Katoen | Presentation of a lecture on fairness in relation to LTL and CTL |
| Model Checking with Strong Fairness | Y. Kesten et al. | A coherent framework for symbolic model checking of linear-time temporal logic ( LTL ) properties over finite state reactive systems, taking full fairness constraints into consideration |
| Model Based Testing with Labelled Transition Systems | J. Tretmans | Academic paper that describes a model based testing theory where models are expressed as labelled transition systems, and compliance is defined with the ‘ioco’ implementation relation |
I’ve maintained notes of my study progress for myself and for other people interested. These notes could be used to improve the setup of the course or to change certain text books and/or articles.
| Date | Note |
|---|---|
| 09/15/2019 | Started with Clarke’s Model Checking, finished chapter 1 |
| 09/20/2019 | Finished chapter 2 of Model Checking |
| 09/25/2019 | Chapter 17 of Clarke’s Model Checking raised some doubts regarding relationship between states and locations. Used the references in the book and decided to read A theory of timed automata first. Also Model-Checking for Real-Time Systems by the creators of UPPAAL seems to be a good reference regarding timed automata |
| 09/26/2019 | Video about overview of timed transition systems and a demo about UPPAAL: https://www.youtube.com/watch?v=tUSxi_rSXwo |
| 09/27/2019 | A theory of timed automata mentions that timed automata must be able to accept ω-regular languages. This video explains a bit about Buchi automata (one form of ω-automata): https://www.youtube.com/watch?v=KOu6IUssxbs. The concept of ω-automata is important in the light of model-checking as it introduces the problem of infinite runs |
| 09/28/2019 | A theory of timed automata read until paragraph 3.5 |
| 10/03/2019 | An introduction to timed automata, presentation by Patricia Bouyer explains well the concepts, especially region equivalence and relation between locations in timed automata and states in state transitions diagrams. Also based on the paper Model Checking Real-Time Systems - Patricia Bouyer |
| 10/04/2019 | Model Checking mentions bisimulation, but chapter 11 of that book doesn’t explain quiet clearly the concept. Found another reference: An introduction to bisimulation and coinduction by Davide Sangiorgi |
| 10/04/2019 | Started reading An introduction to bisimulation and coinduction by Davide Sangiorgi to get more acquinted with LTS equivalence and the concept of bisimulation. These terms are prerequisites in order to continue with Model Checking |
| 10/05/2019 | After reading An introduction to bisimulation and coinduction the notion of bisimularition is understood |
| 10/11/2019 | Reading UPPAAL Tutorial. Reachability, safety and liveness are mentioned in section 2.2 as important subjects. Started reading Timed Automata to get more information regarding reachability |
| 10/12/2019 | Reading UPPAAL Tutorial again, section 2.3 and chapter 7 about patterns |
| 11/6/2019 | Started reading chapter 3 in the textbook Model Checking. Used the Youtube CTL* video and Youtube CTL video to get more clarification about CTL and CTL* |
| 11/6/2019 | Read Logic in computer science, paragraph 3.6. Algorithms for model checking are given in this paragraph. Special attention to paragraph 3.6.2 which explains well the concept of fairness |
| 11/17/2019 | Finished reading Logic in computer science, chapter 3 excluding 3.7. |
| 01/01/2020 | Finished reading Model Based Testing with Labelled Transition Systems, until paragraph 3.4, input & outputs |
| 01/02/2020 | Finished reading Model Based Testing with Labelled Transition Systems, until paragraph 4.1 |
| 01/02/2020 | Finished reading Model Based Testing with Labelled Transition Systems, paragraph 4. |