[NOTÍCIA ATUALIZADA] CURSO - SYSTEM MODELLING WITH LOGIC AND DISCRETE MATHEMATICS

Prezados,

Convidamos todos a participarem do curso "SYSTEM MODELLING WITH LOGIC AND DISCRETE MATHEMATICS", a ser ministrado pelo professor Camilo Rueda da UNIVERSIDAD JAVERIANA-CALI, COLOMBIA.

INSCRIÇÕES

Através do email do PPgMAE: ppgmae@ccet.ufrn.br, até o dia 16/05/2016.

LOCAL, DATAS E HORÁRIOS

Sala: B1, Setor III (todas as sessões)

Dias 16/05 e 18/05: 10:50 - 12:30

Dias 17/05 e 19/05: de 16:50 a 18:30.

PROGRAMA DO CURSO

1. Introduction   (1 hora de duração)
• Constructing Dependable Systems
• Direct techniques for dependable systems: formal models
• Difficulties (real and imaginary) of constructing formal models
• Support tools for modelling

2. Models and correctness   (3 horas de duração)
• Event-B: a language for specifying models
• Static and dynamic components of Event-B models
• Proof obligations of an Event-B model
• Modelling by stepwise refinement: what is a refinement of a model in Event-B
• Labelled transitions semantics of Event-B
• Proof obligations of a refinement
• Animation of an Event-B model using ProB

3. Modelling with Sets   (2 horas de duração)
• The Event-B language of sets
• Sets as types
• Sets for object classification
• Case study: Model of a landing gear

4. Expressing properties in Predicate Logic   (3 horas de duração)
• The Event-B language of Propositional and Predicate logic
• Proof obligations revisited
• The Event-B language of functions and relations
• Case study: expressing properties of a social network

5. Proving a Model   (1 hora de duração)
• Discharging proof obligations interactively
• The variety of Rodin provers
• Strategies for discharging proofs