http://fm2011.lero.ie
June 20 - 24, 2011
Lero, Limerick, Ireland
Sunday, December 12, 2010
Tuesday, November 30, 2010
Structures de données et méthodes formelles, Marc Guyomard, Springer
Ce livre porte sur l’étude des structures de données, à savoir des constituants logiciels dont la qualité conditionne le bon fonctionnement et l’efficacité des applications informatiques. L’originalité de cet ouvrage réside essentiellement dans le lien qu’il établit avec la discipline des méthodes formelles pour le génie logiciel. Il montre comment il est possible de calculer les opérations qui accompagnent une structure de données à partir d’une spécification rigoureuse. L’auteur adopte à la fois une perspective historique et une démarche fonctionnelle. La première partie de l’ouvrage présente les bases de la discipline : la théorie des ensembles, l’étude de structures intermédiaires (listes, arbres, sacs), et l’analyse des algorithmes. La seconde partie se focalise sur l’étude approfondie de cinq structures de données typiques : les ensembles simples, les ensembles composites, les files simples, les files de priorité, et les tableaux flexibles. Des exercices accompagnent chaque chapitre.
1st Edition., 2011, 426 p., Broché
ISBN: 978-2-8178-0199-5
ISBN: 978-2-8178-0199-5
Monday, November 29, 2010
Décès de Michel Sintzoff
http://www.ae-info.org/ae/User/Sintzoff_Michel
On m'apprend :" C'est avec une très grande tristesse que j'ai appris ce lundi le décès de Michel Sintzoff.
Michel était une personnalité exceptionnelle de la recherche en Informatique. Sa curiosité scientifique l'avait amené à travailler dans de nombreux domaines de notre discipline (Langages, Intelligence Artificielle, Bases de Données, Génie Logiciel, Informatique Distribuée,...).
Il avait des amis partout dans le monde, et donc naturellement en France (à Paris, Toulouse, Nancy, Grenoble,...).Beaucoup se souviendront de son ouverture d'esprit, de la pertinence de ses remarques et de son rire inimitable. "
Wednesday, October 20, 2010
FSEN '11
Fourth International Conference on Fundamentals of Software Engineering 2011 Theory and Practice (FSEN '11) http://fsen.ir/2011/fsen.ir/2011 Tehran, Iran April 20-22, 2011
Cours et exercices corrigés d'algorithmique
Vérifier, tester et concevoir des programmes en les modélisant,
Jacques Julliand
Vuibert, 2010
Utilise la notation B.
http://www.vuibert.com/livre33767.html
Jacques Julliand
Vuibert, 2010
Utilise la notation B.
http://www.vuibert.com/livre33767.html
Death of Jean-Claude Laprie
Dear colleague, With deep sadness we bring you the news of Jean-Claude
passing away after a battle with cancer,
Saturday night (October 17). The funeral arrangements are not settled yet.
More information will be provided when available. TSF group at LAAS
Thursday, October 7, 2010
THE PROGRAMMING LANGUAGE B
"B is a computer language designed by D. M. Ritchie and K. L.
Thompson, for primarily non-numeric applications such as system
programming. These typically involve complex logical decisionmaking,
and processing of integers, characters, and bit strings.
On the H6070 TSS system, B programs are usually much easier to
write and understand than assembly language programsj and object
code efficiency is almost as good. Implementation of simple TSS
subsystems is an especially appropriate use for B."
http://minnie.tuhs.org/Mirrors/Dennis/btut.pdf
Thompson, for primarily non-numeric applications such as system
programming. These typically involve complex logical decisionmaking,
and processing of integers, characters, and bit strings.
On the H6070 TSS system, B programs are usually much easier to
write and understand than assembly language programsj and object
code efficiency is almost as good. Implementation of simple TSS
subsystems is an especially appropriate use for B."
http://minnie.tuhs.org/Mirrors/Dennis/btut.pdf
The formal method known as B and a sketch for its implementation
Antti-Juhani Kaijanaho
Master's Thesis
in Information Technology (Software Engineering)
20th December 2002
http://users.jyu.fi/~antkaij/gradu.pdf
Master's Thesis
in Information Technology (Software Engineering)
20th December 2002
http://users.jyu.fi/~antkaij/gradu.pdf
Security of Computer Architectures, Jean-Louis Boulanger
- Relié: 512 pages
- Editeur : ISTE Ltd and John Wiley & Sons Inc (16 juillet 2010)
- Langue : Anglais
- ISBN-10: 184821197X
- ISBN-13: 978-1848211971
- http://eu.wiley.com/WileyCDA/WileyTitle/productCd-184821197X.html?cid=RSS_WILEY2_ENGINEERING
Le dernier livre d'Umberto Eco en français
http://www.bibliosurf.com/De-l-arbre-au-labyrinthe
Dall'albero al labirinto. Studi storici sul segno e l'interpretazione
Studi storici sul segno e l’interpretazione
http://bompiani.rcslibri.corriere.it/libro/5902_dall_albero_al_labirinto_studi_eco.html
Autore: Umberto Eco
Titolo: Dall'albero al labirinto. Studi storici sul segno e l'interpretazione
Editore: BOMPIANI
Collana: STUDI E STRUMENTI
Pagine: 640
Prezzo: 25,00 euro
Anno prima edizione: 2007
ISBN: 45259029
Tuesday, June 15, 2010
Workshop on B Dissemination
Workshop on B Dissemination November 8-9, 2010 Natal, Brazil http://www.bmethod.com/php/conference-sbmf-2010-en.php Satellite event of SBMF 2010 <
http://sbmf2010.dimap.ufrn.br/> Presentation This B / event-B workshop is organized on behalf of the
DEPLOY project <http://www.deploy-project.eu/>.
Its objectives are to present current status and ongoing research and development related to B and
event B languages and tools, as well as applications to industry size problems. Topics addressed by the workshop are many,
including but not limited to: * Tool development (language extensions,
external provers, code generation, etc.) * Modelling challenges (real time properties, probabilistic refinement, design patterns, high order logic, etc.) * Deployment (methodology, cases-studies, return of experience, scaling up, etc.) * Teaching and training Researchers are invited to contribute to the
second day of the workshop
through an open call for papers.
Program
The workshop lasts 2 days:
* The first day is devoted to DEPLOY speakers. General presentation of the project and tools will be sided by
focused talks on scientific/technical matters (modelling time, code generation,
model animation, model checking, etc.) that are being researched in DEPLOY. Reports on industrial applications (space,
railways, automotive, information systems, etc.) will complete the day. * The second day is open to any presenter,
through an international call for papers. Expected contributions would
range from theoretical research to practical applications of B/event B.
Submissions are handled by the programme committee. The workshop is collocated with the SBMF
conference (Monday and Tuesday), at the Imira Plaza hotel <
;http://www.imiraplaza.com.br/>. Important Dates * Paper submission deadline: 30 July 2010 * Notification of acceptance/rejection:
06 September 2010 * Workshop in Natal, Brazil: 08-09 November 2010 Submission and attendance We anticipate a rich exchange of ideas and discussions
during this event. Submissions are welcomed on any
subject that falls within the main issues. Papers should be around 6 pages in ENTCS style. All papers must be submitted in PDF format,
following the instructions at the WOBD'10 submission
site, handled by EasyChair: http://www.easychair.org/conferences/?conf=wobd2010. All accepted papers should be presented during the workshop. Committees Workshop Chair: * Thierry Lecomte <
mailto:thierry.lecomte@clearsy.com> (ClearSy) Program Committee: * Michael Butler (University of Southampton, UK) * Clif Jones (University of Newcastle, UK) * Jérôme Phalampin (Siemens Transportation Systems, France) * Lilian Burdy (ClearSy, France) * David Basin (ETH Zurich, Switzerland) * Michael Leuschel (University of Dusseldorf, Germany) * Mathieu Clabaut (Systérel, France) * Christophe Ponsard (CTIC, Belgium) * Elena Troubitsyna (University of Turku, Finland) * Rainer Gmehlich (Bosch, Germany) * Aryldo Russo (AeS, Brazil)
Tuesday, June 8, 2010
B方法 , The B Book in chinese
http://www.china-pub.com/19779
基本信息
- 作者： [美]Jean-Raymond Abrial, J.-R. Abrial [作译者介绍]
- 译者： 裘宗燕[同译者作品]
- 丛书名： 国外计算机科学教材系列
- 出版社：电子工业出版社
- ISBN：7505393391
- 上架时间：2004-7-1
- 出版日期：2004 年6月
- 开本：16开
- 页码：526
- 版次：1-1
- 所属分类： 计算机 > 软件工程及 软件方法学 >
综合
教材 > 研究生/本 科/专科教材 > 工学 >
计算机
教材 > 计算机教材 > 本科 /研究生 > 计 算机专业 > 计 算机专业课程 >
软件工程
General-Service Ballistic Computer Programming Based on B-Method
"Formal methods offer the promise of significant improvement on quality and reliability of critical embedded software. B-Method is employed to develop general-service ballistic computer programs in the paper, each of which can be adapted to a family of service/weapon-specific ballistic computers. Based on the structuring mechanisms of B-method, a unified approach is proposed to systematically control the complexity of ballistic parameters in the process of type and operation refinement, and ultimately a series of high reliable, reusable, and scalable programs are produced. Experiences with the application of the method and tools are also discussed."
http://d.wanfangdata.com.cn/Periodical_bgxb-e200603005.aspx
http://d.wanfangdata.com.cn/Periodical_bgxb-e200603005.aspx
Monday, May 10, 2010
Sunday, May 9, 2010
Programme of the 2010 conference
http://www.lina.sciences.univ-nantes.fr/apcb/BDayNantes2010/programme_tfmb2010.html
9h00 – 10h00 : Conférence invitée / Invited Talk
Formal proofs of local computation systems, using Rodin and/or Coq
12h15-12h50 : B for Children
8:30-9:00 Welcome
9h00 – 10h00 : Conférence invitée / Invited Talk
Formal proofs of local computation systems, using Rodin and/or Coq
Pierre Castéran, Université de Bordeaux, LaBRI, FR
10h00 – 10h15 : Pause / Break
10h15 – 10h50 : Teaching Logic Proofs for Formal Aspects
David Cumbor, Bill Stoddart, Steve Dunne, University of Teesside, UK
10h50 – 11h25 : Using the B Method in Teaching Software Technology at Eötvös Lorànd University
Akos Fothi, Zoltan Istenès, Eötvös Lorànd University, HU
11h25- 11h40 Pause / Break
11h40 – 12h15 : New Features of Atelier B 4.0
Thierry Lecomte, ClearSy, Aix-en-Provence, FR
12h15-12h50 : B for Children
Mireille Samia, University of Dusseldorf, GE
12h50 – 14h00 : Déjeuner / Lunch
Visite de stands / Visit of stands
14h00 – 15h00 : Conférence invitée / Invited Talk
Development of a Network Topology Discovery Algorithm
Jean-Raymond Abrial, Consultant, Marseille, FR
15h30 – 16h05 : The Teaching of Data Structures: a Balanced Presentation of Skew Heaps
Marc Guyomard, ENSSAT, Université de Rennes, FR
16h05-16h20 : Pause / Break
16h20 – 17h00 : Ten Years Disseminating the B Method,
Thierry Lecomte, ClearSy, Aix-en-Provence, FR
Friday, April 30, 2010
Jean-Raymond Abrial, conference in Nantes on June 7, 2010
Jean-Raymond Abrial is invited for the 2010 conference. The new book of J.R. Abrial will be available for the conference.
Contents
Prologue: faultless systems – yes we can!; Acknowledgements; 1. Introduction; 2. Controlling cars on a bridge; 3. A mechanical press controller; 4. A simple file transfer protocol; 5. The Event-B modeling notation and proof obligations rules; 6. Bounded re-transmission protocol; 7. Development of a concurrent program; 8. Development of electronic circuits; 9. Mathematical language; 10. Leader election on a ring-shaped network; 11. Synchronizing a tree-shaped network; 12. Routing algorithm for a mobile agent; 13. Leader election on a connected graph network; 14. Mathematical models for proof obligations; 15. Development of sequential programs; 16. A location access controller; 17. Train system; 18. Problems; Index.Saturday, April 3, 2010
Conférences grand public JS 2010
L'un des objectifs des Journées Scientifiques de l'Université de Nantes est de diffuser la culture scientifique et technique.
Cette année, le thème de l'enfant et son éducation est à l'honneur.
Les conférences et la table ronde programmées sont gratuites et accessibles à tous.
Cette année, le thème de l'enfant et son éducation est à l'honneur.
Les conférences et la table ronde programmées sont gratuites et accessibles à tous.
Programme prévisionnel
- 15h00-15h45 : Conférence « Comment la connaissance vient aux bébés » par Roger LÉCUYER, Professeur émérite en psychologie de l'enfant, à l'Université Paris V, spécialiste des compétences périnatales
- 16h00-16h45 : Conférence « Stratégies familiales et politiques éducatives » par Agnès VAN ZANTEN, directrice de recherche au CNRS, à l'Observatoire Sociologique du Changement
- 17h00-18h00 : Table ronde sur le thème de l'enfant et son éducation avec Roger LÉCUYER, Agnès VAN ZANTEN, Jean-Christophe ROZÉ (Chef du service de médecine néonatale au CHU Nantes), Catherine CHOQUET (Adjointe au maire de Nantes en charge de la petite enfance, de la santé et des personnes handicapées) et Agnès FLORIN (Professeur en Psychologie de l'enfant et de l'éducation à l'Université de Nantes)
Tuesday, March 30, 2010
Death of Robin Milner
"Robin Milner, FRS FRSE
Professor Emeritus of Computer Science
It is with great sadness that we note the death of Robin Milner.
Robin worked at the Computer Laboratory in Cambridge from 1995 onwards, serving as Head of the Laboratory 1996–1999. Before that, he worked at the University of Edinburgh 1973–1994, where he was founding Director of the Laboratory for Foundations of Computer Science (LFCS). He was awarded the Turing Award in 1991.
Robin played a leading role in the development of many areas of Computer Science, focussing especially on its mathematical foundations but always with a sharp eye on practice. His intellectual legacy includes:
Always an inspirational teacher and colleague, and a warm-hearted man, he will be greatly missed."
Robin Milner visited Nantes on 2007 for a conference.
http://www.cl.cam.ac.uk/misc/obituaries/milner/
Professor Emeritus of Computer Science
It is with great sadness that we note the death of Robin Milner.
Robin worked at the Computer Laboratory in Cambridge from 1995 onwards, serving as Head of the Laboratory 1996–1999. Before that, he worked at the University of Edinburgh 1973–1994, where he was founding Director of the Laboratory for Foundations of Computer Science (LFCS). He was awarded the Turing Award in 1991.
Robin played a leading role in the development of many areas of Computer Science, focussing especially on its mathematical foundations but always with a sharp eye on practice. His intellectual legacy includes:
- machine-assisted proof construction with the LCF approach, underpinning the HOL and Isabelle/HOL provers;
- the design and formal definition of programming languages, especially of Standard ML, including work on type safety, type inference and module systems;
- models of concurrent computation, particularly with the CCS and Pi-Calculus process calculi and their theories of compositional reasoning; and
- the bigraph model of mobile informatic processes with its applications to bioinformatics and pervasive computing.
Always an inspirational teacher and colleague, and a warm-hearted man, he will be greatly missed."
Robin Milner visited Nantes on 2007 for a conference.
http://www.cl.cam.ac.uk/misc/obituaries/milner/
Saturday, March 20, 2010
Invited Speaker 2010
3rd International Conference From Research to Teaching Formal Methods: The B Method (TFM-B'10) June 7, 2010, Nantes, France
Pierre Castéran
http://www.labri.u-bordeaux.fr/perso/casteran/
Commandes latex pour B, Latex commands for B
- : \in
- /: \notin
- <: \subseteq
- /<:
- ><
- => \implies
- % \lambda
- ; \comp
- \/ \cup
- /\ \cap
- & \land
- or \lor
- ! \forall
- # \exists
- --> \fun
- +-> \pfun
- >--> \bij
- <--> \rel
- |-> \mapsto
- |> \rres
- <| \dres
- ||> \nrres
- <|| \ndrres
- >+-> \pbij
- +->> \psurj
- >+-> \pinj
- -->> \surj
- >--> \inj
- == \defs
- <-- \leftarrow
- || \parallel
- /= \neq
- <= \leq
- {} \emptyset
- * \times (produit cartésien, cartesian product)
Monday, March 1, 2010
B in Brazil
Sacomã station in Sao Paulo is now equipped with the COPPILOT System
Since January 10 2010, the new Sacomã station (Line 2 - green) in Brazil
is open to the public since its inauguration by Governor Jose Serra in Sao Paulo..
Since January 10 2010, the new Sacomã station (Line 2 - green) in Brazil
is open to the public since its inauguration by Governor Jose Serra in Sao Paulo..
Thursday, February 11, 2010
Monday, February 1, 2010
3rd International Conference From Research to Teaching Formal Methods: The B Method (TFM-B'10)
First Call for papers 3rd International Conference From Research to Teaching Formal Methods: The B Method (TFM-B'10) June 7, 2010, Nantes, France http://www.lina.univ-nantes.fr/apcb ------------------------------------------------ Invited Speaker: Pierre Castéran / On Coq and B /
LaBRI, U. Bordeaux ------------------------------------------------------
Overview: We anticipate a rich exchange of experiments
on research and teaching Formal Methods, in particular
the B method. We would like to cover various works going from
the elaboration of courses till the teaching materials
and the evaluation of students and teachers themselves. ------------------------------------------------------
TOPICS: The topics of interest for TFM-B'2010 include but
are not limited to: - Experiences with formal methods teaching using B - Teaching materials for the B method - Case studies and exercises featuring the B method - The B method in the software engineering curriculum - Use of the B method in disciplines other
than software engineering - New advances in the B method and their incorporation
into the teaching curriculum - Tool supports for software engineering with the B method - Teaching tool-equipped formal methods - Teaching environments for model-based formal methods - Combining the B method with other approaches - Comparative studies on teaching formal methods . . . ------------------------------------------------------------------------------------ Important Dates: Paper submission deadline March 13, 2010 Notification of acceptance/rejection April 16, 2010 Final version of accepted papers May 8, 2010 Workshop in Nantes, France June 7, 2010 Proceedings with ISBN ------------------------------------------------------------------------------------- Workshop Chairs: Christian ATTIOGBÉ,
Dominique MERY Local Organization: COLOSS Team www.lina.univ-nantes.fr LINA, UMR CNRS 6241, University of Nantes Contact: bdays)@(univ-nantes.fr http://www.lina.univ-nantes.fr/apcb
Wednesday, January 20, 2010
Investigation into the teaching of B worldwide
Investigation into the teaching of B worldwide
The Questionaire
Where is B taught ?
We would like to update the investigation carried out over a year ago by Marie Laure Potet.
Please fill in the following questionaire and return it to us.
University: B is taught in the following departments, on the following courses,
in the following years:
[So we can store as triples (Department, Course, year)]
Department: (E.g. Computer Science)
Course: (E.g. BSc Computer Science)
Year: (E.g. 1st, 2nd)
Duration of Course in lecture hours (e.g. 20 hours)
Do you use a tool? (If so which one?):
How long do the students spend using the tool in the lecturers presence?: (E.g. 20 hours)
Is B used in assignments (outside normal teaching hours)?:
What is the relation between the teaching of B and the teaching of mathematics and logic for IT:
Under which discipline is B taught (e.g. software engineering, programming etc.):
Name of course contact:
Email address:
Type of assessment (e.g. supervised project, group project, machine-based exam):
Have you written course notes?:
Would you be prepared to share them with colleagues?:
-------------------------
The responses to this questionaire have been provided by:
Surname:
First Name:
Postal Address:
E-mail Address:
They are correct as of the date:
--------------------------
Please circulate to other interested parties.
H. Habrias.
We will send an analysis of the results of the questionaire to everyone who has filled one in.
The information provided will be available from one or several web sites. If you do not want your information to be made publicly
available then please do not provide it.
We abide by the freedom of information act.
Completed questionaires (and any questions) should be addressed to:
Henri Habrias
henri dot habrias at univ-nantes dot fr
The answers (2002 !)
http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/coursb/RepEnqueteFin06.html
The Questionaire
Where is B taught ?
We would like to update the investigation carried out over a year ago by Marie Laure Potet.
Please fill in the following questionaire and return it to us.
University: B is taught in the following departments, on the following courses,
in the following years:
[So we can store as triples (Department, Course, year)]
Department: (E.g. Computer Science)
Course: (E.g. BSc Computer Science)
Year: (E.g. 1st, 2nd)
Duration of Course in lecture hours (e.g. 20 hours)
Do you use a tool? (If so which one?):
How long do the students spend using the tool in the lecturers presence?: (E.g. 20 hours)
Is B used in assignments (outside normal teaching hours)?:
What is the relation between the teaching of B and the teaching of mathematics and logic for IT:
Under which discipline is B taught (e.g. software engineering, programming etc.):
Name of course contact:
Email address:
Type of assessment (e.g. supervised project, group project, machine-based exam):
Have you written course notes?:
Would you be prepared to share them with colleagues?:
-------------------------
The responses to this questionaire have been provided by:
Surname:
First Name:
Postal Address:
E-mail Address:
They are correct as of the date:
--------------------------
Please circulate to other interested parties.
H. Habrias.
We will send an analysis of the results of the questionaire to everyone who has filled one in.
The information provided will be available from one or several web sites. If you do not want your information to be made publicly
available then please do not provide it.
We abide by the freedom of information act.
Completed questionaires (and any questions) should be addressed to:
Henri Habrias
henri dot habrias at univ-nantes dot fr
The answers (2002 !)
http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/coursb/RepEnqueteFin06.html
Tuesday, January 12, 2010
Monday, January 4, 2010
Modeling in Event-B
Modeling in Event-B
System and Software Design
Jean-Raymond Abrial
Swiss Federal University (ETH), Zürich
Hardback
Not yet published - available from June 2010
(Stock level updated: 12:41 GMT, 04 January 2010)
c. £60.00
http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569
http://www.event-b.org/abook.html
Subscribe to:
Posts (Atom)
