"Turing and Software Verification" (CLIFF B. JONES)

http://www.cs.ncl.ac.uk/research/pubs/trs/papers/1441.pdf

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)

http://www.igi-global.com/article/an-incremental-b-model-for-rbac-controlled-electronic-marking-system/152246

Modelling and Refining Hybrid Systems in Event-B and Rodin

• 
  
  
  
  Michael J. Butler, Jean-Raymond Abrial, Richard Banach:
  Modelling and Refining Hybrid Systems in Event-B and Rodin. From Action Systems to Distributed Systems 2016: 29-42

  • 
    
    
    
    
    
    
    

Formally Checking Large Data Sets in the Railways

http://arxiv.org/ftp/arxiv/papers/1210/1210.6815.pdf

This article presents industrial experience of validating large data sets against specification written using the B / Event-B mathematical language and the ProB model checker.

Comments:	In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012
Subjects:	Software Engineering (cs.SE)
Cite as:	arXiv:1210.6815 [cs.SE]
	(or arXiv:1210.6815v2 [cs.SE] for this version) See also :http://www.data-validation.fr/data-validation-in-the-railways/

Event-B patterns and their tool support

• Event-B patterns and their tool support
• Author / Creator:Hoang, Thai ; Fürst, Andreas ; Abrial, Jean-Raymond
• Summary:Event-B has given developers the opportunity to construct models of complex systems that are correct-by-construction. However, there is no systematic approach, especially in terms of reuse, which could help with the construction of these models. We introduce the notion of design patterns within the framework of Event-B to shorten this gap. Our approach preserves the correctness of the models, which is critical in formal methods and also reduces the proving effort. Within our approach, an Event-B design pattern is just another model devoted to the formalisation of a typical sub-problem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a larger model. We also present the interaction between developers and the tool support within the associated RODIN Platform of Event-B. The approach has been applied successfully to some medium-size industrial case studies.

Spécifier ou comment maîtriser l'abstrait

J.R. Abrial 
Spécifier ou comment maîtriser l'abstrait, 
TSI, Vol 3, N° 3, 
1984, 
pp. 201-219

Programming as a Mathematical Exercise

http://rsta.royalsocietypublishing.org/content/312/1522/447

Programming as a Mathematical Exercise [and Discussion]

J. R. Abrial, J. C. Shepherdson, J. S. Hillmore, R. L. Constable

Published 1 October 1984.DOI: 10.1098/rsta.1984.0070

Machines virtuelles pour le B événementiel

http://www.researchgate.net/publication/228364789_Machines_virtuelles_pour_le_B_vnementiel

Papers of the ABZ 2014 Conference

http://www.informatik.uni-trier.de/~ley/db/conf/asm/abz2014.html

Papers of J.R. Abrial

http://www.informatik.uni-trier.de/~ley/pers/hd/a/Abrial:Jean=Raymond

Formalizing Hybrid Systems with Event-B

Abstract State Machines, Alloy, B, VDM, and ZLecture Notes in Computer Science Volume 7316, 2012, pp 178-193Formalizing Hybrid Systems with Event-B

• Jean-Raymond Abrial, 
• Wen Su, 
• Huibiao Zhu

Abstract

• This paper contains the development of hybrid systems in Event-B and the Rodin Platform. It follows the seminal approach introduced at the turn of the century in Action Systems. Many examples illustrate our approach.
• http://link.springer.com/chapter/10.1007%2F978-3-642-30885-7_13

From Z to B and then Event-B: Assigning Proofs to Meaningful Programs

Integrated Formal MethodsLecture Notes in Computer Science Volume 7940, 2013, pp 1-15From Z to B and then Event-B: Assigning Proofs to Meaningful Programs

• Jean-Raymond Abrial

Abstract

• The very first paper on Z [1] was published in 1980 (at the time, the name Z was not “invented”), then the book on the B method [2] was published in 1996, and, finally, the book on Event-B [3] was published in 2010. So, 30 years separate Z from Event-B. It is thus clear that I spent a significant time of my scientific professional life working with the same kind of subject in mind, roughly speaking specification languages. I do not know whether this kind of addiction is good or bad, but what I know is that I enjoyed it a lot.
• http://link.springer.com/chapter/10.1007%2F978-3-642-38613-8_1

Set-Theoretic Models of Computations

Theories of Programming and Formal MethodsLecture Notes in Computer Science Volume 8051, 2013, pp 1-22Set-Theoretic Models of Computations

• Jean-Raymond Abrial

Abstract

• The purpose of this paper is to present some set-theoretic models of computation. This topic and its usefulness are clearly related to those presented in the book by Hoare and He: “Unifying Theories of Programming” [12]. However, we prefer to use here the term “computation” to that of “programming” as our purpose is not so much to unify various ways of programming (using different programming languages) but rather to see how various mechanical computation paradigms (be they sequential, distributed, parallel, and so on) can be given a unified mathematical theory. Our purpose is also to study how these computations can be specified and then developed by means of refinements and proofs.

Event-B patterns and their tool support

Software & Systems ModelingMay 2013, Volume 12, Issue 2, pp 229-244Event-B patterns and their tool support

• Thai Son Hoang, 
• Andreas Fürst, 
• Jean-Raymond Abrial
• Abstract
  

  Event-B has given developers the opportunity to construct models of complex systems that are correct-by-construction. However, there is no systematic approach, especially in terms of reuse, which could help with the construction of these models. We introduce the notion of design patternswithin the framework of Event-B to shorten this gap. Our approach preserves the correctness of the models, which is critical in formal methods and also reduces the proving effort. Within our approach, an Event-B design pattern is just another model devoted to the formalisation of a typical sub-problem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a larger model. We also present the interaction between developers and the tool support within the associated RODIN Platform of Event-B. The approach has been applied successfully to some medium-size industrial case studies.
• http://link.springer.com/article/10.1007%2Fs10270-010-0183-7

Formal Development of System of Systems

http://www.hindawi.com/isrn/software.engineering/2013/457837/

A rigorous reasoning about model transformations using the B method

http://hal.inria.fr/hal-00853720

Méthodes de spécification de systèmes temps réel en B

http://www.cert.fr/feria/svf/FAC/2004/Papiers/I2.pdf

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

Processus de validation basée sur la notion de propriété

http://www.rennes.supelec.fr/sic/REUNIONS/SdF/.../Gallardo.ppt

Vers une méthodologie de Validation et de Vérification multi-formelle des Interfaces Utilisateurs en milieu industriel

http://www.cert.fr/tis/theses/jthese_05/ressources/articles/cortier.pdf