mislo

Fakulteta za elektrotehniko, računalništvo in informatiko · Univerza v Mariboru

Formalne metode pri načrtovanju sistemov

Za Formalne metode pri načrtovanju sistemov še ni zapiskov.

Imaš svoje zapiske? Objavi jih: ceno določiš ti, z naročnino ti ostane cela, DDV se doda kupcu.

Objavi zapiske

Čakaš na zapiske? Prijavi se in povej. Ko jih kdo objavi, dobiš sporočilo.

Želim zapiske

Kaj lahko narediš že danes

Naloži svoje gradivo za Formalne metode pri načrtovanju sistemov: Mai ga prebere in ti iz njega naredi kartice, kviz in razlago, ko ti kaj ni jasno. Če zapiske kasneje objaviš, jih prodajaš tukaj.

Naloži svoje gradivo

Učni načrt

Podatki so iz učnega načrta, ki ga objavlja Fakulteta za elektrotehniko, računalništvo in informatiko. Prebrano 6. 9. 2026. Poglej izvirnik

6 kreditnih točk

Obveznosti v urah

  • Predavanja60 ur
  • Samostojno delo120 ur

Vsebina

  1. Uvod: analiza vzrokov za napake v znanih sistemih, definicija formalnih metod, vpeljava formalnih metod v razvojni cikel izdelka, področja uporabe formalnih metod, primeri uspešne uporabe formalnih metod.
  2. Modeliranje sistemov: sistemi prehajanja stanj, Kripkejevi modeli, opisni jeziki za Kripkejeve modele (SMV, Promela), lastnosti sistemov prehajanja stanj (varnost, živost, poštenost).
  3. Temporalne logike: logika drevesa izvajanj -CTL, linearna temporalna logika -LTL.
  4. Verifikacijske tehnike in orodja: preverjanje modelov, dokazovanje izrekov.
  5. Simbolično preverjanje modelov: predstavitev boolovih funkcij z binarnimi odločitvenimi grafi (BDD-ji), algoritmi za simbolično preiskovanje prostora stanj, orodja za preverjanje modelov (Spin in SpinRCP).
  6. Sodobni trendi in smeri nadaljnjega razvoja: nadaljnje raziskave temeljnih konceptov, razvoj učinkovitih in uporabniku prijaznih metod in orodij, integracija metod preverjanja modelov in dokazovanja izrekov, integracija formalnih in neformalnih tehnik.

Ocenjevanje

Projekt 50 %, Ustni izpit 50 %

Pogoji za vključitev

Pogojev ni.

Literatura

  • R. Sebastiani: Introduction to Formal Methods, University of Trento, Italy, 2013. Vir je dostopen v elektronski obliki na naslovu http://disi.unitn.it/~rseba/DIDATTICA/fm2020/.
  • C. Baier, J.-P. Katoen: Principles of Model Checking, MIT Press, Cambridge, 2008.
  • M. Ben-Ari, Principles of the Spin Model Checker, Springer, London, 2008.
  • G. J. Holzmann, The SPIN Model Checker - Primer and Reference Manual, Addison Wesley, Boston, 2003.
  • Z. Brezočnik, T. Kovše: SpinRCP – An Integrated Development Environment for the Spin Model Checker. Orodje je dostopno na naslovu http://lms.uni-mb.si/spinrcp/

Kako deluje

  1. Zapiske kupiš enkrat in ostanejo tvoji.
  2. V aplikaciji iz njih dobiš kartice, kvize in Mai, ki pozna gradivo.
  3. Ceno določi avtor. Prodajalec je Mislo AI, račun dobiš od nas.