Sixième Semestre de la Chaire UNESCO

Mathématiques Discrètes et Logique: Fondements et Applications à la spécification, 

Analyse et conception de logiciels

Tunis, 28 Janvier - 25 Avril 2008

COORDINATEURS : Ali MILI (NJIT, USA), Rahma BEN AYED (ENIT-SysCom/Université Tunis el Manar)

page d'accueil

Affiche du sixième semestre (pdf)

L'objectif du cours

Profil des Participants

Calendrier

Intervenants

Programme du cours 

Calendrier général

Inscription

Aide financière (.doc)

Contact

L'objectif du cours

Selon Harlan D Mills (1919-1996), un Fellow d'IBM, les mathématiques continues modélisent les phnéomènes naturels alors que les mathématiques discrètes modélisent les produits artificiels. Vu que l'informatique est le produit de l'imagination et de l'invention humaine, les mathématiques discrètes sont l'outil de choix pour en modéliser les produits et les processus. L'objectif de ce cours est de présenter un certain nombre de branches des mathématiques discrètes, ainsi que leurs applications en informatique. Historiquement, les modèles mathématiques n'ont pas précédé le développement de leurs champs d'application. En fait, souvent le modèle mathématique a été développé simultanément ou ultérieurement au domaine d'application. Pour des raisons pédagogiques, nous nous éfforcons de présenter les modèles avant leur application, et de motiver les modèles par leur intégrit éet leur intéret intrinséque.

Profil des Participants / Pré-requis

Ce cours s'adrésse à un public large, incluant des informaticiens intéressés par les fondements mathématiques de leur discipline, et des mathématiciens intéressés par les applications informatiques de leur discipline. Des spécialistes d'autres disciplines scientifiques (Physique, Biologie, etc) ou de génie (mécanique, civil, etc) qui ont l'agilité d'esprit et la curiosité d'aborder des disciplines nouvelles peuvent aussi trouver ce cours d'un certain intérêt. Dans l'ensemble, nous exigeons un niveau de maitrise environ (Bac+4), mais pouvons ajuster le niveau du cours selon le profil final des classes.

Calendrier

Intervenants

M. Kaâniche (LAAS-CNRS, France)
Cours V (25-29 février)
Dependability Evaluation of Computer Based-Systems
Biography. Mohamed Kaâniche is Chargé de Recherche at CNRS, the French National Organization for Scientific Research. He joined LAAS-CNRS in 1988 as a member of the research group on Dependable Computing and Fault Tolerance. From March 1997 to February 1998, he was a Visiting Research Assistant Professor at the University of Illinois at Urbana Champaign, USA. His research activities focus on the dependability and security evaluation of fault-tolerant computing systems and critical infrastructures based on analytical modelling and experimental measurement approaches. He has (co)authored more than 70 papers on these subjects in international journals and conference proceedings. He has participated and contributed to several European research projects and acted as a consultant for companies in France and a reviewer for the European Commission. He has served on program and organisation committees of several international conferences. He was Program co-chair of PRDC-2004, Program Chair of EDCC-5, and Conference Coordinator of DSN 2007.

Biography.Adel BOUHOULA obtained his undergraduate degree in computer engineering with distinction from the University of Tunis in Tunisia. He also holds a Master’s, PhD and Habilitation from Henri Poincare University in Nancy, France. He is currently a Full Professor at the Sup’Com Engineering School of Telecommunications in Tunisia. He is also the founder and Director of the Research Unit on Digital Security and the President of the Tunisian association of Digital Security. He has published over 70 articles in leading international journals, in conferences and refereed workshops since 1992. His research interests include Automated Reasoning, Network Security, Cryptography, and Validation of cryptographic protocols. He was invited to give seminars in numerous universities and laboratories namely in France, the United Kingdom, Italy, Germany, Russia, Australia, Canada, the United States and Japan. He was also invited to make several research visits in particular to SRI International (California - USA), to the Mitsubishi Research Institute (Tokyo - Japan), to the Laboratory Specification and Verification at the “Ecole Normale Supérieure” of Cachan (Paris – France), to the Hardware Verification Group at Concordia University (Montreal - Canada) and to the Symbolic Computation Research Group at the University of Tsukuba (Tsukuba – Japan).
Adel BOUHOULA has been in the past the Chairman and CEO of the IRSIT Research Institute for Computer Science and Telecommunication in Tunisia. Prior to that, he has been the Director of Information Technologies and Networks at “Tunisie Telecom” and a Senior Researcher with the INRIA French National Institute for Research in Computer Science and Control in France. Adel BOUHOULA was decorated as the Knight of the Order of the Republic and also the Knight of the National Order of the Merit in the field of the Education and of the Science.

J. Schumann (NASA Ames Research center, USA)
Cours X (7 – 11 avril)
Verification and Validation of Adaptive Systems
Biography. Dr. Johann Schumann (PhD 1991, Dr. habil 2000, Munich, Germany) is a Senior Scientist with RIACS/USRA and working in the Robust Software Engineering Group at NASA Ames.  He is engaged in research on verification and validation of autonomy software and adaptive controllers, and on automatic generation of reliable code for data analysis, navigation, and state estimation. Dr. Schumann's general research interests focus on the application of formal methods to improve design and reliability of advanced safety- and security-critical software.  Dr. Schumann is author of a book on theorem proving in software engineering and has published more than 70 articles on automated deduction, and its applications, automatic program generation, and neural network oriented topics.

 A. Jaoua (University of Qatar, Qatar, and FST, Tunisia)
Cours XI (14 – 18 avril)
Relational Algebra and Data Base
Biography. Professor Ali Jaoua is a faculty member of computer Science and engineering department, University of Qatar, since 2000, in leave from University of Manar (Tunisia), where he supervised the Research Group on Algorithmic and Heuristics (URPAH: 50 Members). He obtained the degree of "Docteur es-Science" (1987) from the University Paul Sabatier of Toulouse (France), "Doctor Engineer" (1979) from Institute Polytechnic of Toulouse, and "Engineer in Computer Science" from ENSEEIHT of Toulouse (1977). His research areas are Software and Information Engineering. He has been working on the Use of Relational Methods in Computer Science since 1984, and the application of formal concept analysis in Information Engineering since 1990. He has been Invited Prof./researcher in the following universities: University Joseph Fournier, Grenoble, France, July 2004, University of Sherbrooke (Canada), in 1989, Sophia-Antipolis (I3S) (France) during December 1991. He has been associate Professor in computer science in Laval University (Quebec, Canada), 1989-1992. He has been invited speaker for some international conferences and universities during the last ten years. He also has organized several conferences in computer science, and has been the seminar coordinator for about 12 years of his carrier. He supervised about 12 Phd-thesis defended mostly on conceptual information engineering, and several Masters. He published about 35 papers in International Journals, and many conferences, and contributes in several books. He is a Member of the Steering Committee of Relational Methods in Computer Science Group, RELMICS, and Editorial member of the associated electronic journal (JORMICS), Member of the Editorial Board of the Journal of Computing, since 2004. Member of The International Reviewers Committee of the Journal of Web Engineering, since 2005. He has also been member of many associations in computer science.

J. R. Abrial (ETH, ZURICH)
Lecture XII (21 – 25 avril / April 21st – April 25th)
Event-B and the Rodin Platform
Biographie. Jean-Raymond Abrial is the co-inventor of Z, B and Event-B. He is the author of the B-book, which presents the B-Method. He is currently finishing a new book on Event-B. He was a guest Professor at ETH Zurich from 2004 to 2007 where he led the team developing the Rodin Platform for Event-B (funded by the European Project Rodin). He is currently a researcher also at ETH Zurich, working on a new European Project called Deploy. Before being in Zurich, he was a consultant for more than 20 years working in close contact with Industrial Companies but also with various Universities around the world.

Programme du cours

Dans la suite nous présentons les différentes descriptions des cours, y compris une synthèse courte, un programme, une bibliographie appropriée, et une biographie des conférenciers.

 Cours I (28 Janvier - 1 Février)
Discrete Structures and Refinement Calculi
Enseignant A. Mili (NJIT)

• Course Objectives.  The purpose of this course is merely to introduce some background material that serves to support most, if not all, subsequent lectures.  This material includes concepts of discrete mathematics and logic, but will also include a discussion of a relational refinement calculus, and its lattice structure. 
• Course Syllabus.  Sets, Relations and Functions.  Partial Orderings and Lattice Structures.  Strict Partial Ordering and Well Founded Sets.  Propositional Logic and Predicate Logic.  Mathematical Induction and Mathematical Deduction.  A Relational Refinement Structure.

Cours II (4 Février -8 Février)
Formal Methods
Enseignant Rahma Ben Ayed (ENIT-SysCom)

• Course Objectives.  While the previous course presents a conceptual background for the many courses in this series, this course presents a practical tenet.  Most formal methods are virtually inoperational in practice unless they are supported by a theorem proving capability.  The objective of this course is to discuss current techniques for automated inference, and expose the participants to some operational tools for theorem proving.
• Course Syllabus. Natural deduction, sequent calculi, unification,  resolution strategies, decision procedures.  Otter:  basic algorithm and usage.  Theorem proving practice in Otter.

 Cours III (11 Février – 15 Février)
Specification and Verification of Distributed Systems (First part)
Enseignant K. Barkaoui (CEDRIC CNAM-Paris)

• Course Objectives.  The specification, verification and design of concurrent and distributed systems differ fundamentally from that of regular sequential systems, and raises fundamentally different theoretical and practical issues.  As a result, it is typically modelled using fundamentally distinct mathematical constructs.  These are the subject of this course, where we will discuss in turn, models and languages of specification, then verification techniques.
• Course Syllabus.  Concurrency paradigms and issues. Specification models : intentional models versus extensional models, interleaving versus true concurrency, linear-time vs branching-time. State transitions systems, synchronized automata, Kripke structure and Petri nets.  Behavorial properties : reachability problem, safety and liveness properties, fairness, simulation, bissimulation, trace equivalence. Structural Verification : structural reduction of nets, linear algebra based techniques, graph-theory based techniques.

Cours IV (18 Février - 22 Février)
Specification and Verification of Distributed Systems (Second part)
Enseignants J.M Ilié et D. Poitrenaud (Université Paris 5 / LIP6 Lab, France)
Support 1 - Support 2

• Course Objectives.  The specification, verification and design of concurrent and distributed systems differ fundamentally from that of regular sequential systems, and raises fundamentally different theoretical and practical issues.  As a result, it is typically modelled using fundamentally distinct mathematical constructs.  These are the subject of this course, where we will discuss in turn, models and languages of specification, then verification techniques.
• Course Syllabus. Temporal logic: linear-time temporal logic (LTL), computation tree logic (CTL), fairness strategy. Model checking techniques and tools for finite concurrent systems: automata theoretic approach of model-checking (Büchi automata, Street automata), techniques to limit the state explosion problem (partial order approaches, symbolic algorithms). Model checking techniques and tools for infinite systems, dynamic structures, timing requirements, extensions for Petri nets (Petri nets with recursion and time), process algebra.

 Cours V (25 Février- 29 Février)
Dependability evaluation of computer-based systems
Enseignant M. Kaâniche (LAAS-CNRS)

• Course Objectives. The purpose of this course is to present: 1) the main concepts and techniques that are commonly used to evaluate the dependability and security of computing systems and 2) the state of knowledge and research challenges in this field. Both accidental and malicious threats will be addressed considering model-based and experimental evaluation approaches. Examples of applications and case studies will be presented for illustration.
• Course Syllabus.  Dependability concepts. Quantitative dependability measures. System level analysis and evaluation methods:
  FMECA, Fault trees, State-based methods (Markov, stochastic Petrinets). Model-based and experimental techniques for fault tolerance
  
  assessment. Software reliability evaluation methods: trend tests and reliability growth models. Evaluation with regard to malicious Threats. Application examples and case studies.

    Cours VI (3 Mars-7 Mars)
Unified Theory of programming
   Enseignant Jim Woodcock (University of York, UK)

http://www.unifyingtheories.org/

• Course Objectives.  By the end of the module, students will: (1) Understand how to model programming constructs in the alphabetized relational calculus. (2) Understand theories of sequential imperative programming. (3) Understand how to combine these theories.
• Course Syllabus.  We introduce Unifying Theories of Programming as a uniform foundation for all these paradigms. We give a tutorial introduction to an alphabetized version of Tarski's relational calculus. We show how this leads to a simple denotational semantics of a language of terminating programs, and show that they form a complete lattice. We extend this work to Hoare-He designs, a relational model of pre- and post-condition specifications, exploring the space of designs as a sub-theory of relations characterized by certain healthiness conditions. Then we turn our attention to another relational sub-theory (reactive processes) once again characterized by healthiness conditions. Finally, we show that the reactive image of the design lattice gives a suitable semantic model for CSP. We end by comparing this semantics with the standard failures-divergences model for CSP. 

Cours VII (10 Mars - 14 Mars)
Application in the Verification of security protocols
Enseingant Adel Bouhoula (Sup'Com, Tunis)
Support

• Course Objectives.Algebraic specifications provide a powerful method for the specification of abstract data types in programming languages and security software systems. Often, algebraic specifications are built with conditional equations. Semantically, the motivation for this is the existence of initial models; operationally, the motivation is the ability to use term rewriting techniques for computing and automatic prototyping. The formal development of a system might give rise to many proof obligations. We must prove the completeness and the ground confluence of the specification and the validity of some inductive properties. In this lecture, we will present procedures to test sufficient completeness and ground confluence and to prove or disprove inductive properties. Algebraic specifications and formal methods are also used to analyze and verify security protocols which allow agents to communicate securely over an insecure network. We will give in the last part of this lecture some techniques both for the verification of security protocols and for identifying attacks on faulty protocols.

• Course Objectives.  Category theory studies properties of algebraic structures by abstracting away from specific structures and focusing instead on their generic properties.  The study of relational categories allows us to investigate general properties of relational algebras, which we then apply to specific practical problems such as verification, refinement, graph transformations, and the composition of complex specifications from tabular expressions.
• Course Syllabus. 1. Tabular notation for software documentation. 2. Conventional semantics of tabular expressions. 3. Algebraic presentation of tabular expressions. 4. Table transformation theorems. 5. Recent developments in table foundations and applications.

• Course Objectives. The need for cybersecurity arises when three conditions are met: 1) High Stakes, i.e. we have a valuable (physical or logical) resource to protect. 2) High Vulnerability, i.e. it is impossible to ensure the resource is protected without disrupting the system operation. 3) High Threat, i.e. perpetrators are intent on gaining access to the resource and possibly damaging it, whether through malice or criminal intent. In today’s computing environment, we are experiencing higher stakes (as the larger and larger sectors of the economy are moving online), higher vulnerability (as the predominant computing paradigm is distributed computing, and modern system architectures favour component autonomy), and higher threats (as perpetrators grow more sophisticated). This makes cybersecurity one of the most critical areas of research in computing for the foreseeable future.

Cours X (7 Avril – 11 Avril)
Verification and Validation of Adaptive Systems
Enseignant J. Schumann (NASA Ames Research center, USA)

• Course Objective. Adaptive and learning systems are nowadays found in many safety-critical areas (e.g. aircraft, automotive industry, chemical and nuclear industry). Often based on neural networks such system provide advanced capabilities of data analysis and control in the face of change (e.g., to control a damaged aircraft). Due to their nonlinear and dynamic nature, however, verification and validation of such systems pose substantial issues and require novel methods and tools. This course will provide a background on the basic principles of artificial neural networks and machine learning systems and its applications, in particular in safety-related areas and it will provide detailed information on methods and tools for the verification and validation of such systems.
• Course Syllabus.   1:  Basic principles underlying artificial neural networks.  An overview of learning paradigms, common neural network architectures. Neural Networks and (Bayesian) statistics.  2: Adaptive Control Systems, architectures and applications.  Verification and Validation of Adaptive Systems, traditional V&V methods, V-shaped diagram, shortcomings of traditional methods.  3:  The three Laws of Adaptive Control.  Lyapunov stability Analysis (Overview).  Detailed working Example.  4:  Assessment of NN-based systems, quality of solution, why doesn't it learn/converge? does it generalize?  how to test NNs?  Tools for NN assessment and monitoring.  5:  Toward certification of adaptive systems.   Advantages and limits of adaptive systems and neural networks.  6.  During the course, some practical examples will be discussed.

• Course Objectives.  Relational algebra has been used for software and program analysis as well as for data mining. In this course, we define different kinds of dependencies in a relational database (functional and difunctional dependencies,…).  This study should help the designer to find some normalized database structures. However these proposed structures are fixed at the design step before the creation of the different instances of a database. Another deeper analysis of the current database instance is needed for a better data understanding. For that purpose, generally, a data reverse engineering process should generate a structure (from different kind of data) through which we may browse to find searched information in a short time. Using concept analysis, we may derive a lattice of formal concepts in a database instance, from which we may extract a set of dependencies (association rules). Putting in equation a request in a database, we discover the exact meaning of an atomic  information as a concept in a lattice structure. From the definition of Galois connection in a binary context, we will also propose some algorithms to reduce a context without losing knowledge, with different precision levels. The proposed study of different dependencies in a database will be used as a starting point to generate dynamically a browsing structure from a text or database. We will be able to illustrate the course by the design of Text pre-reader for a human, a conceptual meta-search engine generation  and a conceptual inference engine.  In this course, we will present different applications of conceptual dependencies in software engineering, machine learning, data reduction, information retrieval, and web engineering.
• Course Syllabus. 1.   Discrete Mathematics (Relational Algebra, Fuzzy relations, Lattice of concepts).  2. Dependencies in the relational Data Base.  (Functional and Difunctional Dependencies in a Relational Database). 3. Construction of the Lattice of Concepts.  4. Knowledge Extraction based on the lattice of concepts.  5.    Concept Generalization and Data Reduction, (Fuzzy Difunctional Dependencies, Fuzzy Concept, Conceptual Crisp and fuzzy binary Relation Reduction).  6. Conceptual Information structuring.  7. Applications of Conceptual Decomposition of a Binary relation (Automatic Text Reader, Design of Conceptual Meta-Search Engine, Learning Machine, Software Decomposition…).

      Cours XII (21 Avril - 25 Avril)
Event-B and the Rodin Platform
Enseignant J. R. Abrial (ETH, ZURICH)

Support 1  Support 2   Support 3
Support 4 
Support 5  Support 6

• Abstract.  This course is an introduction to the construction of complex systems
  using Event-B and the Rodin Platform. Event-B is a mathematical formalism (based on first-order logic and set theory) used to develop formal models of discrete transition systems.
  These models are elaborated before effectively building these systems which are thus intended to be correct by construction.
  Discrete transition system is the unifying paradigm which can be used in many different areas: sequential, distributed, concurrent, parallel. It
  also covers larger systems where one takes into account not only the future software but also its (fragile) environment.
  Models are made of constants and variables related by possibly complex invariants. Their dynamics is defined by means of transitions (called
  events) made of guards (the enabling conditions) and actions (supposed to modify variables in parallel).
  Models are developed by means of successive refinements steps: from quite simple and abstract to very concrete. When a model becomes too
  complicated, it can be decomposed into smaller ones communicating in a systematic fashion.
  Proofs and model-checking are performed at each step of the development. They insure that each model is coherent and that it indeed
  refines its abstraction (if any).
  The Rodin Platform is the tool set which has been developed (as funded by the European Project Rodin) to ensure a mechanical aid to the user of
  this approach. This platform is open source and implemented on Eclipse.
  It works on Windows, Linux and Mac-OS. It contains a database support which contains the developed models. This database is surrounded by
  various plugins: provers, model-checkers, animators, UML transformers, etc. New plugins can be added.
  The intent of the course is to explain all this in greater details by means of various practical examples and tool demonstrations.

Calendrier

14 Mars - 18 Avril :

Lieu des cours

Les cours ont lieu dans la salle "Chaire Unesco", au 1er étage de la Tour Osman Bahri, à l'Enit (Ecole Nationale des Ingénieurs de Tunis), du lundi au vendredi à partir de 9h du matin.

 Inscription
Attendance is free, but candidates must apply for admission by completing the registration form (.doc) and mailing it to : 

Contact

Rahma Ben Ayed
UnescoChair6@enit.rnu.tn
SysCom - ENIT
1002 TUNIS BELVÉDÈRE
TUNISIE
Téléphone : (+216) 71 87 26 79