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 2023
• Semestr: zimní
• E-Kredity: 5
• Rozsah, examinace: zimní s.:2/2, Z+Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• 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. RNDr. Pavel Parízek, Ph.D.
• Vyučující: doc. RNDr. Pavel Parízek, Ph.D.
• Třída: Informatika Mgr. - volitelný
• Kategorizace předmětu: Informatika > Softwarové inženýrství, Teoretická informatika

Anotace

čeština

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. Předpokládají se znalosti v rozsahu předmětu NSWI041 - Úvod do softwarového inženýrství.

Poslední úprava: Kopecký Michal, RNDr., Ph.D. (26.04.2019)

angličtina

The role of formal specification and models in software engineering. Overview of selected methods and tools for formal description of system architecture and behavior. Examples of their usage especially in the design and validation. Knowledge in extent of NSWI041 - Introduction to Software Engineering - is supposed.

Poslední úprava: Kopecký Michal, RNDr., Ph.D. (26.04.2019)

Literatura

čeština

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.

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

Sylabus

čeština

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.

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

angličtina

1. The role of formal specifications and models in software engineering, their benefits and limitations.

2. Algebraic methods, many-sorted algebras, initial models.

3. Rewriting systems, OBJ3, Maude.

4. Model oriented methods.

5. Z language and its extensions (Objective-Z).

6. VDM method and its extensions (VDM++).

7. Introduction to Alloy language.

8. Formal foundations of UML.

9. Specification language OCL.

10. Petri nets and CPN.

11. Temporal logic. Dynamic logic.

12. Domain-specific languages.

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