MF

Print

MF: Models and Formalizations

Person in charge: Antoine Beugnard (mail)

Pedagogical team: Antoine Beugnard, Fabien Dagnat, Serge Garlatti, Damien Massé, Franck Singhoff (mail)

Description

A model is a core concept in sciences. Every representation is eventually a model of the system under study (SuS), whatever the representation is: a talk, a picture or a mathematical description. The goal of this unit is to introduce the modeling problematics (how and why creating a model) in computer science.

To reach this goal, we present some syntactic and semantic tools that have been proposed to elaborate models. Beyond a simple catalog, we focus on the commonalities and differences of the principles used in these modeling and reasoning tools.

Keywords: formal systems, logic, models

Prerequisites: Some mathematical formalisms; programmation basics;

Learning outcomes

Gained knowledge and know-how: At the end of this course students will be able to explain and perform a modeling approach using formal tools (mathematics) or semi-formal (diagrams). Logic, lambda calculus, abstract interpretation or notations such as UML will illustrate the mechanisms used for modeling and the use of these models.

Contents

  • Introduction to modeling (2h)
    • Elaborate a model
    • Syntax et semantic
    • Interpretation
  • Semi-formal Modeling (with UML) (2h)
    • Class diagram and semantic variation points
    • Meta-modeling
  • Standard and non standard logics (4h)
    • Axiomatic and models theories
    • Predicate calculus
    • Modal logics
  • Formal model of calculus (4h)
    • Semantics
    • Formalization of automatic reasoning
    • Elements of lambda calculus (name, substitution, reduction, confluence, type, induction, proof)
    • Elements of pi calculus (labeled transition systems, trace equivalence and bisimulation)
  • Abstract interpretation (4h)
  • Model for real-time (4h)

Bibliography

  • Practical Formal Software Engineering, Bruce Mills
  • Models of Computation: An Introduction to Computability, Maribel Fernandez
  • Introduction aux méthodes formelles, Jean-François Monin
  • Logique Réduction Résolution, René Lalement
  • Communicating and mobile systems: the pi-calculus, Robin Milner

Evaluation mode

  • Final (written) examination of 2 hours mid-december
Buy cheap web hosting service where fatcow web hosting review will give you advices and please read bluehost review for more hosting information.