Bibliografía de la materia
Toda
la bibliografía de la materia
ordenada alfabéticamente (no está actualizada).
Bibliografía de la Unidad I, Unidad III
y Unidad IV dividida en Obligatoria y
Optativa. A su vez la
bibliografía Obligatoria está ordenada según el
tema específico. Sugerimos efectuar
las lecturas en el orden aquí indicado.
Bibliografía Obligatoria significa que las evaluaciones se
harán suponiendo que el
alumno ha leído dicho material.
- Abadi, M., Lamport, L., "An old-fashioned
recipe for real time", ACM Transactions on Programming Languages
and Systems, 16(4): 1543-1571, septiembre 1994.
- Abadi, M.,
Alpern, B., Apt, K., Francez, N., Katz, S., Lamport, L., Schneider, F.,
"Preserving liveness: comments on 'Safety and
liveness from a methodological point of view'", Information
Processing Letters 40(3): 141-142, noviembre 1991.
- Alpern, B., Schneider, F., "Defining liveness", Information
Processing Letters, 21(4): 181-185, octubre 1985.
- Alpern, B., Schneider, F., "Recognizing
safety and liveness. Distributed Computing", 2:117--126, 1987.
- Bhargavam, K., Gunter, C., Gunter, E., Jackson, M., Obradovic,
D., Zave, P.; "The Village Telephone
System: a Case Study in Formal Software Engineering"; 11th
International Conference on Theorem Proving in Higher Order Logics,
September 1998.
- Berry, D.M., Kamsties, E.; "The Dangerous
"All" in Specifications"; 10 International Workshop on Software
Specifications and Design, November 2000.
- Bowen, J., Hinchey, M., "Seven more myths
of formal methods", IEEE Software, 12(4):34-40, julio 1995.
- Brooks, F.P., "No silver bullet: essence and accidents of
software engineering", IEEE Computer, 20(4): 10-19, abril 1987.
Brooks, F.P.,
The Mytical Man-Month, Addison-Wesley, 1975.
- Clarke, E., Wing, J., "Formal methods:
state of the art and future directions", ACM Computing Surveys,
18(4):626-643, diciembre 1996.
- Ghezzi, C., Jazayeri, M. y Mandrioli, D., Fundamentals of
Software Engineering, Prentice Hall, Upper Saddle River, 1991.
- Gibbs, W.W., "La crisis crónica de
la programación", Investigación y Ciencia, 72-81,
noviembre 1994.
- Gunter, C., Gunter, E., Jackson, M., Zave, P.; "A reference model for requirements and
specifications", IEEE Software, 17(3): 37-43, mayo 2000.
- Harel, D., "Statecharts: a visual formalism
for complex systems", Science of Computer Programming, 8(1987):
231-274, 1987.
- Harel, D., "Biting the silver bullet: toward a brighter future
for system development", IEEE Computer, 25(1): 8-20, enero 1992.
- Harel, D., Naamad, A.; "The STATEMATE
semantics of Statecharts", ACM Transactions on Software Engineering
and Methodology, 5(4), octubre 1996.
- Harel, D., Politi, M., "Modeling Reactive
Systems with Statecharts: The Statemate Approach".
- Hinchey, M., Jarvis, S.; Concurrent systems: formal
development in CSP, McGraw Hill, 1995.
- Hoare, C. A. R; Communicating
Sequential Processes, Prentice Hall, 1985.
- Jacky, J.; The way of Z, Cambridge University Press,
Cambridge, 1997.
- Jackson, M.; Software requirements & specificactions: a
lexicon of practice, principles and prejudices, Addison-Wesley,
1995.
- Jackson, M., Zave, P.; "Domain
Descriptions"; Proc. RE'93, pages 56-64; IEEE CS Press, 1993.
- Jackson, M., Zave, P.; "Deriving
Specifications from requirements: an Example"; ICSE'95, Seattle,
Washington USA; ACM 1995.
- Lamport, L., "The temporal logic of
actions", ACM Transactions on Programming Languages and Systems,
16(3): 872-923, mayo 1994.
- Lamport, L., "The module structure of
TLA+", SRC Technical Note, 1996-002, DEC, septiembre 1996.
- Lamport, L., "The operators of TLA+",
SRC Technical Note, 1997-006a, DEC, junio 1997.
- Lamport, L., "Specifying concurrent
systems with TLA+", en Calculational System Design, editores M.
Broy y R. Steinbrüggen, IOS Press, Amsterdam, 1999.
- Maibaum, T.S.E., "What we teach software engineering in the
university: do we take engineering seriously?", ACM Software
Engineering Notes, 22(6): 40-50, noviembre 1997.
- Parnas, D.L., "Software engineering: an
unconsumated marriage", Software Engineering Notes, 22(6): 1-3,
noviembre 1997.
- Potter, B., Sinclair, J., Till, D., An introduction to
formal specification and Z, Prentice Hall International,
Hertfordshire, 1996.
- Sommerville, I., Software Engineering, Addison-Wesley,
Harlow, 1995.
- Wing, J.; "A specifier's introduction to formal methods"; IEEE
Computer, 23(9):8-24, septiembre 1990.
- Wing, J.; "Hints to specifiers";
CMU-S-95-118r; Carnegie Mellon University, mayo 1995.
- Zave,P., Jackson,M.; "Four Dark Corners of
Requirements Engineering"; ACM Transactions on Software Engineering
and Methodology, Vol. 6, No 1, January 1997, Pages 1-30
Obligatoria
- Ghezzi, C.,
Jazayeri, M. y Mandrioli, D., Fundamentals of Software Engineering,
Prentice Hall, Upper Saddle River, 1991. Páginas: 1-8.
- Gibbs, W.W., "La crisis crónica de
la programación", Investigación y Ciencia, 72-81,
noviembre 1994.
- Brooks, F.P., "No silver bullet: essence and accidents of
software engineering", IEEE Computer, 20(4): 10-19, abril 1987.
- Harel, D., "Biting the silver bullet: toward a brighter future
for system development", IEEE Computer, 25(1): 8-20, enero 1992.
- Ghezzi, C., Jazayeri, M. y Mandrioli, D., Fundamentals of
Software Engineering, Prentice Hall, Upper Saddle River, 1991. Páginas: 357-382,
17-40, 43-57.
Optativa
- Brooks, F.P.,
The Mytical Man-Month, Addison-Wesley, 1975.
- Maibaum, T.S.E., "What we teach software engineering in the
university: do we take engineering seriously?", Software Engineering
Notes, 22(6): 40-50, noviembre 1997.
- Parnas, D.L., "Software engineering: an
unconsumated marriage", Software Engineering Notes, 22(6): 1-3,
noviembre 1997.
Obligatoria
Métodos Formales y Especificaciones
- Sommerville, I., Software
Engineering, Addison-Wesley, Harlow, 1995. Páginas:
157-164.
- Bowen, J., Hinchey, M., "Seven more myths
of formal methods", IEEE Software, 12(4):34-40, julio 1995.
- Clarke, E., Wing, J., "Formal methods:
state of the art and future directions", ACM Computing Surveys,
18(4):626-643, diciembre 1996. Por arriba, sobre todo el inicio
de cada sección.
- Jackson, M.; Software requirements & specificactions: a
lexicon of practice, principles and prejudices, Addison-Wesley,
1995. Páginas 9-11, 61-65, 78-83, 98-103,
109-112, 143-146, 193-196, 206-208.
- Wing, J.; "Hints to specifiers";
CMU-S-95-118r; Carnegie Mellon University, mayo 1995.
Z
- Apunte de clase sobre Z
- Jacky, J., The
way of Z, Cambridge University Press, Cambridge, 1997. Páginas
31-145, 218-230.
Statecharts
- Harel, D., "Statecharts: a visual formalism
for complex systems", Science of Computer Programming, 8(1987):
231-274, 1987.
- Apunte de clase sobre Statecharts parametrizados
CSP
- Apunte de clase sobre CSP
TLA
- Lamport, L., Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley Longman Publishing Co., Inc., 2002. Capítulos 1 al 8 inclusive.
Optativa
- Abadi, M., Lamport, L., "An old-fashioned
recipe for real time", ACM Transactions on Programming Languages
and Systems, 16(4): 1543-1571, septiembre 1994.
- Abadi, M., Merz, S., "On TLA as a logic",
en Deductive Program Design (Manfred Broy, ed.), NATO ASI Series,
Springer-Verlag (1995), 235-271. Proceedings of the NATO Advanced Study
Institute on Deductive Program Design, held in Marktoberdorf, Germany
(1994).
- Abadi, M.,
Alpern, B., Apt, K., Francez, N., Katz, S., Lamport, L., Schneider, F.,
"Preserving liveness: comments on 'Safety and
liveness from a methodological point of view'", Information
Processing Letters 40(3): 141-142, noviembre 1991.
- Alpern, B., Schneider, F., "Defining liveness", Information
Processing Letters, 21(4): 181-185, octubre 1985.
- Alpern, B., Schneider, F., "Recognizing
safety and liveness. Distributed Computing", 2:117--126, 1987.
- Bhargavam, K., Gunter, C., Gunter, E., Jackson, M., Obradovic,
D., Zave, P.; "The Village Telephone System:
a Case Study in Formal Software Engineering"; 11th International
Conference on Theorem Proving in Higher Order Logics, September 1998.
- Berry, D.M., Kamsties, E.; "The Dangerous
"All" in Specifications"; 10 International Workshop on Software
Specifications and Design, November 2000.
- Gunter, C., Gunter, E., Jackson, M., Zave, P.; "A reference model for requirements and
specifications", IEEE Software, 17(3): 37-43, mayo 2000.
- Harel, D., Naamad, A., "The STATEMATE
semantics of Statecharts", ACM Transactions on Software Engineering
and Methodology, 5(4), octubre 1996.
- Harel, D., Politi, M., "Modeling Reactive
Systems with Statecharts: The Statemate Approach".
- Hoare, C. A. R; Communicating
Sequential Processes, Prentice Hall, 1985.
- Jackson, M., Zave, P.; "Domain
Descriptions"; Proc. RE'93, pages 56-64; IEEE CS Press, 1993.
- Jackson, M., Zave, P.; "Deriving
Specifications from requirements: an Example"; ICSE'95, Seattle,
Washington USA; ACM 1995.
- Lamport, L., "The temporal logic of
actions", ACM Transactions on Programming Languages and Systems,
16(3): 872-923, mayo 1994. Páginas 872-889, 901-904.
- Roscoe, A., The theory and practice of concurrency,
Prentice Hall International, 1998. Páginas
1-145.
- Wing, J.; "A specifier's introduction to formal methods"; IEEE
Computer, 23(9):8-24, septiembre 1990.
- Zave,P., Jackson,M.; "Four Dark Corners of
Requirements Engineering"; ACM Transactions on Software Engineering
and Methodology, Vol. 6, No 1, January 1997, Pages 1-30
Obligatoria
- Saaltink, M., The
Z/EVES 2.0 user's guide, ORA Canada, Ottawa, 1999. Páginas
35-44, 19-33.
- Saaltink,
M., y
Meisels I., The Z/EVES Reference Manual, ORA Canada,
1997. Lo que necesiten.