Draft Course 1

Draft Course 2

Draft Course 3

A Perspective on the Future of Middleware-based Software Engineering. V. Issarny, M. Caporuscio, N. Georgantas. In Future of Software Engineering 2007 (FOSE) at ICSE (International Conference on Software Engineering). L. Briand and A. Wolf editors, IEEE-CS Press. 2007. link

E-book: Middleware Architecture with Patterns and Frameworks, Prof. Sacha Krakowiak

A Survey on Service Composition Middleware in Pervasive Environments Ibrahim N., Le Mouël F. International Journal of Computer Science Issues (IJCSI) 1 (2009) 1–12 link

Middleware Technologies for Ubiquitous Computing, Ibrahim N., Le Mouël F., Frénot S, in Handbook of Research on Next Generation Networks and Ubiquitous Computing, IGI Global Publication (Ed.) (2009)

Middleware for Robotics: A Survey, Mohamed, N. Al-Jaroodi, J. Jawhar, I., Coll. of Inf. Technol., United Arab Emirates Univ., Al Ain in 2008 IEEE Conference on Robotics, Automation and Mechatronics,21-24 Sept. 2008, p. 736-742, Chengdu, ISBN: 978-1-4244-1675-2 link

http://www.hydramiddleware.eu/hydra_papers/A_Survey_of_Context-aware_Middleware.pdf

http://www.sce.carleton.ca/wmc/middleware/middleware.pdf

http://hal.archives-ouvertes.fr/docs/00/32/64/79/PDF/ACI08-INRIA-TechRep.pdf

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.1.9321&rep=rep1&type=pdf http://users.cis.fiu.edu/~sadjadi/Publications/AdaptiveMiddlewareSurvey.ps

https://rainbow.i3s.unice.fr/~tigli/References/Autre/2CACB8FEd01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Autre/8E123188d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Autre/C11.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Autre/RapportIntellAmbiante.V1.2finale.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/07937E4Fd01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/1C34FA30d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/2EE1E94Bd01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/7CCDDAE4d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/A_Survey_of_Context-aware_Middleware.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/CCF19AA4d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/Crowley Model

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/Crowley-OULU04.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/D68D6526d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/DEB4F9F9d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/F7827FE3d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/Survey

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/UBIMOB06-Vachet-Laurillau.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Context-aware/p19-bolchini.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Middleware_and_AOP/survey-aspect middleware.pdf

https://rainbow.i3s.unice.fr/~tigli/References/PhD/Dissertation.pdf

https://rainbow.i3s.unice.fr/~tigli/References/PhD/these cheung.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Projets_europeen_Context-aware/BE7149EFd01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Projets_europeen_Middleware/210C9626d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Projets_europeen_Middleware/FAC2E264d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Projets_europeen_Middleware/PLASTIC_D3_1.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Slides_context_aware/context-aware.ppt

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/AOSA.pdf.filepart

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/CA200725d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/DAIS07.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/DOC191109.pdf.filepart

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/EDOC-AOMDF-draft.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/EIWAS2005-Remi Douence.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/France09a.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/Morin09a.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/analysis design approaches aop.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/cheung.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/fulltext.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/klein06b.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/middleware08.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/p79-douence.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/rr-inria-5873.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_AOP/survey-aspect middleware.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/1C34FA30d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/5C1AC68Ad01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/7414AB5Fd01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/780A807Ad01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/89DC2B9Dd01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/9BDA84E0d01ressource.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/ABDEF341d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/A_Survey_of_Context-aware_Middleware.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/BBDE183Dd01sensnet.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/C7E487D0d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/DE10D1F0d01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/ROMEROPaper.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/a3-grace.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/chapitre.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/middleware-chapter.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Survey_Middleware/schmidt_middleware.pdf

https://rainbow.i3s.unice.fr/~tigli/References/Ubiquitous_Computing/pcs01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/slides_Middleware/F50FA17Ed01.pdf

https://rainbow.i3s.unice.fr/~tigli/References/slides_Middleware/IWAN05-Dobson.pdf

PLASTIC5, European Commission under FP6 contract numbers 026955, link

AMIGO6 IST, European Commission under FP6 contract numbers 004182, link

There are currently two families of formal methods. These two approaches are complementary.

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 and a very technical task that is hard to automate.

• Abrial, J., “Z: an introduction to formal methods,” Cambridge University Press, 1995.
• Diller, A., “The B-book,” John Willey & SONS, 1994.

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

• Halbwachs, N., A tutorial of Lustre (1993).

From Testing ... through Static Analysis... to Formal Verification (Annie Ressouche)

Software : Lustre V4 / Lesar Distribution

Lustre/Lesar V4 for cygwin

This distribution is experimental.

It requires a recent, fully installed version of the cygwin system for Windows (gcc, g++, tcl/tk etc).

Within a cygwin shell, extract the archive (typically in /usr/local). Modify your bashrc file with:

export LUSTRE_INSTALL=/usr/local/lustre export PATH=$LUSTRE_INSTALL/bin:$PATH export MANPATH=$MANPATH:$LUSTRE_INSTALL/man:

windows beta distribution

An overview of NuSMV

NuSMV is a software tool for the formal verification of finite state systems. It has been developed jointly by ITC-IRST and by Carnegie Mellon University.

NuSMV allows to check finite state systems against specifications in the temporal logic CTL. The input language of NuSMV is designed to allow the description of finite state systems that range from completely synchronous to completely asynchronous. The NuSMV language (like the language of SMV) provides for modular hierarchical descriptions and for the definition of reusable components. The basic purpose of the NuSMV language is to describe (using expressions in propositional calculus) the transition relation of a finite Kripke structure. This provides a great deal of flexibility, but at the same time it can introduce danger of inconsistency (for non expert users).

• On the Formal Verification of Middleware Behavioral Properties, Jérôme Huguesa, Thomas Vergnauda, Laurent Pauteta, Yann Thierry-Miega, Soheib Baarira, and Fabrice Kordona, Electronic Notes in Theoretical Computer Science, Elsevier editor, Volume 133, 31 May 2005, Pages 139-157, Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004)