Monday, January 8, 2018

Méthodes formelles et systèmes cyber-physiques – Séminaire à Shonan

China : Jean-Raymond Abrial : "international science and technology cooperation award"

Source: Xinhua/Shanghai Daily | January 10, 2017,
Presiding over the ceremony, Vice Premier Zhang Gaoli called on those involved in science and technology to follow the example set by the prize winners and contribute to the country’s drive to become a major power in the sector.
The ceremony, attended by around 3,300 representatives from the Communist Party of China, state and military organs and science and technology circles, honored 279 projects, seven scientists and one international organization with national prizes.
The international cooperation prizes were awarded to five scientists from the United States, Germany and France, and the Mexico-headquartered International Maize and Wheat Improvement Center.
Shanghai excelled at the ceremony with 52 projects and scientists honored.

French scientist Jean-Raymond Abrial, who has been working with local scientists on system and software engineering, won the international science and technology cooperation award.

Shanghai-based chip designer Spreadtrum won in the technology progress category for its contribution to the development of TD-LTE (time division-long term evolution), the China-developed 4G standard for phones.
Tongji University was Shanghai’s biggest success story with seven programs developed by its staff winning one first prize and six seconds.
A team led by Tong Xiaohua, a professor at its College of Surveying and Geo-Informatics, won first prize for an invention that improves the accuracy of information collected by remote sensors, thus providing important support for aerospace projects, such as improving imaging quality of Chinese laser sensors for finding safe landing sites
“When satellites and other aerospace facilities are flying high in the space, they may have jitter vibration and face other challenges that will disturb them from taking precise images and data,” Tong said. “Our technology by image analysis can detect and estimate the influence of the disturbances, and thus improve geo-positioning accuracy of high-resolution images together with ground geometric calibration.”
The achievement came after 10 years of cooperation with the Shanghai Institute of Technical Physics of the Chinese Academy of Sciences and the Development Research Center of the China Geological Survey.
Another team led by Zhu Hehua, a professor at Tongji’s College of Civil Engineering, won a second prize for developing a series of key technologies for underground construction in urban areas.
A major health award went to Dr Jing Zaiping of Changhai Hospital for his research into minimally invasive endovascular surgery. His work on aortic dissection and aneurysms made once fatal diseases treatable."

Le scientifique français M. Jean-Raymond Abrial s’est vu décerner le 2 janvier 2017 à Pékin le Prix Chinois de la Coopération Internationale en Science et Technologie, au cours d’une cérémonie récompensant des personnes ayant contribué au développement scientifique et technologique de la Chine. Cette cérémonie s’est tenue en la présence du président XI Jinping, du premier ministre LI Keqiang, et du vice premier ministre ZHANG Gaoli. Le Prix Chinois de la Coopération Internationale en Science et Technologie est un prix annuel de prestige créé en 1994 faisant partie des Prix Nationaux en Science et Technologie. Cette année il a été attribué à cinq scientifiques étrangers et à une ONG internationale.
Jean-Raymond Abrial est un informaticien français de renommée internationale. Anciennement chercheur à l’INRIA (Institut national de recherche en informatique et en automatique), il est membre de l’Académie Européenne des Sciences, et est connu dans le monde du développement logiciel comme le créateur de la notation formelle Z et par la suite de la méthode B. Il a d’ailleurs participé à l’implémentation de la suite d’outils utilisant cette méthode, qui a été utilisée pour des applications de systèmes de sécurité critiques à travers le monde. Il a également fait partie de l’équipe qui a conçu la première version du langage de programmation Ada.
Jean-Raymond Abrial a largement contribué à la recherche scientifique en Chine. En 2005 il a débuté une coopération avec le professeur HE Jifeng de l’Université Normale de la Chine de l’Est où il a dirigé des projets de recherche jusqu’à leur application industrielle. Il a ainsi introduit la méthode B en Chine et, grâce à lui, de nombreux systèmes basés sur des logiciels de sécurité critiques ont été conçus et développés avec succès dans le pays, et de nombreuses entreprises ont été capables de développer ce type de systèmes de manière indépendante. Il a également dirigé, en collaboration avec le professeur HE Jifeng, le développement d’un logiciel pour le métro automatique de Shanghai. Il est prévu que cette nouvelle technologie soit installée sur la Ligne 17 du métro, entre Hongqiao Railway Station et Oriental Land, et les essais devraient commencer à la fin de cette année.
Dernière modification : 12/01/201

Sunday, January 7, 2018

ICTAC2015 Conference - Keynote by Jean-Raymond Abrial

This is the Keynote titled "An Exercise in Mathematical Engineering: Stating and Proving Kuratowski Theorem" by Invited Speaker Jean-Raymond Abrial (Chair: Camilo Rueda)

Lectures of Jean-Raymond Abrial on B, Event-B, Rodin (vidéos)

Lecture 1

Lecture 2

Lecture 3 

Mini-course around Event-B and Rodin

Developping sequential programs

This lecture gives a status report of the hypervisor we are developing using Event-B.

Verification Corner, Modeling, refinement, and verification

In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool, which supports the Event-B formalism.

Monday, January 2, 2017

11th International Conference on Tests And Proofs TAP 2017

First Call for Papers

11th International Conference on Tests And Proofs
TAP 2017 Marburg (Germany), 19-20 July 2017

Part of STAF 2017

Important Dates

Abstract:             17 February 2017
Paper:                24 February 2017
Notification:          7 April 2017
Camera-Ready Version: 21 April 2017
Conference:           17-21 July 2017

Aim and Scope

The TAP conference promotes research in verification and formal
methods that targets the interplay of proofs and testing: the
advancement of techniques of each kind and their combination, with the
ultimate goal of improving software and system dependability.

Research in verification has recently seen a steady convergence of
heterogeneous techniques and a synergy between the traditionally
distinct areas of testing (and dynamic analysis) and of proving (and
static analysis). Formal techniques, such as model checking, that
produce counterexamples when verification fails are a clear example of
the duality of testing and proving. The combination of static
techniques such as satisfiability modulo theory and predicate
abstraction has provided means of proving correctness by complementing
exhaustive enumeration testing-like techniques. More practically,
testing supports the cost-effective debugging of complex models and
formal specifications, and is applicable in conditions that are beyond
the reach of formal techniques -- for example, components whose source
code is not accessible. Testing and proving are increasingly seen as
complementary rather than mutually exclusive techniques.

The TAP conference aims to promote research in the intersection of
testing and proving by bringing together researchers and practitioners
from both areas of verification.

Topics of Interest

TAP's scope encompasses many aspects of verification technology,
including foundational work, tool development, and empirical
research. Its topics of interest center around the connection between
proofs (and other static techniques) and testing (and other dynamic
techniques). Papers are solicited on, but not limited to, the
following topics:

- Verification and analysis techniques combining proofs and tests
- Program proving with the aid of testing techniques
- Deductive techniques (theorem proving, model checking, symbolic
execution, SMT solving, constraint logic programming, etc.) to
support testing: generating testing inputs and oracles, supporting
coverage criteria, and so on.
- Program analysis techniques combining static and dynamic analysis
- Specification inference by deductive and dynamic methods
- Testing and runtime analysis of formal specifications
- Model-based testing and verification
- Using model checking to generate test cases
- Testing of verification tools and environments
- Applications of testing and proving to new domains, such as
security, configuration management, and language-based techniques
- Bridging the gap between concrete and symbolic reasoning techniques
- Innovative approaches to verification such as crowdsourcing and
serious games
- Case studies, tool and framework descriptions, and experience
reports about combining tests and proofs

Highlight Topics

In addition to TAP’s general topics of interests, the 11th edition of
TAP will feature two highlight topics on techniques, tools, and
experience reports on

1. Testing and proving the correctness of security properties and
 implementations of cryptographic functions and protocols with a
 focus on the successful interplay of tests and proofs, and

2. Asserting the correct functioning and testing of verification
 tools, especially on theorem provers, that form the basis of many
 verification results for tools and applications our society
 increasingly depends on.

Submission Instructions

TAP 2017 accepts papers of three kinds:

- Regular research papers: full submissions describing original
research, of up to 16 pages (excluding references).

- Tool demonstration papers: submissions describing the design and
implementation of an analysis/verification tool or framework, of up
to 8 pages (excluding references). The tool/framework described in
a tool demonstration paper should be available for public use.

- Short papers: submissions describing preliminary findings, proofs
of concepts, and exploratory studies, of up to 6 pages (excluding


Program Chairs

- Einar Broch Johnsen
- Sebastian Gabmeyer

Program Committee

- Bernhard K. Aichernig
- Elvira Albert
- Bruno Blanchette
- Jasmin C. Blanchette
- Achim D. Brucker
- Catherine Dubois
- Gordon Fraser
- Carlo A. Furia
- Sebastian Gabmeyer (chair)
- Angelo Gargantini
- Alain Giorgetti
- Christoph Gladisch
- Martin Gogolla
- Arnaud Gotlieb
- Marieke Huisman
- Bart Jacobs
- Einar Broch Johnsen (chair)
- Nikolai Kosmatov
- Laura Kovacs
- Martin Leuker
- Panagiotis Manolios
- Karl Meinke
- Andreas Podelski
- Andrew J. Reynolds
- Martina Seidl
- Martin Steffen
- Martin Strecker
- T. H. Tse
- Luca Viganò
- Burkhart Wolff
- Stijn de Gouw

events mailing list

ABZ 2018

5-8 June 2018, Southampton, U.K.

Saturday, June 4, 2016

An Incremental B-Model for RBAC-Controlled Electronic Marking System

Nasser Al-hadhrami (Ministry of Education, Nizwa, Oman), Benjamin Aziz (School of Computing, University of Portsmouth, Portsmouth, UK) and Lotfi ben Othmane (Fraunhofer Institute for Secure Information Technology, Darmstadt, Germany)

Modelling and Refining Hybrid Systems in Event-B and Rodin