Carregando...

DISCIPLINA Listagem de Ementa/Programa

ENGENHARIA DE SOFTWARE 1DISCIPLINA 316237

VER OFERTA

ÓrgãoCIC Departamento de Ciência da Computação
Código316237
DenominaçãoEngenharia de Software 1
NívelMestrado
Início da Vigência em1994/1
Pré-requisitosDisciplina sem pré-requisitos
EmentaInício da Vigência em 2020/1

Este curso fornece uma introdução à teoria da verificação de modelos e sua
complexidade teórica. Introduzimos sistemas de transição, propriedades de
safety, liveness e fairness, além de cobrimos as lógicas temporais LTL, CTL,
comparamos e tratamos seus algoritmos de verificação de modelo. Finalmente, consideramos a verificação de modelo de autômatos probabilísticos
(DTMC e MDP) e verificação simbólica de modelos. O curso consiste em
palestras e envolvimento ativo em aulas de exercício.

ProgramaInício da Vigência em 2020/1

1. Introdução a princípios de verificação de modelos (model checking).

2. Modelagem de sistemas concorrentes

3. Propriedades tempo-linear

4. Lógica Temporal Linear

5. Lógica de Arvore Computacional

6. Verificação de modelos probabilística e paramétrica: DTMC e MDP.

7. Trabalhos práticos em modelagem e análise em ferramentas de verificação de modelos

BibliografiaInício da Vigência em 2020/1

Bibliografia principal:
Christel Baier, Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008.

J.Magee and J. Kramer. Concurrency: State Models and Java Pro- grams. John Wiley, New York, 1999.

Bibliografia adicional:
1. Timed Automata: Semantics, Algorithms and Tools, Johan Bengtsson and Wang Yi. In Lecture Notes on Concurrency and Petri Nets. W. Reisig and G. Rozenberg (eds.), LNCS 3098, Springer-Verlag, 2004.

2. A Tutorial on Uppaal, Gerd Behrmann, Alexandre David, and Kim G. Larsen. In proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT’04). LNCS 3185.

3. PRISM: Probabilistic Symbolic Model Checker. Marta Kwiatkowska, Gethin Norman and David Parker. In Proc. PAPM/PROBMIV’01 Tools Session, pages 7-12. Available as Technical Report 760/2001, University of Dortmund. September 2001.

4. PRISM 4.0: Verification of Probabilistic Real-time Systems. Marta Kwiatkowska, Gethin Norman and David Parker. In Proc. 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of LNCS, pages 585-591, Springer. July 2011.

5. Symbolic and Parametric Model Checking of Discrete-Time Markov Chains. Conrado Daws. ICTAC 2004: 280-294

6. Efficient Parametric Model Checking Using Domain Knowledge. Radu Calinescu, Colin Paterson, Kenneth Johnson. TSE 2019.