middleware_for_ubiquitous_computing_course
Différences
Ci-dessous, les différences entre deux révisions de la page.
Les deux révisions précédentesRévision précédenteProchaine révision | Révision précédenteDernière révisionLes deux révisions suivantes | ||
middleware_for_ubiquitous_computing_course [2009/12/03 09:08] – tigli | middleware_for_ubiquitous_computing_course [2010/01/17 09:58] – tigli | ||
---|---|---|---|
Ligne 2: | Ligne 2: | ||
====== Middleware for Ubiquitous Computing ====== | ====== Middleware for Ubiquitous Computing ====== | ||
{{: | {{: | ||
- | ====== Course 1 ====== | ||
- | ===== Introduction ===== | + | [[Course 1 |Draft Course 1]] |
- | ==== What does Traditional Middleware Mean ? ==== | + | [[Course |
- | + | ||
- | === Motivations === | + | |
- | + | ||
- | * make development faster and easier | + | |
- | + | ||
- | * to assist distributed software | + | |
- | + | ||
- | * promoting software reuse | + | |
- | + | ||
- | * A bridge between OS and application | + | |
- | + | ||
- | * High level network abstractions matching the application computational model | + | |
- | + | ||
- | === First Definitions === | + | |
- | + | ||
- | === Middleware Taxonomies === | + | |
- | + | ||
- | * W. Emmerich Taxonomy (2000) | + | |
- | * D.E. Baken (2001) | + | |
- | * R. E. Schantz and D. C. Schmidt Taxonomy (2002) | + | |
- | + | ||
- | == Transactional Middleware == | + | |
- | == Tuplespace-based Middleware == | + | |
- | == Message-oriented Middleware == | + | |
- | == Remote procedure Calls Middleware == | + | |
- | == Object oriented Middleware == | + | |
- | + | ||
- | == Component oriented Middleware == | + | |
- | == Service-oriented Middleware == | + | |
- | + | ||
- | === Exercices === | + | |
- | + | ||
- | + | ||
- | === References === | + | |
- | + | ||
- | A Perspective on the Future of Middleware-based Software Engineering. | + | |
- | + | ||
- | [[http:// | + | |
- | + | ||
- | ==== What does Ubiquitous Computing Mean ? ==== | + | |
- | + | ||
- | + | ||
- | === Exercices === | + | |
- | + | ||
- | === videos === | + | |
- | + | ||
- | The following scenes together are a complete [[http:// | + | |
- | + | ||
- | === References === | + | |
- | + | ||
- | GATECH | + | |
- | + | ||
- | + | ||
- | ==== What does Middleware for Ubiquitous Computing Mean ? ==== | + | |
- | + | ||
- | === New motivations === | + | |
- | + | ||
- | * High level device and ressource abstractions matching the application computational model | + | |
- | * device and ressource abstraction is often transparency in multiple access | + | |
- | * Distribution with or without nertwork ... | + | |
- | + | ||
- | === Example in distributed systems === | + | |
- | + | ||
- | === Example in OS and Virtual Machine | + | |
- | + | ||
- | === Example in HMI === | + | |
- | + | ||
- | * application computational model : widgets | + | |
- | * low level device drivers : mouse and screen | + | |
- | * Middleware : | + | |
- | + | ||
- | === Example | + | |
- | + | ||
- | + | ||
- | ==== Trends on the future of Middleware ==== | + | |
- | + | ||
- | ==== From Mobility to Ubiquity | + | |
- | + | ||
- | ==== New Requirements | + | |
- | + | ||
- | === Exercices === | + | |
- | + | ||
- | === Projets de recherche : === | + | |
- | OpenCOM and ReMMoC Web Page, Paul Grace and Gordon S. Blair - [[http:// | + | |
- | + | ||
- | ARLES Project-Team, | + | |
- | + | ||
- | Project AMAZONES, Citi Lab, INSA Lyon, Frenot Stéphane, Le Mouel Frédéric | + | |
- | + | ||
- | + | ||
- | ====== | + | |
- | + | ||
- | There are currently two families of formal methods. These two approaches are complementary. | + | |
- | + | ||
- | ===== Proof-based verification ===== | + | |
- | + | ||
- | Example : such as B or Z | + | |
- | + | ||
- | In proof-based methods, the model is described by | + | |
- | means of axioms, properties are theorems to be verified using a theorem prover. | + | |
- | + | ||
- | Proof-based techniques allow the analysis of infinite systems. However, the use of a theorem prover is a very difficult | + | |
- | + | ||
- | + | ||
- | ===== Model-checking ===== | + | |
- | + | ||
- | + | ||
- | Example : such as Spin or Lustre. | + | |
- | + | ||
- | In model checking, the model is expressed using a language from which an exhaustive | + | |
- | execution can be computed (this usually requires a mathematically based | + | |
- | definition). An “execution engine” produces the exhaustive state space associated | + | |
- | to the system as a graph where actions (atomic instructions in the language) relate | + | |
- | to states (a given possible value of the system’s context). It is then possible to | + | |
- | explore the graph to check if a property is satisfied. | + | |
- | + | ||
- | + | ||
- | Model checking is dedicated to finite-state systems but modeling and verification can be done using graphical toolkits and most steps can be automated | + | |
- | + | ||
- | + | ||
- | ===== References ===== | + | |
- | + | ||
- | On the Formal Verification of Middleware Behavioral Properties, Jérôme Huguesa, Thomas Vergnauda, Laurent Pauteta, Yann Thierry-Miega, | + | |
- | + | ||
- | ====== Course 3 ====== | + | |
- | + | ||
- | + | ||
- | ===== ACME ===== | + | |
- | + | ||
- | [[http:// | + | |
- | + | ||
- | [[http:// | + | |
- | + | ||
- | [[http:// | + | |
+ | [[Course 3 |Draft Course 3]] | ||
====== References : ====== | ====== References : ====== | ||
Ligne 286: | Ligne 152: | ||
[[https:// | [[https:// | ||
- | |||
- | |||
- | |||
middleware_for_ubiquitous_computing_course.txt · Dernière modification : 2010/01/17 10:00 de tigli