Mètodes Formals en l'Enginyeria del Software (MFES)
| Professors Responsables: |
M. PILAR NIVELA ALOS (nivela lsi.upc.edu)
|
|
Crèdits: 4.5 (3.0 T 1.5 P 0.0 L)
| |
Departament:
LSI
|
Tipus d'assignatura
Optativa per la EI
Requisits de l'assignatura
|
ES:E
- Pre-requisit per la EI
|
|
Objectius docents
Proporcionar els coneixements matemàtics bàsics dels
mètodes formals: semàntica dels llenguatges d'especificació
i sistemes lògics d'inferència
Conèixer els mètodes per demostrar propietats del software
automàtica i semi-automàticament a partir de l'especificació
Programa
1. Introducció (Durada: 1
setmana)
-Què és un mètode formal: llenguatges formals
d'especificació; validació i correctesa; execució de
prototipus; metodología de desenvolupament (refinaments successius, transformacions, síntesi)
-Tipus de mètodes formals: mètodes orientats a models (VDM, Z) i mètodes axiomàtics (Larch)
2. Mètodes formals axiomàtics
(Durada: 5 setmanes)
-Llenguatges d'especificació axiomàtica: semàntica inicial i laxa
-Operacions d'estructuració
-La família de llenguatges Larch
3. Demostraciò automàtica i semi-automàtica
(Durada: 9 setmanes)
-Deducció equacional i reescriptura: terminació; confluència;
compleció de Knuth-Bendix
-LP: el demostrador de Larch
-Deducció amb clausules generals: resolució; paramodulació
saturació
Avaluació
La nota final serà 3/5 de la nota de teoria i 2/5 de la nota de problemes.
Per a fer promig, cal obtenir al menys un 4 a cadascuna de les parts
Càrrega
Els 4.5 crèdits de l'assignatura es descomposen en 3 de teoria i 1.5
de problemes
Degut a que una part del contingut de l'assignatura ès teòric i
que no hi ha laboratori es recomana a l'alumne fer pràctiques amb
Larch per tal de facilitar la comprensiò dels conceptes desenvolupats a
classe.
Bibliografia
Bibliografia bàsica
- Dershowitz, N., Jouannaud, J.P. Rewrite Systems. Handbook of Theoretical Computer Science, Vol B J. van Leeuwen (Ed.), Elsevier, 1990, pp. 243-320
- Ehrig, H., Mahr, B. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics Springer Verlag, 1985
- Guttag, J.V., Horning, J.J. Larch: Languages and Tools for Formal Specification Springer Verlag, 1993
Bibliografia complementària
-
Bicarregui, J.C., Fitgerald, J.S., Lindsay, P.A., Moore, R.C., Ritchie, B.
Proof in VDM: A Practitioner's Guide Springer Verlag, 1993
- Hall, A. Seven Myths
on Formal Methods IEEE Software, September 1990
- Hayes, I.J. Specification Case Studies
Prentice Hall, 1987
- Hinchey, M.G., Bowen, J.P. (Eds.) Applications of Formal
Methods Prentice Hall, 1995
- Hoffmann, B., Krieg-Br¨ckner, B. (Eds.)
Program Development by
Specification and Transformation: The Prospectra Methodology,
Language Family and System Springer Verlag, Lecture Notes in Computer Science, 680
, 1993
- Jones, C.B. Systematic Software Development using VDM Prentice
Hall, 1990
- Jones, C.B., Shaw, R.C. Case Studies in Systematic Software
Development Prentice Hall, 1990
- Turski, W.M., Maibaum, T.S.E. The Specification
of Computer Programs Addison Wesley, 1987
- Sannella, D. A Survey of Formal Software Development Methods,Software Engineering: A Europea Thayer R.H., McGettrick, A.D. (Eds.), IEEE Computer Society Press Tutorial, 1992, pp. 281-297
- Spivey, J.M. The Z Notation Prentice Hall, 1990
- Wirsing, M. Algebraic Specification,Handbook of Theoretical Computer Science, Vol B: Formal J. van Leeuwen (Ed.), Elsevier, 1990, pp. 675-788
|
