Lógica
aplicada a la verificación del software
y optimización
Curso
2007-2008
Programa de Máster en Ingeniería del
Software, Métodos Formales y Sistemas de Información
DEPARTAMENTO DE SISTEMAS INFORMÁTICOS
Y
COMPUTACIÓN (DSIC)
OBJETIVO
•
La
lógica no es sólo un concepto filosófico o
matemático. A lo largo de la historia distintos tipos de
lógicas se han utilizado en prácticamente todos los
campos relacionados con la informática. El objetivo de esta
asignatura es que el alumno conozca y sepa distinguir las posibles
aplicaciones de distintos tipos de lógicas en el ciclo de vida
del desarrollo de software. Al final de curso el alumno debe ser
capaz de identificar qué tipo de aproximación es
adecuada para un problema específico.
•
Los
contenidos de este seminario pueden ser usados con distintos
objetivos finales y en distintos procesos de la ingeniería del
software, dando lugar a métodos ágiles, parciales,
optimizados y/o automáticos de técnicas de
verificación, modelado, etc. No nos vamos conformar con dar a
conocer las distintas lgicas que han sido definidas a lo largo de los
años, sino que también pretendemos mostrar cuáles
son las lógicas que podemos aplicar en cada momento dependiendo
del propósito final (modelado, verificación, etc.) y del
marco de trabajo en el que se tenga que integrar
(programación declarativa, visual, bases de datos, etc.).
Además de profundizar en la aplicabilidad de las distintas
lógicas, otro objetivo principal de este seminario es el de
conocer dos técnicas de optimización básicas que
pueden ser integradas, de nuevo, en las distintas áreas y
niveles de la ingeniería del software. Se trata de las representaciones simbólicas
(especialmente útiles en las técnicas de
verificación para compactar el espacio de búsqueda) y de
la interpretación abstracta
(que puede ser el mecanismo para hacer posible el manejo de problemas
con dominios infinitos, por ejemplo para la verificación de
programas con un
número infinito de estados).
Para mostrar la aplicabilidad tanto de las lógicas como de las
técnicas de optimización, introduciremos un modelo
concurrente con el que podemos especificar software complejo, como
pueden ser los sistemas reactivos, protocolos de comunicación,
sistemas empotrados, etc.
•
-
Metodologia de enseñanza y aprendizaje: Clases
presenciales, ejercicios propuestos para resolver en clase, trabajo no
presencial tutorizado.
-
Criterios y procedimientos de evaluación : Trabajos
individuales realizados durante el curso, o examen escrito al finalizar
el cuatrimestre
TEMARIO
1.
Introducción
2.
Lógicas y sus aplicaciones
Historia
Lógica
modal
Lógica temporal
Lógica dinámica
Lógica epistémica
Lógica difusa
3.
Técnicas de optimización asociadas
4.
Caso de estudio
BIBLIOGRAFÍA
BÁSICA
•
Lógicas
- Temporal and Modal Logic.
E. Allen Emerson. Handbook of Theoretical Computer Science (vol. B):
Formal Models and Semantics, páginas 995-1072, MIT Press, 1990
- A new introduction to modal logic [Recurso
electrónico-En línea] (Hughes, G. E (1918-))
- Model theory for modal logic : Kripke models for modal
predicate calculi (Bowen, Kenneth A.)
- Dynamic Logic.
D. Harel, Dexter Kozen y Jerzy Tiuryn. Handbook of Philosophical Logic
Volume II - Extensions of Classical Logic, páginas 497-604. D.
Reidel Publishing Company, 1984.
- Dynamic logic (Harel, David)
- Lógica fuzzy para principiantes : Cuando la
máquina se acerca al pensamiento humano (Hernández
Negrín, Isabel; López Campos, Ibán)
- Metodos de tableaux para logicas con declaraciones de
terminos,
dominios preordenados y operaciones monotonas [Recurso
electrónico-En
línea] (Martin de la Calle, Pedro Jesus)
- Rewriting Logic as a Logical
and Semantic Framework. Narciso Martí-Oliet y José
Meseguer. Proc. 1st Intl. Workshop on Rewriting Logic and its
Applications, Electronic Notes in Theoretical Computer Science,
Elsevier Sciences, 1996.
- Apuntes de la asignatura DSW:
DSIC-DD/02/06 - Versión digital disponible. Autor:
Alicia Villanueva
Complementaria
- Regular model checking.
A. Bouajjani, B. Jonsson, M.
Nilsson, and T. Touili. In Proc. 12th Int. Conf. Computer Aided
Verification (CAV'2000), Chicago, USA, July 2000, volume 1855 of
Lecture Notes in Computer Science. Springer, 2000.
- A Timed Concurrent Constraint
Language. F.S. de Boer, M. Gabbrielli y M.C. Meo. Information
and Computation, vol. 161, 2000.
- Concurrent Constraint
Programming. V.A. Saraswat y M. Rinard. Proc. of 17th Annual ACM
Symposium on Principles of Programming Languages, páginas
232-245. ACM Press, 1990.
- Model Checking: A Tutorial
Introduction. M. Muller-Olm, D.A. Schmidt y B. Steffen. Proc.
SAS'99. vol. 1696 de Lecture Notes in Computer Science, páginas
330-354. 1999
- Symbolic boolean manipulation
with ordered binary decision diagrams. R.E. Bryant. ACM
Computing Surveys, vol. 24(3), páginas 293-318, 1992.
- Difference Decision Diagrams.
J. Moller, J. Lichtenberg, H.R. Andersen y H. Hulgaard. Proc. of the
13th International Workshop on Computer Logic Science, vol. 1683,
Lecture Notes in Computer Science, páginas 111-125. 1999.
- Symbolic Model Checking: 1020 states and beyond. J.R. Burch,
E.M. Clarke, K.L. McMillan, D.L. Dill y L.J. Hwang.Information and
Computation, vol. 98, no. 2, páginas 142-170. 1992.
- Abstract Interpretation: A
unified lattice model for static analysis of programs by construction
or approximation of fixpoints. P. Cousot y R. Cousot. Proc. of
the 4th ACM Symposium POPL. páginas 238-252. ACM Press, 1979.
- Model Checking and Abstraction.
E.M. Clarke, O. Grumberg y D.E. Long. ACM Transactions on PRogramming
Languages and Systems. vol 16, páginas 1512-1542, 1994.
- N. Jones, F. Nielson.
Abstract interpretation: a semantics-based tool for program
analysis. En S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum,
editores, Handbook of Logic in Computer Science, volume 4, Semantic
Modelling, páginas 527-636, Oxford University Press, 1995
- Software reliability
methods (Peled, Doron A.)
- Model checking (Clarke, Edmund M., Jr.)
- Automated theorem proving, a logical basis (Loveland,
Donald W.)
Última actualización:
Julio de 2007