Study programme 2020-2021Français
Project in formal methods for system design (List A)
Programme component of Master's in Mathematics à la Faculty of Science

Students are asked to consult the ECTS course descriptions for each learning activity (AA) to know what special Covid-19 assessment methods are possibly planned for the end of Q3

CodeTypeHead of UE Department’s
contact details
Teacher(s)
US-M1-SCMATH-048-MOptional UERANDOUR MickaëlS820 - Mathématiques effectives
  • RANDOUR Mickaël

Language
of instruction
Language
of assessment
HT(*) HTPE(*) HTPS(*) HR(*) HD(*) CreditsWeighting Term
  • Français
Français401565001212.00Année

AA CodeTeaching Activity (AA) HT(*) HTPE(*) HTPS(*) HR(*) HD(*) Term Weighting
S-MATH-043Formal methods: Introduction100000Q1
S-MATH-051Formal methods: foundations3015500Q1
S-MATH-056Formal Methods: Applications006000Q2
Programme component

Objectives of Programme's Learning Outcomes

  • Have integrated and elaborate mathematical knowledge.
    • Mobilise the Bachelor's course in mathematics to address complex issues and have profound mathematical expertise to complement the knowledge developed in the Bachelor's course.
    • Use prior knowledge to independently learn high-level mathematics.
    • Research mathematical literature in an efficient and relevant way.
    • Read research articles in at least one discipline of mathematics.
  • Carry out major projects.
    • Independently carry out a major project related to mathematics or mathematical applications. This entails taking into account the complexity of the project, its objectives and the resources available to carry it out.
    • Give constructive criticism on the quality and progress of a project.
    • Work in teams and, in particular, communicate effectively and with respect for others.
    • Appropriately use bibliographic resources for the intended purpose.
    • Present the objectives and results of a project orally and in writing.
  • Apply innovative methods to solve an unprecedented problem in mathematics or within its applications.
    • Mobilise knowledge, and research and analyse various information sources to propose innovative solutions targeted unprecedented issues.
    • Appropriately make use of computer tools, as required by developing a small programme.
  • Communicate clearly.
    • Communicate the results of mathematical or related fields, both orally and in writing, by adapting to the public.
    • make a structured and reasoned presentation of the content and principles underlying a piece of work, mobilised skills and the conclusions it leads to.
    • Have sufficient knowledge of English for basic scientific communication.
  • Adapt to different contexts.
    • Have developed a high degree of independence to acquire additional knowledge and new skills to evolve in different contexts.
    • Critically reflect on the impact of mathematics and the implications of projects to which they contribute.
    • Demonstrate thoroughness, independence, creativity, intellectual honesty, and ethical values.

Learning Outcomes of UE

Thorough understanding of the core concepts of formal methods, mastery of the underlying mathematical frameworks, ability to apply them to practical cases using software tools, ability to include formal methods in software development processes, understanding of advanced work in the field.

Content of UE

Theory: Introduction to formal methods, Modeling systems, Linear temporal logic, Computation tree logic, Symbolic model checking, Model checking probabilistic (and quantitative) systems, Synthesis of probabilistic (and quantitative)
systems, Synthesis via game theory. Tool presentations by students. Presentation of advanced work on verification and synthesis of computer systems. Project: system development using formal methods.

Prior Experience

Basic notions of algorithmics, programming, complexity, logic.

Type of Assessment for UE in Q1

  • Presentation and/or works
  • Oral examination

Q1 UE Assessment Comments

Oral exam on theory and exercises (Evaluation E1). Tool presentation by students (Evaluation E2).

Type of Assessment for UE in Q2

  • Presentation and/or works
  • Oral Examination

Q2 UE Assessment Comments

Presentations of advanced work based on scientific articles or books (Evaluation E3). Project (possibly within a group) (Evaluation E4). Final grade for UE. If an evaluation is below 8, the final grade is equal to the minimal evaluation. Otherwise, the following weights are used: E1 (40%), E2 (10%), E3 (20%), E4 (30%).

Type of Assessment for UE in Q3

  • Presentation and/or works
  • Oral examination

Q3 UE Assessment Comments

Same rules as for Q1/Q2. Any evaluation below 10 must be passed in Q3.

Type of Resit Assessment for UE in Q1 (BAB1)

  • N/A

Q1 UE Resit Assessment Comments (BAB1)

Not applicable.

Type of Teaching Activity/Activities

AAType of Teaching Activity/Activities
S-MATH-043
  • Cours magistraux
S-MATH-051
  • Cours magistraux
  • Exercices dirigés
  • Utilisation de logiciels
  • Démonstrations
  • Préparations, travaux, recherches d'information
S-MATH-056
  • Préparations, travaux, recherches d'information

Mode of delivery

AAMode of delivery
S-MATH-043
  • Face to face
S-MATH-051
  • Face to face
S-MATH-056
  • Face to face

Required Reading

AA
S-MATH-043
S-MATH-051
S-MATH-056

Required Learning Resources/Tools

AARequired Learning Resources/Tools
S-MATH-043Lecture notes available on Moodle.
S-MATH-051Lecture notes available on Moodle.
S-MATH-056Lecture notes available on Moodle.

Recommended Reading

AA
S-MATH-043
S-MATH-051
S-MATH-056

Recommended Learning Resources/Tools

AARecommended Learning Resources/Tools
S-MATH-043Not applicable
S-MATH-051Not applicable
S-MATH-056Not applicable

Other Recommended Reading

AAOther Recommended Reading
S-MATH-043C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
S-MATH-051C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
S-MATH-056C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
(*) HT : Hours of theory - HTPE : Hours of in-class exercices - HTPS : hours of practical work - HD : HMiscellaneous time - HR : Hours of remedial classes. - Per. (Period), Y=Year, Q1=1st term et Q2=2nd term
Date de génération : 09/07/2021
20, place du Parc, B7000 Mons - Belgique
Tél: +32 (0)65 373111
Courriel: info.mons@umons.ac.be