Sixth  Semester of the UNESCO Chair

Discrete Mathematics and Logic:

Foundations and Applications in Software Specification, Analysis and Design

Tunis, January 28th -April 25th, 2008

COORDINATORS : Ali MILI (NJIT, USA), Rahma BEN AYED (ENIT-SysCom/University Tunis el Manar)

page d'accueil

Speakers

Program of the course

General calendar

Audience and pre-requisites

Registration

Financial aid(.doc)

Contact

Objective of the Course

According to Harlan D. Mills (1919-1996), IBM Fellow, continuous mathematics model natural phenomena whereas discrete mathematics model human made artifacts.  Given that computing is the fruit of human imagination and creativity, discrete mathematics are an ideal tool to model its products and processes.  The goal of this course is to present a number of branches of discrete mathematics, along with their computing applications.   Historically, the development of these models has not preceded the development of their application domains; more typically, a need emerges and ad-hoc solutions are composed to fulfill it, then mathematical models are subsequently developed to better understand the problem, and better manage/ control the derivation of its solution. For obvious pedagogical motives, we present the mathematical models and highlight their integrity and intrinsic interest, then we discuss some important application thereof.

Language of Instruction

Speakers

A. Mili (NJIT and Rutgers University, USA)
Lecture I (28 janvier – 1er février / January 28 -February 1st)
Discrete Structures and Refinement Calculi
Biography. A. Mili holds a PhD from the University of Illinois at Urbana, USA, and a Doctorate es-Sciences d’Etat from the Universite Joseph Fourier de Grenoble, France. He is a Professor at NJIT (Newark, NJ) and a faculty member of the graduate school at Rutgers Newark. He has authored or co-authored two books in Arabic, five books in English, thirteen book chapters, and about 180 papers in journals and conferences. He has served on the editorial board of TSI (in French), IEEE-TSE and JSS, and is currently serving on the board of "Innovations in Systems and Software Engineering: a NASA Journal".

R. Ben Ayed (ENIT / SysCom Lab, Tunisia)
Lecture II (4-8 février / February 4th -February 8th)
Formal Methods
Biography. Rahma Ben Ayed earned the Doctorat de Troisieme Cycle from the Faculty of Sciences of Tunis in 1990 and the Habilitation from the Engineering School in 2005. She is currently a professor of Computing and Telecommunications at ENIT (Engineering School of Tunis) and member of SysCom Research Laboratory. Her research interests are in software engineering, including formal methods of specification, verification, and their application in telecommunication systems. She has served on program and organisation committees of several international conferences.

K. Barkaoui (CNAM-Paris, France)
 Lecture III (11-15 février / February 11th – February 15th)
Specification & Verification of Distributed Systems (1)
Biography. Kamel Barkaoui received a Ph.D. degree in Computer Science in 1988 from the University Paris 6. He is currently a Professor at the Conservatoire National des Arts et Métiers (CNAM - Paris). His research interests include formal verification techniques and performance evaluation methods of concurrent and distributed systems with applications to computer and communication systems. He received the 1995 IEEE Int. Conf. on System Man and Cybernetics Outstanding Paper Award. Dr Barkaoui has served on PCs and as PC chair for numerous international workshops and conferences and was a guest editor of Journal of Systems and Software and of Formal Aspects Computing Journal.

 J.M. Ilié and D. Poitrenaud (Université Paris 5 / LIP6 Lab, France)
Lecture IV (18-22 février / February 18th – February 22th)
Specification & Verification of Distributed Systems (2)
Biography.  Jean-Michel Ilié is currently Associate Professor of Computer Science at the University René Descartes, Paris, and Associate Researcher at the University Pierre and Marie Curie, Paris, France. His research aims at elaborating efficient techniques to improve the verification and evaluation tools of concurrent systems. Topics are currently oriented to the correct design of time specifications. Dr. Ilié served in numerous journal and conference PCs, has been invited in Italian and Algerian universities. In 2005, he received the Best Paper Award of the Int. QEST Conference.
Biography. Denis Poitrenaud earned a PhD at the University Pierre and Marie Curie, Paris, France, in 1996. He is currently Associate Professor of Computer Science at the University René Descartes, Paris, France and Associate Researcher at the University Pierre and Marie Curie, Paris, France. His research interests include the design and verification of concurrent systems. He develops techniques and algorithms to limit the state explosion problem by using partial order reductions as well as symbolic approaches. Morever, he studies the expressive power of specifiaction languages for infinite systems.

M. Kaâniche (LAAS-CNRS, France)
Lecture V (25-29 février / February 25th – February 29th)
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.

J. Woodcock (University of York, UK)
Lecture VI (3-7 mars / March 3th – March 7th)
Unified Theory of programming
Biography. Jim Woocock gained his PhD from the University of Liverpool. Until 2001 he was Professor of Software Engineering at the Oxford University Computing Laboratory, where he was also a Fellow of Kellogg College. He then joined the University of Kent. He is now based at the University of York. His research interests include: strong software engineering, Grand Challenge in dependable systems evolution, unifying theories of programming, formal specification, refinement, concurrency, state-rich systems, mobile and reconfigurable processes, nanotechnology, Grand Challenge in the railway domain. He has a background in formal methods, especially the Z notation and CSP. Woodcock worked on applying the Z notation to the IBM CICS project, helping to gain a Queen's Award for Technological Achievement, and Mondex, helping to gain the highest ITSECclassification level.

Adel BOUHOULA (Sup'Com, Tunis)
Lecture VII (10-14 mars / March 10th – March 14th)
Application in the Verification of security protocols 

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.

W. Kahl (McMaster University, Canada)
Lecture VIII (24-28 mars / March 24th – March 28th)
Tabular Expressions
Biography. Wolfram Kahl earned the PhD in at the Fakultaet fuer Informatik, Universitaet des Bundeswehr Muenchen, Germany, in 1995, and the Habilitation Thesis at Fakultaet fuer Informatik, Universitaet des Bundeswehr Muenchen, Germany, in 2001. He is currently Associate professor of Computer Science at the Department of Computing and Software at McMaster University in Hamilton, Ont. Canada. His research interests include Mathematically rigorous software design and verification, support for tabular expressions; Functional Programming and Program Transformation, pattern matching calculus (PMC); Relational Methods in Computer Science; and graph transformation, especially term graph transformation.

F. T. Sheldon (Oak Ridge National Lab, USA)
Lecture IX (31 mars – 4 avril / March 31th – April 4th)
Cybersecurity and Infrastructure Protection
Biography.Frederick Sheldon has 22 years of experience in the field of computer science and is currently a Senior Research Staff Member in the Cyberspace Sciences and Intelligence Information Research (CSIIR) group at Oak Ridge National Laboratory. Formerly, he was assistant  professor at WSU, CU and research staff at DaimlerChrysler, Lockheed  Martin, Raytheon and NASA Langley/Ames. He received Ph.D./MS at Univ. of Texas at Arlington in '89 (also has two degrees from Univ. of  Minnesota in Computer Science and Microbiology). He founded the Software Engineering for Secure and Dependable Systems Lab in 1999.  He is a Senior Member of the IEEE and member of ACM, IASTED, AIAA,  including the Tau Beta Pi and Upsilon Pi Epsilon honour societies  and has received the Sigma Xi award for an outstanding dissertation.   He has published over seventy papers in various journals and international conferences (http://www.ioc.ornl.gov/sheldon). His research has been concerned with developing and validating/testing  models, applications, methods and supporting tools for the creation of safe, secure and dependable software/systems.

J. R. Abrial (ETH, ZURICH)
Lecture XII (21 – 25 avril / April 21st – April 25th)
Event-B and the Rodin Platform
Biography. 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.

Program of the course

In the sequel we present the individual course descriptions, including a short synopsis, a syllabus, a relevant bibliography, and a biography of the lecturer.   These are ranked by chronological order of their delivery.

 Lecture I (January 28 -February 1st)
Discrete Structures and Refinement Calculi
Lecturer 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.

Lecture II (February 4th -February 8th)
Formal Methods
Lecturer 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.

 Lecture III (February 11th – February 15th)
Specification and Verification of Distributed Systems (First part)
Lecturer 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.

Lecture IV (February 18th - February 22th )
Specification and Verification of Distributed Systems (Second part)
Lecturer J.M Ilié and 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.

 Lecture V (February 25th- February 29th )
Dependability evaluation of computer-based systems
Lecturer 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.

    Lecture VI (March 3th-March 7th)
Unified Theory of programming
   Lecturer Jim Woodcock (University of York, UK)

http://www.unifyingtheories.org/

Contact for the support

• 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. 

Lecture VII ( March10th - March 14th )
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.

Lecture X (April 7th – April 11th)
Verification and Validation of Adaptive Systems
Lecturer 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…).

Lecture XII (April 21st - April 25th)
Event-B and the Rodin Platform
Lecturer J. R. Abrial (ETH, ZURICH)

Support 1  Support 2   Support 3

• 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.
  

April 14th - April 18th:

April 21th - April 25th:

Audience and pre-requisites

This course is geared towards a fairly large audience, including in particular computer scientists who are interested in theoretical foundations of their discipline and mathematicians interested in computing applications of their discipline.  Specialists from other branches of sciences (Physics, Biology, etc) and engineering (mechanical, civil, electrical, etc) who have the agility and the motivation to explore a new discipline may find this course of some interest.  Overall, we require/ expect participants to have an undergraduate degree in mathematics, computer science or related field, but may adjust the course material to the profile of the class.

Registration

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

Applications must be received by December 10.
Notifications of admission and/or financial aid will be sent out by December 29.
Lectures start January 28.
Spring Break: March 17-21.
Lectures conclude April 25.

Financial aid

We anticipate to offer a large number of scholarships that cover travel expenses and local expenses, totally or
partially, accordiang to candidate needs, condidate interest, and availability of funds. Interested candidates are
encouraged to accompany their application for admission with application of financial aid.

We propose to offer a financial support for 2 or 3 Tunisians to cover  local expenses. Contact UnescoChair6@enit.rnu.tn.

Contact
Rahma Ben Ayed
UnescoChair6@enit.rnu.tn
SysCom - ENIT
1002 TUNIS BELVEDERE
TUNISIA
Telephone : (+216) 71 87 26 79