PředmětyPředměty(verze: 802)
Předmět, akademický rok 2016/2017
   Přihlásit přes CAS
Formální základy softwarového inženýrství - NTIN043
Anglický název: Formal Foundations of Software Engineering
Zajišťuje: Katedra softwarového inženýrství (32-KSI)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2015
Semestr: zimní
E-Kredity: 5
Rozsah, examinace: zimní s.:2/2 Z+Zk [hodiny/týden]
Počet míst: neomezen
Minimální obsazenost: neomezen
Stav předmětu: vyučován
Jazyk výuky: čeština, angličtina
Způsob výuky: prezenční
Další informace: http://d3s.mff.cuni.cz/teaching/ntin043
Garant: doc. Mgr. Martin Nečaský, Ph.D.
RNDr. Pavel Parízek, Ph.D.
Třída: Informatika Mgr. - volitelný
Kategorizace předmětu: Informatika > Softwarové inženýrství, Teoretická informatika
Prerekvizity : NSWI041
Anotace -
Poslední úprava: Tajemník Katedry (29.04.2015)

Role formálních specifikací a modelů v softwarovém inženýrství. Přehled vybraných metod a nástrojů pro formální popis architektury a chování systému. Ukázky jejich použití zejména ve fázích návrhu a validace.
Literatura -
Poslední úprava: Tajemník Katedry (29.04.2015)

I. Sommerville: Software Engineering. 8th ed., Pearson Education. ISBN 0-321-31379-8, 2007.

D. Bjorner et al.: Logics of Specification Languages. Springer, 2008.

J. Goguen et al.: Introducing OBJ3. SRI-CSL-88-9, SRI International, USA, 1988.

J.M. Spivey: The Z Notation: A Reference Manual. 2nd ed., Prentice Hall, 1992. http://spivey.oriel.ox.ac.uk/~mike/zrm/

C.B. Jones: Systematic Software Development using VDM. Prentice Hall, 1990.

K. Jensen: Coloured Petri Nets. Springer Verlag.

The Maude System: http://maude.cs.illinois.edu/w/index.php?title=The_Maude_System

David Bednárek: Materiály k předmětu TIN043. 2006.

Sylabus -
Poslední úprava: Tajemník Katedry (29.04.2015)

1. Úloha formálních specifikací a modelů v softwarovém inženýrství, jejich výhody a nevýhody.

2. Algebraické metody, vícedruhové algebry, iniciální modely.

3. Přepisovací systémy, OBJ3, Maude.

4. Modelově orientované metody.

5. Jazyk Z a vybrané nadstavby (Objective-Z).

6. Metoda VDM a její nadstavby (VDM++).

7. Úvod do jazyka Alloy.

8. Formální základy UML.

9. Specifikační jazyk OCL.

10. Petriho sítě a CPN.

11. Temporální logika. Dynamická logika.

12. Doménově specifické jazyky.

 
Univerzita Karlova | Informační systém UK