8 EIN. / ECTS

The focus of this course is on modeling and model checking reactive and concurrent systems, with a formal basis as well as a practical point of view. We start with formal semantics of concurrent models as basic transition systems presented by Manna and Pnueli. Then we introduce model checking and temporal logics of LTL and CTL using Huth and Ryan book. The actor‐based language Rebeca and the coordination language Reo and their formal semantics will be covered next. We will also study Petri Nets. While introducing the models we will also look at the verification tools which support them. We will work with the widely used model checkers of NuSMVand Spin and also supporting tools of Rebeca and Reo. A proper medium‐size case study shall be selected and studied by the students and then modeled and model checked by one of the languages and tools which are introduced in the course. Model checking algorithms and temporal logic are not fully covered in this course.

Undanfarar
Engir undanfarar.

Hæfniviðmið
On completion of the course students should: • Be able to build the transition system as semantics of a given concurrent model • Be able to understand the meaning of an LTL and CTL formula and write the properties of a model using LTL and CTL (as property languages for model checking) • Be able to build simple to medium‐size models using Petri nets, coordination lanaguage Reo and actor‐based language Rebeca • Be able to build models and model check their models using NuSMV and Spin model checkers (not an expert in) • Be able to find their way in choosing a proper modeling language and analysis method for their application (not necessarily the best one!).

Námsmat
Final exam (30%) The grade 50/100 is needed in the exam to pass the course. Particpation (10%) Active participation in class and discussions. Homework assignments (15%) Manna assignments (8 points), Huth assignments (3 points), Reo assignments (2 points), Petri net assignments (2 points) Late returns = 10% penalty for each day. Class projects (20%) NuSMV and Spin (10 points) - Reo, Rebeca, Petri net (10 points) Late returns = 10% penalty for each day. Final project (25%) You choose a medium-size application as your case study and then model it and verify it. The deliverables are: • a progress report as a formal presentation, including an explanation of the selected case study and the modeling language you decide to use (5 point) • modeling and verifying the case study (10 points) • a final report (10 points).

Kennsluaðferðir
Week 1: Introduction to the course ‐ Manna: Chapter 1: 1.1, 1.2 Assignment: ‐‐‐ Project: Work with SMV – Code Binomial Coefficient in SMV Week 2: Manna 1.3, 1.4, 1.5 – Introduction to Rebeca Assignment: Manna problems 1.1, 1.2 Project: Code Greatest Common Divisor by SMV Week 3: Manna 1.6, 1.7 Assignment: Manna problem 1.3 Project: Work with Spin Week 4: Manna 1.8, 1.9, 1.10 Assignment: Manna problems 1.4, 1.5, 1.6, 1.7 Project: Code Bin and GCD by Spin Week 5: Huth: Chapter 3: 3.1‐3.2, pp. 172‐187 Assignment: Huth (3.2) 1 (a,c,d) , 2, (3.3) 1 (a,b), 3 Project: Verify the properties of your codes + more codes Week 6: Huth 3.3‐3.4, pp. 187‐217 Assignment: Huth (3.4) 2, 3 (a, c, d, e), 5, 6, 8, 10 (a, d), 11(b) (3.5) 1 (b, c, d), 4 Project: Verify the properties of your codes Week 7: Reo: The Coordination Language + its semantics: Constraint Automata Assignment: CA for some Reo Circuits Project: Look for applications/case studies as the final project of the course Week 8: More on Rebeca and Reo: applications, tools Assignment: ‐‐‐ Project: Look into Afra and Reo tools http://khorshid.ece.ut.ac.ir/~rebeca/Tools.htm http://reo.project.cwi.nl/cgi-bin/trac.cgi/reo/wiki/Tools Week 9: Manna 1.11 Petri net Assignment: Manna problem 1.9 Project: Petri net tools http://www.informatik.uni‐hamburg.de/TGI/PetriNets/tools/db.html Week 10: Wil van der Aalst slides on Petri net Assignment: exercises form slides Project: work with Petri net tools Week 11: Discussions on the final project Assignment: ‐‐‐ Project: final project Week 12: Discussions on the final project Assignment: ‐‐‐ Project: final project.

Kennari
Marjan Sirjani

Tungumál
Enska

SKRÁNING HÉR

Forföll og innheimta

FagMennt áskilur sér rétt til þess að rukka 10.000 króna skráningar og umsýslugjald ef þátttakandi skráir sig úr námskeiði innan viku áður en námskeið hefst. Nauðsynlegt er að skrá sig úr námskeiði a.m.k. 2 dögum fyrir námskeið. Að öðrum kosti áskilur FagMennt sér rétt til þess innheimta fullt námskeiðsgjald.
Sjá greiðsluskilmála

Nánari upplýsingar

Bryndís Bjarnadóttir
Verkefnastjóri hjá Opna háskólanum
bryndisb@hr.is
Sími 599-6387