点击看大图基本信息
- 作者： [美]Jean-Raymond Abrial, J.-R. Abrial [作译者介绍]
- 译者： 裘宗燕
- 丛书名： 国外计算机科学教材系列
- 出版社：电子工业出版社
- ISBN：7505393391
- 上架时间：2004-7-1
- 出版日期：2004 年6月
- 开本：16开
- 页码：526
- 版次：1-1
Thursday, November 3, 2011
原书名： The B-Book:Assigning Programs to Meanings
Wednesday, November 2, 2011
Techniques industrielles de modélisation formelle pour le transport
Introduction - Jean-Louis BOULANGER
1. Une approche innovante et une aventure humaine au service
de la sécurité ferroviaire - Sylvain FIORONI
2. SAET-METEOR - Jean-Louis BOULANGER
3. Preuve de propriétés globales à l’aide de l’outil de preuve SIMULINK
DESIGN VERIFIER - Véronique DELEBARRE, Jean-Frédéric ETIENNE
4. Démonstration de la sécurité d’une application ferroviaire de signalisation
en mode nominal et en modes dégradés par la preuve formelle
Jean-Marc MOTA, Evguenia DMITRIEVA, Amel MAMMAR, Paul CASPI,
Salimeh BEHNIA, Nicolas BRETON, Pascal RAYMOND
5. Utilisation de la preuve formelle dans le CBTC (OCTYS)
Christophe TREMBLIN, Pierre LESOILLE, Omar REZZOUG
6. Validation d’automatismes ferroviaires de sécurité à base de réseaux
de Petri - Marc ANTONI
7. ERTMS Formal Specs : un langage dédié pour la formalisation
des spécifications pour le développement d’unité bord ERTMS
Laurent FERIER, Stanislas PINTE, Darius BLASBAND, Svitlana LUKICHEVA
8. Synthèse et conclusions - Jean-Louis BOULANGER
Glossaire
Bibliographies. Index
http://www.lavoisier.fr/livre/h3230.html
1. Une approche innovante et une aventure humaine au service
de la sécurité ferroviaire - Sylvain FIORONI
2. SAET-METEOR - Jean-Louis BOULANGER
3. Preuve de propriétés globales à l’aide de l’outil de preuve SIMULINK
DESIGN VERIFIER - Véronique DELEBARRE, Jean-Frédéric ETIENNE
4. Démonstration de la sécurité d’une application ferroviaire de signalisation
en mode nominal et en modes dégradés par la preuve formelle
Jean-Marc MOTA, Evguenia DMITRIEVA, Amel MAMMAR, Paul CASPI,
Salimeh BEHNIA, Nicolas BRETON, Pascal RAYMOND
5. Utilisation de la preuve formelle dans le CBTC (OCTYS)
Christophe TREMBLIN, Pierre LESOILLE, Omar REZZOUG
6. Validation d’automatismes ferroviaires de sécurité à base de réseaux
de Petri - Marc ANTONI
7. ERTMS Formal Specs : un langage dédié pour la formalisation
des spécifications pour le développement d’unité bord ERTMS
Laurent FERIER, Stanislas PINTE, Darius BLASBAND, Svitlana LUKICHEVA
8. Synthèse et conclusions - Jean-Louis BOULANGER
Glossaire
Bibliographies. Index
http://www.lavoisier.fr/livre/h3230.html
Fourth NASA Formal Methods Symposium
SECOND CALL FOR PAPERS NFM 2012 Fourth NASA Formal Methods Symposium Norfolk, Virginia, USA April 3 - 5, 2012 http://shemesh.larc.nasa.gov/nfm2012/ nasa-nfm2012@mail.nasa.gov |
Thursday, October 6, 2011
Tutorial on the Event-Based B Method
http://www.needocs.com/document/academique-cours-mathematiques-tutorial-on-the-event-based-b-method,9034
tutorial de Dominique Cansell, Dominique Méry
tutorial de Dominique Cansell, Dominique Méry
ABZ 2012
http://ifm-abz.isti.cnr.it/page22/abzindex.html
B Track Chair :
Michael Leuschel , University of Düsseldorf, Germany (leuschel@cs.uni-duesseldorf.de)
B Track Chair :
Michael Leuschel , University of Düsseldorf, Germany (leuschel@cs.uni-duesseldorf.de)
9th International Conference on Integrated Formal Methods (iFM 2012) in conjunction with ABZ 2012, in honor of Egon Boerger's 65th birthday for his contribution to state-based formal methods
PRELIMINARY
CALL FOR PAPERS
**********************************************************************
9th International Conference on Integrated Formal Methods (iFM 2012)
in conjunction with ABZ 2012, in honor of Egon Boerger's 65th birthday
for his contribution to state-based formal methods
June 18 - 22, 2012 - CNR - Pisa - ITALY http://ifm.isti.cnr.it
Consiglio Nazionale delle Ricerche
Istituto di Scienza e Tecnologie dell'Informazione ``A. Faedo''
Formal Methods && Tools Lab.
Via Moruzzi 1 - 56124 Pisa
**********************************************************************
OBJECTIVES AND SCOPE
Applying formal methods may involve the modeling of different aspects
of a system that are expressed through different paradigms.
Correspondingly, different analysis techniques will be used to examine
differently modeled system views, different kinds of properties, or
simply in order to cope with the sheer complexity of the system.
The iFM conference series seeks to further research into the
combination of (formal and semi-formal) methods for system development,
regarding modeling and analysis, and covering all aspects from language
design through verification and analysis techniques to tools and their
integration into software engineering practice Areas of interest
include but are not limited to:
- Case Studies;
- Experience reports;
- Formal and semiformal modelling notations;
- Integration of formal methods into software engineering practice;
- Logics;
- Model checking;
- Model transformations;
- Semantics;
- Static Analysis;
- Refinement;
- Theorem proving;
- Tools;
- Type Systems;
- Verification
SUBMISSION GUIDELINES
iFM 2012 solicits high quality papers reporting research results and/or
experience reports related to the overall theme of method integration.
The conference proceedings will be published by Springer Lecture Notes
in Computer Science series. All papers must be original, unpublished,
and not submitted for publication elsewhere. All submissions must be
in PDF format, using the Springer LNCS style files; we suggest to use
the LaTeX2e package (the llncs.cls class file, available in llncs2e.zip
and the typeinst.dem available in typeinst.zip as a template for your
contribution). Submissions should be made using the iFM 2012 Easychair
web site. Papers should not exceed 15 pages in length. Each paper will
undergo a thorough review process.
All accepted papers must be presented at the conference. Their
authors must be prepared to sign a copyright transfer statement.
At least one author of each accepted paper must register to the
conference by the early date indicated by the organizers, and
present the paper.
IMPORTANT DATES
Paper submission: January 14, 2012
Paper notification: March 1, 2012
Final version paper: March 20, 2012
INVITED SPEAKERS
Egon Boerger, University of Pisa, Italy
Muffy Calder, University of Glasgow, United Kingdom
Ian J. Hayes, University of Queensland, Australia
ABZ - iFM 2012 GENERAL CHAIRS
John Derrick, University of Sheffield, United Kingdom
Stefania Gnesi, CNR-ISTI, Italy
iFM PROGRAMME COMMITTEE CHAIRS:
Diego Latella, CNR-ISTI, Italy
Helen Treharne, University of Surrey, United Kingdom
FINANCE CHAIR
Alessandro Fantechi, Universita' di Firenze, Italy
ORGANIZING COMMITTEE CHAIR
Maurice ter Beek, CNR-ISTI, Italy
WORKSHOP CHAIRS
Maurice ter Beek, CNR-ISTI, Italy
Angelo Gargantini, Universita' di Bergamo, Italy
PROGRAM COMMITTEE
Marc Benveniste, STMicroelectronics Rousset, France
Eerke Boiten, University of Kent, UK
Jonathan Bowen, Museophile Limited, UK
Jim Davies, Oxford University, UK
John Derrick, University of Sheffield, UK
Jin Song Dong, National University of Singapore
Kerstin Eder, University of Bristol, UK
Alessandro Fantechi, Univ. Florence & CNR/ISTI, Italy
John Fitzgerald, University of Newcastle, UK
Andy Galloway, University of York, UK
Einar Broch Johnsen, University of Oslo, Norway
Rajeev Joshi, NASA Jet Propulsion Laboratory, USA
Diego Latella, CNR/ISTI, Italy
Michael Leuschel, University of Duesseldorf, Germany
Michele Loreti, University of Florence, Italy
Dominique Mery, Nancy University and LORIA, France
Stephan Merz, INRIA Nancy and LORIA, France
Alexandre Mota, CIn-UFPE, Brasil
Flemming Nielson, Technical University of Denmark
Luigia Petre, Abo Akademi University, Turku, Finland
David Pichardie, INRIA Rennes, France
Thomas Santen, Microsoft Research, Aachen, Germany
Steve Schneider, University of Surrey, UK
Kaisa Sere, Abo Akademi University, Turku, Finland
Graeme Smith, University of Queensland, Australia
Kenji Taguchi, AIST, Japan
Helen Treharne, University of Surrey, UK
Mirco Tribastone, LMU, Germany
Marina Walden, Abo Akademi Univ., Turku, Finland
Heike Wehrheim, University of Paderborn, Germany
Kirsten Winter, University of Queensland, Australia
**********************************************************************
This call for papers and additional information about the conference
can be found at http://ifm.isti.cnr.it
For information regarding the conference you can contact:
iFM2012@isti.cnr.it
Rodin User and Developer Workshop, 27-29 February 2012, Fontainebleau, France
Rodin User and Developer Workshop, 27-29 February 2012, Fontainebleau, France http://wiki.event-b.org/index.php/Rodin_Workshop_2012 Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A range of plug-ins have already been developed including ones that support animation, model checking and UML-B. The first Rodin User and Developer Workshop was held at the University of Southampton while the second took place at the University of Düsseldorf in 2010. The 2012 workshop will be part of the DEPLOY Federated Even hosted by the LACL laboratory at IUT Sénart-Fontainebleau. Fontainebleau is within easy reach of Paris: http://www.bmethod.com/php/federated-event-2012-en.php If you are interested in giving a presentation at the Rodin workshop, send a short abstract (1 or 2 pages PDF) to rodin@ecs.soton.ac.uk by 16 January 2012. Attendance at the DEPLOY Federated Event (including the Rodin Workshop) is open to all. Organisers Michael Butler, University of Southampton Stefan Hallerstede, University of Aarhus Thierry Lecomte, ClearSy Michael Leuschel, University of Düsseldorf Alexander Romanovsky, Newcastle University Laurent Voisin, Systerel |
Une Deuxième Révolution Galiléenne
Ca se passe le vendredi prochain 7 octobre à 15h30
en salle i001, département de mathématiques de l'Université d'Angers. Cela peut intéresser les chercheurs, mais aussi les enseignants ! Colin ===================================== Une Deuxième Révolution Galiléenne Gilles Dowek (INRIA) L'introduction d'un nouveau concept
scientifique permet souvent de donner de nouvelles réponses à des
questions anciennes qui n'avaient jusqu'alors reçu que des réponses
imparfaites. Par exemple, l'introduction des notions d'atome
et molécule a permis de donner de nouvelles réponses aux questions/
"qu'est-ce que l'oxygène ?","qu'est-ce que l'eau ?", "qu'est-ce qu'une
réaction chimique ?",/.... Cet exposé présentera quelques questions qui
ont trouvé de nouvelles réponses depuis que nous comprenons mieux
la notion d'algorithme : "/qu'est-ce qu'un aéroport ?", "qu'est-ce
qu'un nombre entier ?", "qu'est-ce qu'une démonstration mathématique ?",
"qu'est-ce qu'une théorie mathématique ?", "qu'est-ce qu'une loi physique ?",/
... La prise de conscience du caractère algorithmique de ces
objets scientifiques nous amène à considérer de nouveaux langages
pour les décrire. Cette révolution, dans le langage dans lequel la science
s'écrit, peut-être comparée à la révolution qui s'est produite,
au début du XVIIe siècle, quand le langage mathématique a commencé
à être utilisé pour décrire des phénomènes physiques.
Sunday, June 5, 2011
Les Journées Scientifiques 2011 de l'Université de Nantes
Ont lieu demain. La conférence The B Method : from Research to Teaching n'aura pas lieu cette année.
RDV aux conférences grand-public
10h30 - 18h00 : Nous vous invitons également à venir visiter les stands et expositions dans la grande halle de la Cité Nantes Events Center (laboratoires, expositions, vidéos, formations...).
RDV aux conférences grand-public
- 15h00-16h00 : Conférence « Greffer des organes d'animaux sur l'homme : rêve ou réalité ?" par Jean-Paul SOULILLOU, Professeur à l'Université de Nantes, Praticien Hospitalier au CHU de Nantes
- 16h15-17h00 : Conférence « Pourquoi une éthique du soin est-elle nécessaire aujourd'hui ?" par Fabienne BRUGÈRE, Philosophe, Professeur à l'Université Montaigne-Bordeaux III, Présidente du Conseil de développement durable de la Communauté Urbaine de Bordeaux
- 17h00-18h00 : Table ronde sur le thème des nouvelles technologies en santé. Échange avec le public en présence de :
- Jean-Paul SOULILLOU
- Fabienne BRUGÈRE
- Jean-Paul GALMICHE, Professeur à l'Université de Nantes, Praticien hospitalier au CHU de Nantes, spécialiste d'hépato-gastroentérologie.
10h30 - 18h00 : Nous vous invitons également à venir visiter les stands et expositions dans la grande halle de la Cité Nantes Events Center (laboratoires, expositions, vidéos, formations...).
Thursday, February 17, 2011
WWV 2011 Automated Specification and Verification of Web Systems
First Call for Papers WWV 2011 Automated Specification and Verification of Web Systems 7th International Workshop (as part of DisCoTec'11) http://rap.dsi.unifi.it/wwv2011/ June 9, 2011 - Reykjavik, Iceland ******************************************************** IMPORTANT DATES Abstract Submission March 28, 2011 Full Paper Submission April 4, 2011 Acceptance Notification May 3, 2011 Camera Ready (pre-proceedings) May 30, 2011 Workshop June 9, 2011 Camera Ready (post-proceedings) July 4, 2011
Workshop B 2011, colocated with FM 2011, Limerick, Ireland, june, 21, 2011
http://membres-liglab.imag.fr/idani/BWorkshop/index.html
IMPORTANT DATES Abstract submission March 3, 2011 Paper submission March 10, 2011 Acceptance notification April 12, 2011 Final version May 4, 2011 Workshop June 21, 2011
Sunday, February 13, 2011
the release of ProB for Rodin 2.1
We are happy to announce the release of
ProB for Rodin 2.1
Numerous improvements went into the latest release:
- constraint-based deadlock checker: finds counter-examplesto the deadlock freedom PO using constraint-solving - improved kernel with improved constraint solving (in particular improved boolean constraint solver) - ProB can now efficiently solve integer constraints using the finite domain solver CLP(FD) (you can turn this feature on in the Preferences Dialog) - improved LTL model checker with new counter-example display - new, improved version of BMotionStudio to generate graphical visualisations of your models - automatic record detection (when defining closed records using Records plug-in or manually using bijections on Cartesian products) - 64-bit version of ProB for Mac OS X (performance improvement; less hash collisions in model checking; larger range for the integer constraint solver; ...) - and many more. To install ProB, first download Rodin 2.1, choose Help -> Install New Software and simply choose the pre-configured ProB update site. More detailed installation instructions and a brief tutorial can be found here: http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Rodin_First_Step We have also released the new version 1.3.3 of ProB Classic, a version of ProB with a Tcl/Tk interface. It can be obtained at: http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download ProB Classic, is a stand-alone application but can be started automatically from within Rodin by setting the ProB Classic preference. ProB Classic provides some features which are not yet available in the ProB for Rodin version (graphical visualisation of the state space, debugging of axioms with unsat core computation, CSP support...). Kind regards, The ProB Team from Düsseldorf http://www.stups.uni-duesseldorf.de/ProB/ |
Have we learned from the Wasa disaster ? J.R. Abrial
http://videotorium.hu/en/recordings/details/1674,Have_we_learned_from_the_Wasa_disaster_
- Conference, 2006. September 19 - 20.
- http://www.jaist.ac.jp/~bjorner/ae-is-budapest/
Subscribe to:
Posts (Atom)
