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.


 

 

 

 

 






General

  1. Abadi, M., Lamport, L., "An old-fashioned recipe for real time", ACM Transactions on Programming Languages and Systems, 16(4): 1543-1571, septiembre 1994.
  2. 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.
  3. Alpern, B., Schneider, F., "Defining liveness", Information Processing Letters, 21(4): 181-185, octubre 1985.
  4. Alpern, B., Schneider, F., "Recognizing safety and liveness. Distributed Computing", 2:117--126, 1987.
  5. 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.
  6. Berry, D.M., Kamsties, E.; "The Dangerous "All" in Specifications"; 10 International Workshop on Software Specifications and Design, November 2000.
  7. Bowen, J., Hinchey, M., "Seven more myths of formal methods", IEEE Software, 12(4):34-40, julio 1995.
  8. Brooks, F.P., "No silver bullet: essence and accidents of software engineering", IEEE Computer, 20(4): 10-19, abril 1987.
  9. Brooks, F.P., The Mytical Man-Month, Addison-Wesley, 1975.
  10. Robert N. Charette, "The Trillion-Dollar Cost of IT's Willful Ignorance", IEEE Spectrum 62(12):38-43 (2025)
  11. Clarke, E., Wing, J., "Formal methods: state of the art and future directions", ACM Computing Surveys, 18(4):626-643, diciembre 1996.
  12. Hubert Garavel, Maurice H. ter Beek, Jaco van de Pol, "The 2020 Expert Survey on Formal Methods", FMICS 2020: 3-69
  13. Ghezzi, C., Jazayeri, M. y Mandrioli, D., Fundamentals of Software Engineering (2nd edition), Prentice Hall, Upper Saddle River, 2002.
  14. Gibbs, W.W., "La crisis crónica de la programación", Investigación y Ciencia, 72-81, noviembre 1994.
  15. Gunter, C., Gunter, E., Jackson, M., Zave, P.; "A reference model for requirements and specifications", IEEE Software, 17(3): 37-43, mayo 2000.
  16. Harel, D., "Statecharts: a visual formalism for complex systems", Science of Computer Programming, 8(1987): 231-274, 1987.
  17. Harel, D., "Biting the silver bullet: toward a brighter future for system development", IEEE Computer, 25(1): 8-20, enero 1992.
  18. Harel, D., Naamad, A.; "The STATEMATE semantics of Statecharts", ACM Transactions on Software Engineering and Methodology, 5(4), octubre 1996.
  19. Harel, D., Politi, M., "Modeling Reactive Systems with Statecharts: The Statemate Approach".
  20. Hinchey, M., Jarvis, S.; Concurrent systems: formal development in CSP, McGraw Hill, 1995.
  21. Hoare, C. A. R; Communicating Sequential Processes, Prentice Hall, 1985.
  22. Jackson, M.; Software requirements & specificactions: a lexicon of practice, principles and prejudices, Addison-Wesley, 1995.
  23. Jackson, M., Zave, P.; "Domain Descriptions"; Proc. RE'93, pages 56-64; IEEE CS Press, 1993.
  24. Jackson, M., Zave, P.; "Deriving Specifications from requirements: an Example"; ICSE'95, Seattle, Washington USA; ACM 1995.
  25. Lamport, L., "The temporal logic of actions", ACM Transactions on Programming Languages and Systems, 16(3): 872-923, mayo 1994.
  26. Lamport, L., "The module structure of TLA+", SRC Technical Note, 1996-002, DEC, septiembre 1996.
  27. Lamport, L., "The operators of TLA+", SRC Technical Note, 1997-006a, DEC, junio 1997.
  28. Lamport, L., "Specifying concurrent systems with TLA+", en Calculational System Design, editores M. Broy y R. Steinbrüggen, IOS Press, Amsterdam, 1999.
  29. Lamport, L., Specifying Systems. The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2003
  30. 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.
  31. Parnas, D.L., "Software engineering: an unconsumated marriage", Software Engineering Notes, 22(6): 1-3, noviembre 1997.
  32. William Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1997.
  33. Schneider, S., The B-Method: an Introduction, Palgrave, 2001.
  34. Sommerville, I., Software Engineering, Addison-Wesley, Harlow, 1995.
  35. Wing, J.; "A specifier's introduction to formal methods"; IEEE Computer, 23(9):8-24, septiembre 1990.
  36. Wing, J.; "Hints to specifiers"; CMU-S-95-118r; Carnegie Mellon University, mayo 1995.
  37. Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John S. Fitzgerald, "Formal methods: Practice and experience", ACM Comput. Surv. 41(4): 19:1-19:36 (2009)
  38. 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




Unidad I

Optativa

  1. Ghezzi, C., Jazayeri, M. y Mandrioli, D., Fundamentals of Software Engineering (2nd edition), Prentice Hall, Upper Saddle River, 2002. Capítulos 1-3, 7.
  2. Gibbs, W.W., "La crisis crónica de la programación", Investigación y Ciencia, 72-81, noviembre 1994.
  3. Robert N. Charette, "The Trillion-Dollar Cost of IT's Willful Ignorance", IEEE Spectrum 62(12):38-43 (2025)
  4. Brooks, F.P., "No silver bullet: essence and accidents of software engineering", IEEE Computer, 20(4): 10-19, abril 1987.
  5. Harel, D., "Biting the silver bullet: toward a brighter future for system development", IEEE Computer, 25(1): 8-20, enero 1992.
  6. Brooks, F.P., The Mytical Man-Month, Addison-Wesley, 1975.
  7. 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.
  8. Parnas, D.L., "Software engineering: an unconsumated marriage", Software Engineering Notes, 22(6): 1-3, noviembre 1997.

 

Unidad III

Obligatoria

B

  1. Apunte de clase sobre B
  2. Schneider, S., The B-Method: an Introduction, Palgrave, 2001. Capítulos 1, 2, 4-7 y 9; pueden obviar todo lo relacionado a "weakest precondition".

Statecharts

  1. Harel, D., "Statecharts: a visual formalism for complex systems", Science of Computer Programming, 8(1987): 231-274, 1987.
  2. Apunte de clase sobre Statecharts parametrizados
    3.

CSP

  1. Apunte de clase sobre CSP

TLA

  1. 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

  1. Abadi, M., Lamport, L., "An old-fashioned recipe for real time", ACM Transactions on Programming Languages and Systems, 16(4): 1543-1571, septiembre 1994.
  2. 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).
  3. 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.
  4. Alpern, B., Schneider, F., "Defining liveness", Information Processing Letters, 21(4): 181-185, octubre 1985.
  5. Alpern, B., Schneider, F., "Recognizing safety and liveness. Distributed Computing", 2:117--126, 1987.
  6. 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.
  7. Berry, D.M., Kamsties, E.; "The Dangerous "All" in Specifications"; 10 International Workshop on Software Specifications and Design, November 2000.
  8. Gunter, C., Gunter, E., Jackson, M., Zave, P.; "A reference model for requirements and specifications", IEEE Software, 17(3): 37-43, mayo 2000.
  9. Harel, D., Naamad, A., "The STATEMATE semantics of Statecharts", ACM Transactions on Software Engineering and Methodology, 5(4), octubre 1996.
  10. Harel, D., Politi, M., "Modeling Reactive Systems with Statecharts: The Statemate Approach".
  11. Hoare, C. A. R; Communicating Sequential Processes, Prentice Hall, 1985.
  12. Jackson, M., Zave, P.; "Domain Descriptions"; Proc. RE'93, pages 56-64; IEEE CS Press, 1993.
  13. Jackson, M., Zave, P.; "Deriving Specifications from requirements: an Example"; ICSE'95, Seattle, Washington USA; ACM 1995.
  14. 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.
  15. Roscoe, A., The theory and practice of concurrency, Prentice Hall International, 1998. Páginas 1-145.
  16. Wing, J.; "A specifier's introduction to formal methods"; IEEE Computer, 23(9):8-24, septiembre 1990.
    17.
  17. 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
  18. Sommerville, I., Software Engineering, Addison-Wesley, Harlow, 1995. Páginas: 157-164.
  19. Bowen, J., Hinchey, M., "Seven more myths of formal methods", IEEE Software, 12(4):34-40, julio 1995.
  20. 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.
  21. 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.
  22. Wing, J.; "Hints to specifiers"; CMU-S-95-118r; Carnegie Mellon University, mayo 1995.

Unidad IV

Obligatoria

Ver el material en la sección TP/Proyecto