| Ementa: |
Este curso fornece uma introdução à teoria da verificação de modelos e suacomplexidade teórica. Introduzimos sistemas de transição, propriedades desafety, 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 empalestras e envolvimento ativo em aulas de exercício. |
| Referências: |
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-2946. Efficient Parametric Model Checking Using Domain Knowledge. Radu Calinescu, Colin Paterson, Kenneth Johnson. TSE 2019. |
