% % Copyright (c) 1999-2008 Samuel Colin on behalf of the BRILLANT team, % identified as the developers of the BRILLANT project. % Permission is granted to copy, distribute and/or modify this document % under the terms of the GNU Free Documentation License, Version 1.2 % or any later version published by the Free Software Foundation; % with no Invariant Sections, no Front-Cover Texts, and no Back-Cover % Texts. A copy of the license is included in the section entitled "GNU % Free Documentation License". % % $Id: Bmethod.bib 982 2008-10-13 21:19:31Z scolin $ @String{FACIT = "Formal Approaches to Computing and Information Technology"} @String{LNCS = "Lecture Notes in Computer Science (Springer-Verlag)"} @String{TSI = "Technique et Science Informatique"} @String{ENTCS = "Electronic Notes in Theoretical Computer Science"} % B07-* keys == B 2007 / 2007 January / Besan{\c{c}}on % ZB05-* keys == ZB 2005 / 2005 April / Guildford % ZB03-* keys == ZB 2003 / 2003 June / Turku % ZB02-* keys == ZB 2002 / 2002 January / Grenoble % ZB00-* keys == ZB 2000 / 2000 August / Oxford % FM99-* keys == FM 99 / 1999 September / Toulouse % BUGM99-* keys == FM 99 User Group Meeting / 1999 September / Toulouse % B98-* keys == 2nd B Conference / 1998 Avpril / Montpellier % B96-* keys == 1st B Conference / 1996 November 24-26 / Nantes % AFM-* keys == Book Application of Formal Methods / 1995 % AFADL98-* keys == AFADL1998 / (LISI-ENSMA) 1998 / Poitiers % "SEE AFADL'2000 at http://www-lsr.imag.fr/afadl2000/Programme/ProgrammeAFADL2000.html" % Z2B-* keys == Z to B Conference / 1995 November / Nantes % "AFADL2001-* keys == AFADL2001 / (LORIA) 2001 / Nancy" % "AFADL2000-* keys == AFADL2000 / (LSR-IMAG) 2000 / Grenoble" % "AFADL03-* keys == AFADL2003 / (IRISA) 2003 / Rennes" % "AFADL04-* keys == AFADL04 / (IRISA) 2004 / Besan{\c{c}}on" % "AFADL06-* keys == AFADL06 / (CEDRIC-CNAM) 2006 / Paris" @InProceedings{AFADL04-Barradas, author = "Ru{\'\i}z Barradas, H{\'e}ctor and Bert, Didier", title = "Propri{\'e}t{\'e}s dynamiques avec hypoth{\`e}ses d'{\'e}quit{\'e} en {B} {\'e}v{\'e}nementiel", booktitle = "AFADL'2004", crossref = "AFADL2004", keywords = "event-B", pages = "299--316", year = "2004", } @InProceedings{AFADL04-Couchot, author = "Couchot, J.-F. and Giorgetti, A.", title = "Analyse d'atteignabilit{\'e} d{\'e}ductive", keywords = "B-Method, model-checking", booktitle = "AFADL'2004", crossref = "AFADL2004", pages = "131--148", year = "2004", } @InProceedings{AFADL04-Mammar, author = "Mammar, Amel and Laleau, R{\'e}gine", title = "{G}{\'e}n{\'e}ration de code ex{\'e}cutable {\`a} partir d'une sp{\'e}cification {B} : application aux bases de donn{\'e}es", booktitle = "AFADL'2004", crossref = "AFADL2004", keywords = "code generation", pages = "77--94", year = "2004", } @InProceedings{AFADL04-Okalas, author = "Okalas-Ossami, Dieu-Donn{\'e} and Souqui{\`e}res, Jeanine and Jacquot, Jean-Pierre", title = "Op{\'e}rations de construction de sp{\'e}cifications multi-vues {UML} en {B}", keywords = "UML, B2UML", booktitle = "AFADL'2004", crossref = "AFADL2004", pages = "115--130", year = "2004", } @InProceedings{AFADL04-Stouls, author = "Stouls, Nicolas and Potet, Marie-Laure", title = "Explicitation du contr{\^o}le de d{\'e}veloppements {B} {\'e}v{\`e}nementiels", booktitle = "AFADL'2004", crossref = "AFADL2004", pages = "13--28", year = "2004", } @InProceedings{AFADL04-Truong, author = "Truong, Ninh Thuan and Souqui{\`e}res, Jeanine", title = "Validation des propri{\'e}t{\'e}s de construction d'un sc{\'e}nario {UML/OCL} {\`a} partir de sa d{\'e}rivation {B}", booktitle = "AFADL'2004", crossref = "AFADL2004", keywords = "UML, UML2B", pages = "99--114", year = "2004", } @InProceedings{AFADL2000-Bodeveix, author = "Bodeveix, J.-P. and Filali, Mamoun and Mun{\~o}z, C. A.", title = "Formalisation de la m{\'e}thode {B} en {COQ} et {PVS}", booktitle = "AFADL'2000", crossref = "AFADL2000", pages = "96--110", year = "2000", } @InProceedings{AFADL2000-Bon, author = "Bon, Philippe and El Koursi, El Miloudi and Yim, Pascal", title = "Du cahier des charges aux sp{\'e}cifications formelles - Une m{\'e}thode bas{\'e}e sur la mod{\'e}lisation par les r{\'e}seaux de {P}etri de haut niveau", booktitle = "AFADL'2000", crossref = "AFADL2000", pages = "158--172", year = "2000", keywords = "Petri nets", } @InProceedings{AFADL2000-Cave, author = "Cave, Francis and Bert, Dider", title = "It{\'e}rateurs pour le langage {B}", booktitle = "AFADL'2000", crossref = "AFADL2000", pages = "96--110", year = "2000", } @InProceedings{AFADL2000-Marcano, author = "Marcano-Kamenoff, Rafael and Meyer, Eric and L{\'e}vy, Nicole and Souqui{\`e}res, Jeanine", title = "Utilisation de patterns dans la construction de sp{\'e}cifications {UML} et {B}", booktitle = "AFADL'2000", crossref = "AFADL2000", pages = "66--80", keywords = "B-Method, UML", year = "2000", } @InProceedings{AFADL2000-Motre, author = "Motr{\'e}, St{\'e}phanie", title = "Mod{\'e}lisation et impl{\'e}mentation formelle de la politique de s{\'e}curit{\'e} dynamique de la {JavaCard}", booktitle = "AFADL'2000", crossref = "AFADL2000", pages = "158--172", keywords = "JavaCard, smartcards", year = "2000", } @InProceedings{AFADL2000-Mountassir, author = "Mountassir, H. and Bellegarde, Fran{\c{c}}oise and Julliand, Jacques and Masson, P.-A.", title = "Coop{\'e}ration entre preuve et model-checking pour v{\'e}rifier modulairement des propri{\'e}t{\'e}s {LTL}", booktitle = "AFADL'2000", crossref = "AFADL2000", pages = "127--141", year = "2000", } @InProceedings{AFADL2000-Py, author = "Py, Laurent and Legeard, Bruno and Tatibou{\"e}t, Bruno", title = "{\'e}valuation de sp{\'e}cifications formelles en programmation logique avec contraintes ensemblistes -- application {\`a} l'animation de sp{\'e}cifications formelles {B}", booktitle = "AFADL'2000", crossref = "AFADL2000", pages = "21--35", year = "2000", } @Proceedings{AFADL2000, title = "Approches Formelles dans l'Assistance au {D}{\'e}veloppement de Logiciels", year = "2000", address = "LSR/IMAG -- BP 72 38402 Saint-Martin d'Heres Cedex -- Grenoble -- France", month = jan, organization = "AFADL2000, LSR/IMAG", URL = "http://www-lsr.imag.fr/afadl2000/Programme/ProgrammeAFADL2000.html", publisher = "LSR/IMAG", } @InProceedings{AFADL2001-Bert, author = "Bert, Didier", title = "Preuve de propri{\'e}t{\'e}s d'{\'e}quit{\'e} en {B} : Preuve de l'algorithme d'arbitrage du bus {SCSI}-3", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "221--241", URL = "http://www.loria.fr/conferences/afadl/Papiers/bert.ps", year = "2001", month = jun, } @InProceedings{AFADL2001-Boite, author = "Boite, Olivier", title = "Prouveur sp{\'e}cialis{\'e} pour le langage d'ensemble d'entiers et de bool{\'e}ens {LEEB}", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "157--171", URL = "http://www.loria.fr/conferences/afadl/Papiers/boite.ps", year = "2001", month = jun, } @InProceedings{AFADL2001-Cansell, author = "Cansell, Dominique and Jaray, Jacques", title = "Utilisation de {B} pour l'aide {\`a} la sp{\'e}cification d'un syst{\`e}me de diagnostic", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "67--81", year = "2001", month = jun, } @InProceedings{AFADL2001-Casset, author = "Casset, Ludovic", title = "Formal Implementation of a verification algorithm using the {B} method", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "51--65", year = "2001", month = jun, abstract = "The Java language is advertised as a secure language. Several components enforce the Java security, as the Java Virtual Machine (JVM) and the API. As a part of the JVM, the Java byte code verifier plays an important role in the security of the system. Therefore, its implementation has to be correct. To ensure this correctness, formal methods are used as a means of proving that the implementation of the verifier corresponds to its specification. On a subset of the Java language, we provide the formal implementation of a verification algorithm taking into account control flow and object initialization. The works focuses on the design and the proof of the type inference algorithm. The proof of the algorithm termination is performed using the B method and its implementation is proposed in B0.", URL = "http://citeseer.ist.psu.edu/554285.html", keywords = "B-Method, byte code verifier, JVM, Java, B0", } @InProceedings{AFADL2001-Charlet, author = "Bellegarde, Fran{\c{c}}oise and Charlet, C. and Kouchnarenko, O.", title = "Raffiner pour v{\'e}rifier une classe de syst{\`e}mes param{\'e}tr{\'e}s", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "189--204", URL = "http://www.loria.fr/conferences/afadl/Papiers/charlet.ps", keywords = "model-checking, refinement", year = "2001", month = jun, } @InProceedings{AFADL2001-Chouali, author = "Bellegarde, Fran{\c{c}}oise and Chouali, S. and Julliand, Jacques and Kouchnarenko, O.", title = "Comment limiter la sp{\'e}cification de l'{\'e}quit{\'e} dans les syst{\`e}mes d'{\'e}v{\'e}nements {B}", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "205--219", URL = "http://www.loria.fr/conferences/afadl/Papiers/chouali.ps", year = "2001", month = jun, } @InProceedings{AFADL2001-Ledang, author = "Ledang, Hung", title = "Des cas d'utilisation {\`a} une sp{\'e}cification {B}", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "131--140", keywords = "UML, UML2B, use case", year = "2001", month = jun, } @InProceedings{AFADL2001-Ledoux, author = "Ledoux, Franc and Mota, Jean-Marc and Arnould, Agn{\`e}s and Dubois, Catherine and Le Gall, Pascale and Bertrand, Yves", title = "Sp{\'e}cification formelle du chanfreinage", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "157--171", keywords = "CASL, algebraic specifications, geometric modelling", URL = "http://www.loria.fr/conferences/afadl/Papiers/ledoux.ps", year = "2001", month = jun, } @InProceedings{AFADL2001-Legeard, author = "Legeard, Bruno and Perreux, Fabien", title = "{G}{\'e}n{\'e}ration de s{\'e}quences de test {\`a} partir d'une sp{\'e}cification {B} en {PLC} ensembliste", booktitle = "AFADL'2001", crossref = "AFADL2001", keywords = "test generation, constraint logic programming, constraint programming", pages = "113--130", year = "2001", month = jun, } @InProceedings{AFADL2001-Marcano, author = "Marcano-Kamenoff, Rafael and L{\'e}vy, Nicole", title = "Transformation d'annotations {OCL} en expressions {B}", booktitle = "AFADL'2001", crossref = "AFADL2001", pages = "39--49", year = "2001", month = jun, URL = "http://www.loria.fr/conferences/afadl/Papiers/marcano.ps", keywords = "OCL, UML, B-Method, UML2B", } @Proceedings{AFADL2001, title = "Approches Formelles dans l'Assistance au {D}{\'e}veloppement de Logiciels", year = "2001", address = "ADER/LORIA Nancy -- France", month = jun, organization = "AFADL2001, ADER/LORIA", URL = "http://www.loria.fr/conferences/afadl/", publisher = "ADER/LORIA", } @InProceedings{AFADL2003-Badeau, author = "Badeau, Fr{\'e}d{\'e}ric and Bert, Didier and Boulm{\'e}, Sylvain and Potet, Marie-Laure and Stouls, Nicolas and Voisin, Laurent", title = "Traduction de {B} vers des langages de programmation: points de vue du projet {BOM}", keywords = "code generation", crossref = "AFADL2003", booktitle = "AFADL'2003", pages = "87--102", year = "2003", month = jan, } @InProceedings{AFADL2003-Berkani, author = "Berkani, Karim and Dubois, Catherine and Faivre, Alain and Falampin, J{\'e}r{\^o}me", title = "Validation des r{\`e}gles de base de l'{Atelier B}", keywords = "validation", crossref = "AFADL2003", booktitle = "AFADL'2003", pages = "121--136", year = "2003", } @InProceedings{AFADL2003-Bodeveix, author = "Bodeveix, Jean-Paul and Filali, Mamoun", title = "Machines virtuelles pour le {B} {\'e}v{\'e}nementiel", keywords = "event-B", crossref = "AFADL2003", booktitle = "AFADL'2003", pages = "227--242", year = "2003", } @InProceedings{AFADL2003-Bouquet, author = "Bouquet, Fabrice and Legeard, Bruno", title = "{R}{\'e}ification de scripts ex{\'e}cutables en g{\'e}n{\'e}ration de tests {\`a} partir de sp{\'e}cifications formelles: application aux m{\'e}canismes de transaction de la {JavaCard}", keywords = "JavaCard, smartcards", crossref = "AFADL2003", booktitle = "AFADL'2003", pages = "141--156", year = "2003", } @InProceedings{AFADL2003-Hammad, author = "Hammad, Ahmed and Julliand, Jacques and Mountassir, Hassan and Okalas-Ossami, Dieudonn{\'e}", title = "Expression en {B} et raffinement des syt{\`e}mes r{\'e}actifs temps r{\'e}el", keywords = "realtime, reactive systems", crossref = "AFADL2003", booktitle = "AFADL'2003", pages = "211--226", year = "2003", } @InProceedings{AFADL2003-Ledang, author = "Ledang, Hung and Souqui{\`e}res, Jeanine and Charles, S{\'e}bastien", title = "Argo/{UML} {B}: un outil de transformation syst{\'e}matique de sp{\'e}cification {UML} en {B}", keywords = "UML, UML2B, tool", crossref = "AFADL2003", booktitle = "AFADL'2003", pages = "3--18", year = "2003", month = jan, } @InProceedings{AFADL2003-Petit, author = "Petit, Dorian and Mariano, Georges and Poirriez, Vincent", title = "{G}{\'e}n{\'e}ration de composants {\`a} partir de sp{\'e}cifications {B}", keywords = "automatic code generation, tool, components, BRILLANT", crossref = "AFADL2003", booktitle = "AFADL'2003", pages = "103--120", year = "2003", } @Proceedings{AFADL2003, title = "Approches Formelles dans l'Assistance au {D}{\'e}veloppement de Logiciels", year = "2003", address = "IRISA Rennes -- France", month = jan, organization = "AFADL2003, IRISA", publisher = "IRISA", } @Proceedings{AFADL2004, title = "Approches Formelles dans l'Assistance au {D}{\'e}veloppement de Logiciels", year = "2004", address = "LIFC, 16, route de Gray, F-25030 Besan{\c{c}}on -- France", month = JUN, organization = "AFADL2004, Laboratoire d'Informatique de Franche-Comt{\'e}", URL = "http://lifc.univ-fcomte.fr/afadl2004/", publisher = "Jacques Julliand -- LIFC", } @InProceedings{AFADL98-Julliand, author = "Julliand, Jacques and Bellegarde, Fran{\c{c}}oise", title = "Extension de sp{\'e}cifications {B} par de la logique temporelle lin{\'e}aire pour d{\'e}crire des propri{\'e}t{\'e}s dynamiques de syst{\`e}mes r{\'e}actifs", booktitle = "AFADL'98", pages = "125--136", crossref = "AFADL98", } @InProceedings{AFADL98-Lanet, author = "Lanet, Jean-Louis", title = "Using the {B} Method to model protocols", booktitle = "AFADL'98", source = "GEMPLUS", abstract = "In this paper we suggest to use the {B} formal method to model a protocol dedicated to smart cards. We use a pragmatic approach to prove the dynamic properties of the protocol by using historical variables to express the past. We check manually that those variables have been correctly updated in the different operations. With this approach we can avoid the use of a model checker to verify the dynamic properties. We show the advantages of this method to express general properties and service properties. We focused on the formalisation of the rules given in the standard and on the refinement process. We introduce new events and invariants at each level. Using this method enabled us to bring to the fore some ambiguities and errors of the protocol.", URL = "http://www.gemplus.fr/smart/rd/publications/", keywords = "formal method, protocol, event based model, smartcards, JavaCard", crossref = "AFADL98", pages = "79--90", } @InProceedings{AFADL98-Ledru, author = "Ledru, Yves and Salanville, R{\'e}my", title = "Description d'architecture logicielle par connexion de machines abstraites", booktitle = "AFADL'98", pages = "37--48", crossref = "AFADL98", } @InProceedings{AFADL98-Ledru2, author = "Ledru, Yves and Oriat, Catherine and Potet, Marie-Laure", title = "Le raffinement vu comme primitive de sp{\'e}cification - une comparaison de {VDM}, {B}, {Specware}", booktitle = "AFADL'98", pages = "63--76", crossref = "AFADL98", } @Proceedings{AFADL98, title = "Approches Formelles dans l'Assistance au {D}{\'e}veloppement de Logiciels", year = "1998", address = "T{\'e}l{\'e}port2 - Avenue 1 - BP109 - 86960 FUTUROSCOPE Cedex", month = oct, organization = "AFADL1998, LISI/ENSMA", publisher = "LISI/ENSMA", } @InCollection{AFM-DeMe, author = "Dehbonei, Babak and Mejia, Fernando", title = "Formal Development of Safety-Critical Software Systems in Railway Signalling", crossref = "AFM95", booktitle = "Applications of Formal Methods", keywords = "railway signalling", pages = "227--252", year = "1995", } @InCollection{AFM-JHoare, author = "Hoare, Jonathan P.", title = "Application of the {B}-Method to {CICS}", crossref = "AFM95", pages = "97--124", year = "1995", } @Book{AFM95, title = "Applications of Formal Methods", publisher = "Prentice Hall International", year = "1995", editor = "Hinchey, M. G. and Bowen, J. P.", series = "Series in Computer Science", } @InProceedings{ALNS91, title = "The {B}-method (software development)", author = "Abrial, Jean-Raymond and Lee, M. K. O. and Neilson, D. S. and Scharbach, P. N. and Sorensen, I. H.", organization = "BP Res., Sunbury Res. Centre, Sunbury-on-Thames, UK", booktitle = "{VDM} 91. Formal Software Development Methods. 4th International Symposium of {VDM} Europe Proceedings.", volume = "2", pages = "398--405", editor = "Prehn, S. and Toetenel, J. W.", publisher = "Springer-Verlag, Berlin, Germany", year = "1991", month = oct, abstract = "The {B}-method is a formal software development process for the production of highly reliable, portable and maintainable software which is verifiably correct with respect to its functional specification. The method uses the abstract machine notation (AMN) as the language for specification, design and implementation within the process. {AMN} is a sugared and extended version of E.W. Dijkstra's (1976), guarded command notation with built-in structuring mechanisms for the construction of large systems. The method is supported over the entire spectrum of activities from specification to implementation by a set of computer-aided tools. (3 Refs)", keywords = "formal specification, program verification, software maintenance, B-Method, formal software development process, maintainable software, verifiably correct, functional specification, AMN, guarded command notation, built-in structuring mechanisms, computer-aided tool", } @InProceedings{AVIS2001-Bellegarde, author = "Bellegarde, Fran{\c{c}}oise and Darlot, C. and Julliand, Jacques and Kouchnarenko, O.", title = "How to Verify {LTL} perperties of Infinite Refined Systems by Proof and Model-Checking Cooperation", booktitle = "Proc. Int. Ws. on Automated Verification of Infinite-State Systems (AVIS'2001), joint to FME'01", year = "2001", address = "Berlin, Allemagne", month = mar, keywords = "model-checking, refinement, LTL logic", } @Article{Abri84a, title = "Specification or how to give reality to abstraction", author = "Abrial, Jean-Raymond", journal = "Technique et Science Informatiques", year = "1984", abstract = "The specification and construction of an algorithm for managing secondary memory space are described. This algorithm contains mechanisms for commitment and for recovery in the event of a breakdown. (3 Refs)", keywords = "program specification, algorithm construction, programming, programming theory, memory management, fault-tolerant computing, abstraction, secondary memory space, commitment, system recovery, breakdown", } @Article{Abri84b, title = "The mathematical construction of a program", author = "Abrial, Jean-Raymond", journal = "Science of Computer Programming", volume = "4", number = "1", pages = "45--86", month = apr, year = "1984", abstract = "This paper is an exercise in program construction using mathematics as a tool. The program which the author undertook the construction of is a general purpose proof checker. It is 'general purpose' in that it may take as input the axiomatization of a formal theory together with a proof written within this theory. As output it delivers a result which tells us whether the proof is correct or not. In order to test the generality of the proposed approach, the author uses the proof checker to check proofs written within theories such as propositional calculus and predicate calculus and set theory. (7Refs", keywords = "programming theory, mathematical construction, program construction, propositional calculus, predicate calculus, set theory", } % Additional information: 11-16 september @InProceedings{Abri88a, title = "The {B} tool (proof proving tool)", author = "Abrial, Jean-Raymond", booktitle = "{VDM} 88. {VDM} - The Way Ahead. 2nd {VDM}-Europe Symposium. Proceedings", pages = "86--7", editor = "Bloomfield, R. and Marshall, L. and Jones, R.", publisher = "Springer-Verlag, Berlin, West Germany", year = "1988", month = sep, abstract = "Summary form only given. {B} is an interactive program whose function is to assist people in doing formal proofs. The basic features of {B} are outlined. Built on these elementary features, {B} also contains a simplistic inference engine allowing simple goal-oriented proofs to be conducted in an interactive mode. The tool has a few built-in rules corresponding to a very limited knowledge of first-order predicate logic.", keywords = "formal logic, formal specification, inference mechanisms, program verification, software tools, formal specification, software tools, B tool, proof proving tool, B-Method, interactive program, formal proofs, inference engine, goal-oriented proofs, built-in rules, first-order predicate logic", } @Article{Abri88b, title = "A formal approach to software system development", author = "Abrial, Jean-Raymond", journal = "G{\'e}nie Logiciel et Syst{\`e}mes Experts", volume = "1", number = "11", pages = "22--8", month = mar, year = "1988", abstract = "Attention is directed to aspects of software specification such as mathematical models of the data, animation of the models and coherence of such data models. Considerations in software programming and unification of the two concepts are also covered.(22 Refs)", keywords = "programming, software engineering, specification languages, systems analysis, software specification, formal approach, software system development, mathematical models, animation, consistency, data models, software programming", } % Additional information: 26-30 June @InProceedings{Abri89, title = "A formal approach to large software construction", author = "Abrial, Jean-Raymond", booktitle = "Mathematics of Program Construction. 375th Anniversary of the Groningen University International Conference. Proceedings", pages = "1--20", editor = "Van de Snepscheut, J. L. A.", publisher = "Springer-Verlag, Berlin, West Germany", year = "1989", month = jun, abstract = "Is the rationalisation of software construction the main preoccupation of computer scientists today? The author presents, briefly and informally, a number of results concerning the so called axiomatic answer to this question. One of the recent trends of the discipline is to reduce the traditional distinction of the two main activities of software construction, namely specification and programming. This trend sometimes takes the form of 'executable specifications'; the author adopts a somewhat different approach, that of 'non necessarily executable programs'. The author shows that the main concepts of specification and those of programming can be unified. From this unification, a new activity, called design, will emerge; design is situated between specification and programming and its role is to ensure the systematic passage from one to the other. (20 Refs)", keywords = "formal specification, programming theory, formal approach, software construction, specification, programming", } @InProceedings{Abri91, title = "A refinement case study (using the {A}bstract {M}achine {N}otation)", author = "Abrial, Jean-Raymond", booktitle = "4th Refinement Workshop. Proceedings of the 4th Refinement Workshop", pages = "51--96", editor = "Morris, J. M. and Shaw, R. C.", publisher = "Springer-Verlag, Berlin, Germany", year = "1991", month = jan, abstract = "The author develops in detail a classical little example of refinement from initial specification down to final code. He insists on a few methodological points among which are the following: the importance of a sound mathematical preamble; the systematic usage of data refinement steps based on clear and intuitive technical decisions; and the reusability of already specified and refined pieces of code. The exercise is conducted using an homogeneous notational style based on abstract machines and generalized substitutions. (8 Refs)", keywords = "formal specification, software engineering, refinement, AMN, initial specification, data refinement steps, reusability, generalised substitutions", } @InProceedings{Abri92, title = "On constructing large software systems", author = "Abrial, Jean-Raymond", journal = "IFIP Transactions A (Computer Science and Technology)", volume = "A-12", pages = "103--12", year = "1992", booktitle = "Algorithms, Software, Architecture. Information Processing 92. IFIP 12th World Computer Congress", month = sep, abstract = "Some general principles are presented that one could follow in order to build large software systems with reduced probability of failure. The following topics are discussed: people, framing, set theory, programming languages, proof and tools. (0 Refs)", keywords = "human factors, software engineering, general principles, large software systems, people, framing, set theory, programming languages, proof, tools", } @InProceedings{Abrial88, author = "Abrial, J.-R.", title = "The {B} Tool", pages = "86--87", ISBN = "3-540-50214-9", editor = "Bloomfield, R. and Marshall, L. and Jones, R.", booktitle = "Proceedings of the 2nd {VDM}-Europe Symposium", month = sep, series = LNCS, volume = "328", publisher = "Springer", address = "Berlin", year = "1988", } @InProceedings{Abrial98, author = "Abrial, Jean-Raymond and Mussat, Louis", title = "Specification and Design of a Transmission Protocol by Successive Refinements Using {B}", booktitle = "Mathematical Methods in Program Development", editor = "Broy, Manfred and Schieder, Birgit", publisher = "Springer", series = "NATO ASI Series F: Computer ans Systems Sciences", volume = "158", year = "1997", pages = "129--200", } % Additional information: Sat Oct 10 14:40:24 MDT 1998 @Article{Abrial:1998:B, author = "Abrial, J.-R", title = "On {B}", journal = LNCS, volume = "1393", pages = "1--8", year = "1998", CODEN = "LNCSD9", ISSN = "0302-9743", } @InProceedings{Aertryck97a, author = "Van Aertryck, Lionel and Benveniste, Marc and Le Metayer, Daniel", title = "{CASTING} : une m'ethode formelle de g{\'e}n{\'e}ration de cas de tests", pages = "99--112", booktitle = "AFADL : Approches formelles dans l'assistance au d{\'e}veloppement de logiciel", year = "1997", keywords = "testing, tool", address = "Toulouse, France", month = may, } @InProceedings{Aertryck97b, author = "Van Aertryck, Lionel and Benveniste, Marc and Le Metayer, Daniel", title = "{CASTING} : {A} Formally Based Software Test Generation Method", pages = "101--111", booktitle = "ICFEM'97, First IEEE International Conference on Formal Engineering Methods", year = "1997", address = "Hiroshima, Japon", month = nov, } @PhdThesis{Aertryck98-PhD, author = "Van Aertryck, Lionel", title = "Une m{\'e}thode et un outil pour l'aide {\`a} la g{\'e}n{\'e}ration de jeux de tests de logiciels.", school = "Universit{\'e} de Rennes I", year = "1998", key = "Aertryck98", month = jan, abstract = "Pour obtenir un exemplaire \texttt{lionel.van-aertryck@irisa.fr}", } % Additional information: 5-6-7 Mai @InProceedings{Ait-Ameur-ISPS03, author = "A{\"\i}t-Ameur, Y. and Baron, M. and Kamel, N.", title = "Utilisation de techniques formelles dans la mod{\'e}lisation d'Interfaces Homme-Machine. Une exp{\'e}rience comparative entre {B} et Promela/{SPIN}.", booktitle = "In Proceedings of 6th International Symposium on Programming and Systems, Alg{\'e}rie", pages = "57--66", year = "2003", month = may, organization = "ISPS 2003", abstract = "Cet article pr{\'e}sente une exp{\'e}rience dans l'utilisation des techniques formelles pour la conception, la v{\'e}rification et la validation d'IHM au travers de l'utilisation de deux techniques dans un d{\'e}veloppement incr{\'e}mental. La premi{\`e}re technique est fond{\'e}e sur le raffinement et la preuve avec {B} et la seconde est fond{\'e}e sur la v{\'e}rification sur mod{\`e}le avec Promela/SPIN. Diff{\'e}rentes propri{\'e}t{\'e}s telles que la robustesse, l'atteignabilit{\'e}, l'insistance sont v{\'e}rifi{\'e}es gr{\^a}ce {\`a} l'utilisation de ces techniques. Nous discutons {\'e}galement les avantages et inconv{\'e}nients de ces deux techniques.", keywords = "HCI, B-Method, robustness, reachability, verification", } % Additional information: June 23 - 26 @InProceedings{Ait-Ameur-SERP03, author = "A{\"\i}t-Ameur, Y. and Baron, M. and Girard, P.", title = "Formal validation of {HCI} user tasks.", booktitle = "In Proceedings of The 2003 International Conference on Software Engineering Research and Practice, Las Vegas, Nevada USA", pages = "732--738", year = "2003", month = jun, organization = "SERP 2003", publisher = "CSREA Press, 2003", keywords = "HCI, B-Method, design, verification, validation", abstract = "Our work focuses on the use of formal techniques in order to increase the quality of HCI software and of all the processes resulting from the development, verification, design and validation activities. This paper shows how the {B} formal technique can be used for user tasks modelling and validation. A trace based semantics is used to describe either the HCI or the user tasks. Each task is modelled by a sequence of fired events. Each event is defined in the abstract specification and design of the HCI system.", } @Misc{Alnet96, key = "Alnet96", author = "Alnet, St{\'e}phane", title = "Test de programme {\`a} partir de sp{\'e}cifications {B}", howpublished = "Rapport de DEA", year = "1996", month = sep, abstract = "Nous {\'e}tudions le test {<<}bo{\^\i}te-noire{>>} de programme {\'e}crits {\`a} partir de la m{\'e}thode {B}. Nous proposons de plus une s{\'e}mantique pour de tels programmes, s{\'e}mantique observationnelle bas{\'e}e sur des traces.", keywords = "testing, B-Method", } @InProceedings{Ameur98a, author = "A{\"\i}t-Ameur, Y. and Girard, P. and Jambon, F.", title = "Using the {B} formal approach for incremental specification design of interactive systems", booktitle = "IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98)", year = "1998", address = "Heraklion (Crete), Greece", month = sep, keywords = "HCI", } @InProceedings{Ameur98b, author = "A{\"\i}t-Ameur, Y. and Girard, P. and Jambon, F.", title = "A Uniform approach for the Specification and Design of Interactive Systems: the {B} method", booktitle = "5th International Eurographics Workshop on Design, Specification", pages = "333--352", year = "1998", address = "Cosener's House, Abingdon, UK", month = jun, keywords = "HCI", } @InProceedings{Attiogbe97, author = "Attiogb{\'e}, Christian", title = "{R}{\'e}utilisation de composantes formelles par filtrage s{\'e}mantique: Cas des machines abstraites de {B}", number = "46", series = "G{\'e}nie Logiciel", pages = "95--99", booktitle = "Le G{\'e}nie Logiciel est ses Applications -- 1o eme Journ{\'e}es Internatinales - ACTES", year = "1997", month = dec, } @InProceedings{B-DC, author = "Colin, Samuel and Mariano, Georges and Poirriez, Vincent", title = "{D}uration calculus: a real-time semantic for {B}", booktitle = "First International Colloquium on Theoretical Aspects of Computing", year = "2004", month = sep, organization = "{UNU}-{IIST}", note = "Guiyang, China", } @InProceedings{B96-Abrial, author = "Abrial, Jean-Raymond", title = "Extending {B} without changing it (for Developing Distributed Systems)", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "Consultant ind{\'e}pendant, Paris, F", pages = "169--191", } @InProceedings{B96-Behm, author = "Behm, Patrick", title = "{D}{\'e}veloppement formel des logiciels s{\'e}curitaires de {METEOR}", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", keywords = "railway", institution = "MATRA Transport International, Montrouge, France", pages = "3--10", } @InProceedings{B96-Bert, author = "Bert, Didier and Potet, Marie-Laure and Rouzaud, Yves", title = "A Study on Components and Assembly Primitives in {B}", booktitle = "Proceedings of 1st Conference on the {B} method", keywords = "modularity", crossref = "B96-Habrias", institution = "{IMAG-LSR}, Grenoble, F", pages = "47--62", URL = "http://www-lsr.imag.fr/users/Didier.Bert/Papers/firstB.ps.gz", } @InProceedings{B96-Burdy, author = "Burdy, Lilian", title = "Obligations de preuve de raffinement en {B}", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "{MATRA} {T}ransport {I}nternational, Montrouge, F", pages = "121--132", } @InProceedings{B96-Butler, author = "Butler, Michael J. and Wald{\'e}n, M.", title = "Distributed System Development in {B}", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "Univ. of Southampton (UK), Abo Akademi University (turku,Finland)", pages = "155--168", } @InProceedings{B96-Chauvet, author = "Chauvet, Jean-Yves", title = "Une {\'e}tude de cas en {B}: les feux tricolores", booktitle = "Proc. of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "{CNAM}, Tours, F", pages = "329--352", } @InProceedings{B96-Clutterbuck, author = "Clutterbuck, D. and Bicarregui, J. and Matthews, B.", title = "Experiences with Proof in a Formal Development", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "Praxis Critical Systems, Rutherford Appleton Lab, UK", pages = "27--46", } @InProceedings{B96-Draper, author = "Draper, Jonathan", title = "The use of the {B-Method} on an avionics example - the {MIST} Project", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "{GEC-Marconi Avionics Ltd}, Rochester, UK", pages = "303--305", } @InProceedings{B96-Dune, author = "Dunne, Steve and Stoddart, Bill", title = "Hypersubstitutions : Extending the Generalised Substitution to Model Semi-decidable Operations", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "University of Teesside, Middlesbrough, UK", pages = "221--237", } @InProceedings{B96-El-Koursi, author = "El Koursi, El Miloudi and Mariano, Georges", title = "Safety Critical Software Assessment : Past Experience and New Approach", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "INRETS-ESTAS, Villeneuve d'Ascq, France", pages = "11--26", } @InProceedings{B96-Facon, author = "Facon, P. and Laleau, R. and Nguyen, H. P.", title = "{D}{\'e}rivation de sp{\'e}cifications formelles {B} {\`a} partir de sp{\'e}cifications semi-formelles de syst{\`e}mes d'information", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "CEDRIC-IIE, {CNAM}, F", pages = "271--290", } @InProceedings{B96-Fraer, author = "Fraer, Ranan", title = "Formal Development in {B} of a Minimum spanning Tree Algorithm", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "INRIA, Sophia-Antipolis, F", pages = "305--328", URL = "ftp://ftp-sop.inria.fr:/pub/croap/rfraer/papers/mst.ps.gz", } @Proceedings{B96-Habrias, title = "Proceedings of the 1st Conference on the {B} method", year = "1996", key = "B96-Habrias", editor = "Habrias, Henri", series = "Putting into Practice methods and tools for information system design", organization = "B1996, {IRIN} Institut de recherche en informatique de Nantes", address = "3 rue du Mar{\'e}chal Joffre, BP 34103, 44041 Nantes Cedex 1", month = nov, } @InProceedings{B96-Lano, author = "Lano, Kevin and Bicarregui, J. and Sanchez, A.", title = "Using {B} to design and Verify Controllers for Chemical Processing", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "Imperial College, London, UK", pages = "237--270", } @InProceedings{B96-Lopez, author = "Lopez, N.", title = "La construction de la sp{\'e}cification formelle d'un syst{\`e}me complexe", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "{{CNAM}}, Paris, F", pages = "63--120", } @InProceedings{B96-Mery, author = "M{\'e}ry, Dominique", title = "Machines Abstraites Temporelles. Analyse Comparative de {B} et {TLA+}", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", keywords = "TLA", institution = "Univ. de Nancy, CRIN, Institut Univ. de France, F", pages = "169--191", } @InProceedings{B96-Robinson, author = "Robinson, K. A.", title = "Early Experiences in Teaching the {B}-{Method}", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "Univ. of New South Wales, Sydney, Australia", pages = "297--302", abstract = "This paper describes some of the experiences of teaching software development using the {B}-Method and the {B}-Toolkit to a small class of postgraduate students at the University of New South Wales. Difficulties experienced and lessons learnt are discussed.", } @InProceedings{B96-Shore, author = "Shore, Richard", title = "Object-Oriented Modelling in {B}", booktitle = "Proceedings of 1st Conference on the {B} method", crossref = "B96-Habrias", institution = "University of Teesside, Middlesbrough, UK", pages = "133--154", } @InProceedings{B98-Abrial, author = "Abrial, Jean-Raymond and Mussat, Louis", title = "Introducing Dynamic Constraints in {B}.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "83--128", URL = "http://www.atelierb.societe.com/ressources/articles/IDCiB.pdf", abstract = "In {B}, the expression of dynamic constraints in notoriously missing. In this paper, we make various proposals for introducing them. They all express, in different complementary ways, how a system is allowed to evolve. Such descriptions are independent of the proposed evolutions of the system, which are defined, as usual, by means of a number of operations. Some proof obligations are thus proposed in order to reconcile the two points of view. We have been very careful to ensure that these proposals are compatible with refinement. They are illustrated by several little examples, and a larger one. In a series of small appendices, we also give some theoretical foundations to our approach. In writing this paper, we have been heavily influenced by a pioneering works of Z. Manna and P. Pnueli, L. Lamport, R. Back and M. Butler.", } @InProceedings{B98-Banach, author = "Banach, R. and Poppleton, M.", title = "Retrenchment: An Engineering Variation on Refinement.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "129--147", URL = "http://www.cs.man.ac.uk/~banach/some.pubs/Retrench.Eng.Var.Ref.ps.gz", abstract = "It is argued that refinement, in which I/O signatures stay the same, preconditions are weakened and postconditions strengthened, is too restrictive to describe all but a fraction of many realistic developments. An alternative notion is proposed called retrenchment, which allows information to migrate between I/O and state aspects of operations at different levels of abstraction, and which allows only a fraction of the high level behaviour to be captured at the low level. This permits more of the informal aspects of design to be formally captured and checked. The details are worked out for the {B}-Method.", } @InProceedings{B98-Behm, author = "Behm, P. and Burdy, L. and Meynadier, J.-M.", title = "Well Defined {B}.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "29--45", abstract = "B is a language with a three valued semantics: terms like min({}) can be ill defined, consequently formulas containing ill defined terms can also be ill defined or not. Therefore the deduction system we use for the proof obligations proof should be constructed from a three valued logic. Here, we present a deduction system which allows to make proofs in two valued logic if new proof obligations called well definedness lemmas are also proved. We define this deduction system and the new proof obligations that ensure the well definedness of {B} machines. The soundness of this new deduction system is not proved here but we completely define the well definedness lemmas for machine, refinement and implementation.", } @InProceedings{B98-Chartier, author = "Chartier, Pierre", title = "Formalisation of {B} in {I}sabelle/{HOL}.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "66--82", abstract = "We describe a semantic embedding of the basic concepts of the {B} language in the higher-order logic instance of the generic theorem prover Isabelle (IsabelleHOL). This work aims at a foundation to formalise the full abstract machine notation, in order to produce a formally checked proof obligation generator. The formalisation is based on the {B}-Book \cite{BBook}. First we present an encoding of the mathematical basis. Then we formalise generalised substitutions by the before-after model and we prove the equivalence with the weakest precondition axiomatic model. Finally we define operations and abstract machines.", } @InProceedings{B98-Ducasse, author = "Ducasse, Mireille", title = "Teaching {B} at a Technical University is Possible and Rewarding", crossref = "B98-educational", URL = "http://www.irisa.fr/lande/ducasse/B-edu-98.ps.gz", } @InProceedings{B98-Heuberger, author = "Heuberger, Ph.", title = "Two Strategies to Data-refine an Equivalence to a Forest.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "261--272", address = "Turku Centre for Computer Science (TUCS), {\AA}bo Akademi University, Finland.", abstract = "Well-known strategies give incentive to the algorithmic refinement of programs and we ask in this paper whether general patterns also exist for data refinement. In order to answer this question, we study the equivalence relation problem and identify the motivations to replace the equivalence relation by a data structure suitable for efficient computation.", } @InProceedings{B98-Julliand, author = "Julliand, Jacques and Legeard, Bruno and Machicoane, T. and Parreaux, B. and Tatibou{\"e}t, Bruno", title = "Specification of an Integrated Circuit Card. Protocol Application using the {B} method and Linear Temporal Logic.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "273--292", abstract = "In this paper we propose a construction method of multiformalism specifications based on {B} and linear temporal logic. We examined this method with a case study of communication protocol between an integrated circuit card and a device such a terminal studied in collaboration with the Schlumberger company. We show the current advantages and limits to joining many specifications formalisms the associated toolkits ; Atelier {B} and SPIN. Finally, we draw a few conclusions about future directions of research on the proof of heterogeneous specifications, incremental verification and on tool cooperation to assist in the verification step (e.g. a prover, a model-checker and an animator)", keywords = "communication protocol, model-checking, SPIN, AtelierB, linear temporal logic, smartcards", } @InProceedings{B98-Malioukov, author = "Malioukov, A.", title = "An Object-Based Approach to the {B} Formal Method.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "162--181", abstract = "In this paper, we describe an approach to the design of distributed systems that integrate object-oriented methods (OOM) and the non object- oriented {B} formal method. Our goal is to retain some OOM advantages and produce a flexible and reliable specification, and through the use of our example we show how this is achieved. We prove formally that our design meets its informal specification with the help of {B}-Toolkit Release 3.3.1. We illustrate the approach by the B specification of A Computerized Visitor Information System (ACVIS). Using Object Modeling Technique diagrams allows us to make ACVIS more readable and open for changes.", keywords = "object-oriented, distributed systems", } @InProceedings{B98-Matthews, author = "Matthews, B. and Ritchie, B. and Bicarregui, J.", title = "Synthesising structure from flat specifications.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", URL = "http://theory.doc.ic.ac.uk:80/~jcb1/vdmbpapers.html", pages = "148--161", abstract = "Within the design process, a high-level specification is subject to two conflicting tensions. It is used as vehicle for validating the requirements, and also as a first step of the refinement process. Whilst the structuring mechanisms available in the {B} method are well-suited for the latter purpose, the rich type constructions of VDM are useful for the former. In this paper we propose a method which synthesises a structured {B} design from a flat VDM specification by analysing how type definitions are used within the VDM state in order to generate a corresponding {B} machine hierarchy.", } @InProceedings{B98-Petin, author = "P{\'e}tin, J.-F. and Morel, G. and M{\'e}ry, D. and Lamboley, P.", title = "Process control engineering: contribution to a formal structuring framework with the {B} method.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "198--209", abstract = "This paper explores the use of the {B} method as a formal framework for structuring and verifying the process control systems engineering. In particular, it is shown how the {B} method can be used to define implementation independent modular specifications. {B}enefits are related to the re-use of verified and perennial specifications for the control system facing with a fast evolution of the implementation technologies. Limits are related to the compliance of formal methods with the other methods or methodologies involved in the development of a production system. That justifies a methodological framework needed for representing, reasonning and verifying the control system as interacting with other technological or human systems. The approach is illustrated and discussed using a level control system example.", } @InProceedings{B98-Potet, author = "Potet, Marie-Laure and Rouzaud, Yann", title = "Composition and Refinement in the {B} method.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "46--65", abstract = "In this paper, we propose a framework to study refinement of abstract machines in the {B} method. It allows us to properly deal with shared variables, possibly introduced by composition primitives SEES and IMPORTS. We exhibit local conditions on components which are sufficient to ensure global correctness of a software system. Finally, we show how restrictions on the architecture of software systems may guarantee these conditions.", } @InProceedings{B98-Sekerinski, author = "Sekerinski, E.", title = "Graphical Design of Reactive Systems.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "182--197", abstract = "Reactive systems can be designed graphically using statecharts. This paper presents a scheme for the translation of statecharts into Abstract Machine Notation (AMN) of the {B} method. By an example of a conveyor system, we illustrate how the design can be initially expressed graphically with statecharts, then translated to AMN and analysed in AMN, and then further refined to executable code.", URL = "http://www.cas.mcmaster.ca/~emil/publications/statechartsinb/index.html", keywords = "statecharts, reactive systems, conveyor system, case study", } @InProceedings{B98-Stoddart, author = "Stoddart, B. and Dunne, S. and Galloway, A. and Store, R.", title = "Abstract State Machines: Designing Distributed Systems with State Machines and {B}.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "226--242", abstract = "We outline a theory of communicating state machines. The state of our machines can be factored into a behavioural state and a data state. The behavioural states are shown on a state diagram, whose transitions are labelled with {B} operations which describe I/O and changes to the machines data state. The paper includes simple examples, the translation of Abstract State Machines to {B} Action Systems, the translation of high level Abstract State Machines into primitive Abstract State Machines, the parallel combination of high level Abstract State Machines, and short notes on pre-conditions, choice, refinement, and time.", keywords = "distributed systems, action systems", } @InProceedings{B98-Traverson, author = "Taouil-Traverson, S. and Vignes, S.", title = "Designing a {B} model for safety-critical software systems.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "210--225", abstract = "The observations described in this paper are based on the experience we gained in applying the {B} method to a realistic safety-critical case study. The main goal was to integrate the {B} method into the heart of development cycle, particularly for such applications. We outline a framework to reason about control process systems in order to capture functional and safety- related properties and to organise the conceptual architecture of these systems. Thus, we describe how a {B} Model can be designed both with respect to safety constraints and in terms of software architecture abstractions. We use the {B} method to support architectural abstraction, codifying the interactions of components. Finally, we present essential results of the case study and we show the significant impact of such a {B} formal development on the development process by giving some metrics.", } @InProceedings{B98-Treharne, author = "Treharne, Helen and Draper, Jonathan and Schneider, Steve", title = "Test Case Preparation using a Prototype.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "293--311", abstract = "This paper reports on the preparation of test cases using a prototype within the context of a formal development. It describes an approach to building a prototype using an example. It discusses how a prototype contributes to the testing activity as part of a lifecycle based on the use of formal methods. The results of applying the approach to an embedded avionics case study are also presented.", keywords = "testing, avionics, case study", } @InProceedings{B98-Walden, author = "Wald{\'e}n, M.", title = "Layering Distributed Algorithms within the {B}-method.", booktitle = "B'98 : The 2nd International {B} Conference", crossref = "B98", pages = "243--260", address = "Turku Centre for Computer Science (TUCS), {\AA}bo Akademi University, Finland.", abstract = "Superposition is a powerful program modularization and structuring method for developing parallel and distributed systems by adding new functionality to an algorithm while preserving the original computation. We present an important special case of the original superposition method, namely, that considering each new functionality as a layer that is only allowed to read the variables of the previous layers. Thus, the superposition method with layers structures the presentation of the derivation. Each derivation step is, however, large and involves many complicated proof obligations. Tool support is important for getting confidence in these proofs and for administering the derivation steps. We have chosen the {B}-method for this purpose. We propose how to extend the {B}-method to make it more suitable for expressing the layers and assist in proving the corresponding superposition steps in a convenient way.", keywords = "B extension, distributed algorithms", } @Proceedings{B98, title = "{B}'98 : The 2nd International {B} Conference, Recent Advances in the Development and Use of the {B} Method", editor = "Bert, Didier", key = "B98", series = LNCS, volume = "1393", year = "1998", organization = "B1998, {LIRRM} Laboratoire d'Informatique, de Robotique et de Micro-{\'e}lectronique de Montpellier", publisher = "Springer-Verlag", address = "Montpellier", month = apr, } @Proceedings{B98-educational, title = "{B}'98 : The 2nd International {B} Conference, Proceedings of the Educational Session", editor = "Habrias, H. and Dunn, S. E.", key = "B98-educational", year = "1998", organization = "Association de Pilotage des Conf{\'e}rences B", address = "Nantes", month = apr, } @InProceedings{BB94, author = "Bieber, Pierre and Boulahia-Cuppens, N.", title = "Formal Development of Authentication Protocols", booktitle = "Proceedingsof BCS-FACS Sixth Refinement Workshop", abstract = "In this paper, we apply the {B} method to the formal development of authentification protocols. Our approach consists in first providing a very abstract specification of authentification, and then refining progressively this specification in order to obtain an authentification protocol. During the refinement process we consider various ways to use encrypted messages and to distribute encryption keys that relate with several existing protocols.", keywords = "B-Method, AMN, formal development, abstract specification, authentication, protocols", URL = "http://www.cert.fr/francais/deri/bieber/papers/refinement.ps.gz", year = "1994", } @InProceedings{BBLW93, author = "Bieber, Pierre and Boulahia-Cuppens, N. and Lehmann, T. and Van Wickeren, E.", title = "Abstract Machines for Communication Security", booktitle = "Proceedingsof IEEE Workshop on Foundations of Computer Security VI", abstract = "We use an existing formal software developement method called {B} in order to build and verify specification of a communication channel, cryptographic fonctions and security properties. We show on an example how these basic specifications may be combinated in order to write abstract specifications of cryptographic protocols and to verify their security.", keywords = "B-Method, AMN, formal software developement, communication channel, cryptographic protocol", URL = "http://www.cert.fr/francais/deri/bieber/papers/pierre.franconia93.ps.gz", year = "1993", } @Book{BBook, author = "Abrial, Jean-Raymond", title = "The {B}~Book - Assigning Programs to Meanings", publisher = "Cambridge University Press", ISBN = "0-521-49619-5", year = "1996", month = aug, } @Proceedings{BUGM99, title = "{FM}'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", year = "1999", publisher = "Springer-Verlag", } @InProceedings{BUGM99-Bellegarde, author = "Bellegarde, Fran{\c{c}}oise and Julliand, Jacques and Mountassir, Hassan", title = "Model-based verification through refinement of {B} event systems", booktitle = "FM'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", keywords = "event-B", crossref = "BUGM99", pages = "16--26", } @InProceedings{BUGM99-Bodeveix, author = "Bodeveix, Jean-Paul and Filali, Mamoun and Mun{\~o}z, C{\'e}sar", title = "A Formalization of the {B} method in {Coq} and {PVS}", booktitle = "FM'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", crossref = "BUGM99", pages = "32--48", } @InProceedings{BUGM99-Burdy, author = "Burdy, Lilian and Meynadier, Jean-Marc", title = "Automatic Refinement", booktitle = "FM'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", crossref = "BUGM99", pages = "3--15", } @InProceedings{BUGM99-Butler, author = "Butler, Michael J.", title = "An overview of the {CSP2B} Tool", booktitle = "FM'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", crossref = "BUGM99", pages = "1--2", } @InProceedings{BUGM99-Lano, author = "Lano, Kevin and Bicarregui, Juan and Sanchez, A.", title = "Invariant-based Synthesis and Composition of Control Algorithms using {B}", booktitle = "FM'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", crossref = "BUGM99", pages = "69--86", URL = "http://theory.doc.ic.ac.uk/~jcb1/", } @InProceedings{BUGM99-Lopez, author = "Lopez, Nestor", title = "An {``}{event based B}{''} industrial experience", booktitle = "FM'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", keywords = "event-B", crossref = "BUGM99", pages = "87", } @InProceedings{BUGM99-Stoddart, author = "Stoddart, Bill and Dunne, Steve and Papatsaras, Antonis", title = "A graphical interface tool to support modelling and refinement in {B} using communicating Abstract State Machines", booktitle = "FM'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", crossref = "BUGM99", pages = "27--32", } @InProceedings{BUGM99-Treharne, author = "Treharne, Helen and Schneider, Steve", title = "Classifying and capturing timing requirements", booktitle = "FM'99 -- {B} Users Group Meeting -- Applying {B} in an industrial context : Tools, Lessons and Techniques", keywords = "time requirements", crossref = "BUGM99", pages = "49--68", } @TechReport{BUT-D2, author = "Matthews, Brian and Bicarregui, Juan", title = "Architecture for Proof Engineering: a comparison of two models of support for the proof process", institution = "B User Trial", year = "1994", key = "BUT-D2", type = "Deliverable", number = "BUT/RAL/BMM/12/V1", address = "Rutherford Appleton Laboratory, Chilton, Oxon, OX11 0QX", month = jun, abstract = "Contact authors.", } @TechReport{BUT-D8, author = "Bicarregui, Juan and Matthews, Brian", title = "Architecture for Structuring Proof", institution = "B User Trial", year = "1994", key = "BUT-D8", type = "Deliverable", number = "BUT/RAL/BMM/11/V1", address = "Rutherford Appleton Laboratory, Chilton, Oxon, OX11 0QX", month = apr, abstract = "Contact authors.", } @PhdThesis{Baron-2003, author = "Baron, Micka{\"e}l", title = "Vers une approche s{\^u}re du d{\'e}veloppement des Interfaces Homme-Machine", school = "Universit{\'e} de Poitiers", year = "2003", month = dec, keywords = "HCI, formal methods, B-Method, model-based systems, task validation", abstract = "Les interfaces homme-machine (IHM) constituent une part indispensable dans la quasi-totalit{\'e} des syst{\`e}mes informatiques. Le recours {\`a} des notations de description des IHM, et {\`a} des mod{\`e}les de sp{\'e}cification, de d{\'e}veloppement, de v{\'e}rification et de validation devient indispensable pour assurer que le syst{\`e}me satisfait les propri{\'e}t{\'e}s d{\'e}finissant la notion d'utilisabilt{\'e}. Aujourd'hui, on peut consid{\'e}rer que deux approches exploitant les mod{\`e}les du domaine de l'IHM peuvent {\^e}tre mises en parall{\`e}le pour la v{\'e}rification de propri{\'e}t{\'e}s : les approches fond{\'e}es sur le d{\'e}veloppement formel et les approches fond{\'e}es sur la d{\'e}finition d'outils. Malgr{\'e} des avanc{\'e}es int{\'e}ressantes, aucune d'elles n'est encore parvenue {\`a} s'imposer. Nous proposons dans cette th{\`e}se deux nouvelles approches permettant le d{\'e}veloppement s{\^u}r d'interfaces homme-machine, fond{\'e}es sur une m{\^e}me m{\'e}thode formelle (la m{\'e}thode B). La premi{\`e}re fond{\'e}e sur le d{\'e}veloppement formel permet, d'int{\'e}grer des notations et des techniques h{\'e}t{\'e}rog{\`e}nes du domaine de l'IHM dans une seule et unique m{\'e}thode formelle (la m{\'e}thode B), afin d'exprimer, v{\'e}rifier et valider des propri{\'e}t{\'e}s du syst{\`e}me interactif. La seconde, fond{\'e}e sur la d{\'e}finition d'outils, (SUIDT), permet de concevoir de mani{\`e}re interactive le dialogue entre un noyau fonctionnel d{\'e}velopp{\'e} formellement en {B} et une pr{\'e}sentation graphique de l'interface, tout en garantissant le respect des propri{\'e}t{\'e}s exprim{\'e}es {\`a} la fois dans le noyau fonctionnel et au niveau des t{\^a}ches de l'utilisateur.", } @Book{Bcases98, editor = "Sekerinski, E. and Sere, K.", title = "Program Development by Refinement : Case Studies Using the {B} Method", publisher = "Springer-Verlag London", year = "1998", key = "Bcases98", number = "ISBN 1-85233-053-8", series = FACIT, URL = "http://www.cs.abo.fi/Bcases/", month = dec, } @InBook{Bcases98-Robinson, author = "Robinson, Ken", title = "Introduction to the {B} Method", publisher = "Springer", crossref = "Bcases98", } @InProceedings{Behm93, author = "Behm, Patrick", title = "Application d'une m{\'e}thode formelle aux logiciels s{\'e}curitaires ferroviaires", booktitle = "Atelier Logiciel Temps R{\'e}el, 6{\`e}me Journ{\'e}es Internationales du G{\'e}nie Logiciel", abstract = "La m{\'e}thode {B} est utilis{\'e} {\`a} {M}atra {T}ransport pour la formalisation des logiciels s{\'e}curitaires des automatismes de {\em METEOR}, la future ligne parisienne de m{\'e}tro sans conducteur. Nous pr{\'e}sentons plus particuli{\`e}rement la formalisation du {\em Pilote Automatique Embarqu{\'e}} et nous t{\^a}chons de d{\'e}gager de cette exp{\'e}rience des {\'e}l{\'e}ments de r{\'e}ponse au probl{\`e}me de l'application des m{\'e}thodes formelles aux d{\'e}veloppements industriels", keywords = "B-Method, METEOR, formal method, safety-critical software, railway", year = "1993", } @InBook{Behm97, author = "Behm, Patrick and Desforges, Pierre and Mejia, Fernando", title = "Application de la m{\'e}thode {B} dans l'industrie ferroviaire", chapter = "3", keywords = "railway", pages = "59--88", crossref = "arago20", } @PhdThesis{Behnia-PhD, author = "Behnia, Salimeh", title = "Test de mod{\`e}les formels en {B} : cadre th{\'e}orique et crit{\`e}res de couvertures", school = "Institut National Polytechnique de Toulouse", year = "2000", URL = "http://ethesis.inp-toulouse.fr/archive/00000008/01/behnia.pdf", month = oct, } @TechReport{Behnia98, author = "Behnia, Salimeh and Waeselynck, H{\'e}l{\`e}ne", title = "External verification of a {B} development process", institution = "LAAS (TSF) -- INRETS (ESTAS)", year = "1998", pages = "4", number = "98085", } % Additional information: 5th-9th January @InProceedings{Bert-2002, author = "Bert, Didier", title = "Event System Specification in {B} and Representation as Finite Labelled Transition Systems", booktitle = "IFIP WG1.3, L'Alpe d'Huez (France)", year = "2002", month = jan, abstract = "The talk first introduces the {B} specification method. {B} belongs to model-oriented specification methods. Data specification relies upon Set Theory, static and invariant properties are written in First-Order Logic and actions (operations) are described by predicate transformers. A specification unit is called a {``}machine{''} which encapsulates a state and provides exported operations. A machine can be refined by another kind of unit called {``}refinement{''}. The last refinement in a development chain is called an {``}implementation{''}. These units must fulfill syntactic conditions. For example, operations in implementations must be fully deterministic. Moreover, it is possible to combine machines by the way of aggregating links {``}includes{''} and {``}uses{''}. A complex development can be split in a structured way by means of {``}imports{''} and {``}sees{''} primitives. Validation conditions (called proof obligations) ensures that operations preserve the invariant of the state and that a refinement preserves the observable effect of the machine (or the refinement) that it refines. Event systems are an extension of the formalism that allow the user to specify systems evolving by means of {``}events{''}. The events may be triggered only if their guard is true. The theoretical framework of Event-B is the same as the one of classical B. Nevertheless, refinement conditions are more flexible because they allow introduction of new events which are not present (or not perceptible) at a more abstract level. So, it is admitted that Event-B is more powerful than classical {B} from a user point of view. For a presentation of Event-B. The second part of the talk is devoted to the presentation of the construction of finite labelled transition systems (LTS) from {B} abstract systems. This work is done in our team to investigate the benefits of a (sometimes partial) representation of the behaviour of {B} event systems. We choose to decompose the state of an abstract system in several disjunctive predicates. These predicates provide the basis for defining a set of states which are the nodes of the LTS, while the events are the transitions. We illustrate the method by developing the SCSI-2 (Small Computer Systems Interface) input-output system. We intend to carry out a connection between the {B} environment (Atelier B) and the Caesar/Aldebaran Development Package (CADP) which is able to deal with finite LTS.", } @InProceedings{Bert2003, author = "Bert, Didier and Boulm{\'e}, Sylvain and Potet, Marie-Laure and Requet, Antoine and Voisin, Laurent", title = "Adaptable translator of {B} specifications to embedded {C} programs", booktitle = "Formal Methods Europe 2003", pages = "94--113", year = "2003", editor = "Araki, K. and Gnesi, S. and Mandrioli, D.", volume = "2805", keywords = "code generation", organization = "Formal Methods Europe", publisher = "Springer-Verlag", } @InProceedings{BiRi93, author = "Bicarregui, J. and Ritchie, B.", title = "Invariants, Frames and Postconditions: a Comparison of the {VDM} and {B} Notations", organization = "FME'93 Proceedings", booktitle = "FME'93", URL = "http://theory.doc.ic.ac.uk:80/~jcb1/vdmbpapers.html", series = LNCS, volume = "670", editor = "Springer-Verlag", year = "1993", } @Article{BiRi95, title = "Invariant, Frames and Postconditions: a Comparison of the {VDM} and {B} notations", author = "Bicarregui, Juan and Ritchie, Brian", journal = "IEEE Transaction On Software Engineering", volume = "21", number = "2", pages = "79--89", month = feb, crossref = "BiRi93", year = "1995", abstract = "{VDM} and {B} are two ``model-oriented'' fromal methods. Each gives a notation for the specification of systems as state machines in terms of a set of states with operations defined as relations on that set.\\ \ldots \\ This paper makes a comparison of the two notations throuhg an example of a communications protocol previously formalized.\\ Particular attention is paid to three areas where the notations differ: the use of postconditions that enforce it; the explicit ``framing'' of operations as ooposed to the ``minimal frame'' approach; and the use of relationnal postconditions as opposed to generalized substitutions. (9 Refs)", keywords = "AMN, B-Method, formal methods, model-oriented specification, VDM", } @InProceedings{Bicarregui95, title = "Formal methods in practice: a comparison of two support systems for proof", author = "Bicarregui, J. C. and Matthews, B. M.", year = "1995", ISBN = "3-540-60609-2", booktitle = "{SOFSEM} `95: {T}heory and {P}ractice of {I}nformatics. 22nd {S}eminar on {C}urrent {T}rends in {T}heory and {P}ractice of {I}nformatics. {P}roceedings", abstract = "{T}his paper discusses the use of formal methods in the light of experience gained from two industrial projects using the {B} {A}bstract {M}achine {N}otation. {A} simple example is presented which demonstrates the use of formal specification, refinement and proof in the {B}-{M}ethod, and this is compared with a similar development in {VDM}. {T}he role of fully formal proof is considered and, in particular, the construction of application specific theories for balancing automation and interaction in the verification of designs is explored. (24 {R}efs)", keywords = "formal methods, industrial projects, AMN, formal specification, refinement, proof, B-Method, VDM, fully formal proof, application specific theories, design verification, specification language, B-Toolkit", } @Article{Bicarregui97, author = "Bicarregui, J. C.", title = "Formal Methods Into Practice: case studies in the application of the {B} Method", journal = "IEE Proceedings on Software Engineering", URL = "http://theory.doc.ic.ac.uk:80/~jcb1/vdmbpapers.html", year = "1997", volume = "144", number = "2", pages = "119--133", month = apr, } @InProceedings{Bicarregui98, author = "Lano, Kevin and Bicarregui, J. C. and Kan, P.", title = "Experiences of Using Formal Methods for Chemical Process Control Specification", book = "INCOM'98", year = "1998", pages = "119--133", month = jun, } @Article{Bieber96a, author = "Bieber, Pierre", title = "Interpr{\'e}tation d'un mod{\`e}le de s{\'e}curit{\'e}", journal = "Techniques et Sciences Informatiques", year = "1996", volume = "15", number = "6", month = apr, URL = "ftp://ftp.cert.fr/pub/ssi/acsac96.ps.gz", abstract = "Cet article d{\'e}crit une application des m{\'e}thodes formelles dans le cadre du d{\'e}veloppement d'un produit de s{\'e}curit{\'e}. Le travail r{\'e}alise vise a permettre une {\'e}valuation de la s{\'e}curit{\'e} selon les crit{\`e}res ITSEC. Pour cela un mod{\`e}le formel de securite a {\'e}t{\'e} d{\'e}velopp{\'e}. Ce mod{\`e}le a {\'e}t{\'e} d{\'e}crit et v{\'e}rifi{\'e} a l'aide de la m{\'e}thode {B}. Puis il a {\'e}t{\'e} mis en correspondance avec les sp{\'e}cifications du produit. Ce travail d'interpr{\'e}tation du mod{\`e}le a permis de guider la conception des fonctions de securite du produit. Available at ftp://ftp.cert.fr/pub/ssi/acsac96.ps.gz", } @InProceedings{Bieber96b, author = "Bieber, Pierre", title = "Formal Techniques for an {ITSEC-E4} Secure Gateway", booktitle = "proceedings of the 12th Annual Computer Security Applications Conference", year = "1996", organization = "IEEE computer society press", month = dec, abstract = "In this paper we describe the method used to develop a gateway capable of meeting the ITSEC E4 requirements. The security policy was formally modelled and proven consistent with the functional specifications by means of an interactive theorem prover. The formalisms were used to assist in the design of the security architecture. Available at ftp://ftp.cert.fr/pub/ssi/tsi.ps.gz", URL = "ftp://ftp.cert.fr/pub/ssi/tsi.ps.gz", } @PhdThesis{Bon-PhD, author = "Bon, Philippe", title = "Du cahier des charges aux sp{\'e}cifications formelles : une m{\'e}thode bas{\'e}e sur les r{\'e}seaux de Petri de haut niveau", school = "Universit{\'e} des Sciences et Techniques de Lille", year = "2000", month = oct, keywords = "Petri nets, formal specification", } @Book{Bos92, author = "Bosilca, Gheorghe", title = "{D}{\'e}veloppement et Preuve formelle de programmes", publisher = "M{\'e}moire de DEA. Universit{\'e} d'Orsay Paris XI", year = "1992", abstract = "En reprenant l'exp{\'e}rience d'autres disciplines scientifiques, la communaut{\'e} informatique a d{\'e}velopp{\'e} son propre mod{\`e}le pour repr{\'e}senter le cycle de vie d'un produit informatique. Depuis 1968 ont {\'e}t{\'e} d{\'e}velopp{\'e}es des m{\'e}thodes formelles de d{\'e}veloppement d'un produit informatique afin de r{\'e}aliser leurs preuves formelles de correction. Quelques unes sont pass{\'e}es dans la pratique industrielle, permettant quelques fois d'affirmer {\`a} la l{\'e}g{\`e}re que {\em le produit a {\'e}t{\'e} prouv{\'e} du point de vue math{\'e}matique} comme une garantie totale en ce qui concerne sa correction absolue.", keywords = "B-Method, substitution, formal proof, formal development", } @InProceedings{Boulanger2001, author = "Boulanger, J.-L. and Mariano, Georges and Aljer, Ammar", title = "Conception s{\^u}re de circuits bas{\'e}e sur la notion de propri{\'e}t{\'e}", booktitle = "ICSSEA'2001 -- 14th Int. Conf. on Software Systels Engineering and Their Applications", year = "2001", volume = "2", address = "{CNAM}, Paris, France", month = dec, } @Book{Bro93, author = "Brossard, M.", title = "Sp{\'e}cification, programmation et preuve formelles. Tome 2: Technique ensemblistes", publisher = "France T{\'e}l{\'e}com CNET", year = "1993", month = dec, abstract = "Ce tome 2 est consacr{\'e} {\`a} la famille des langages ensemblistes comme {Z} ou {B}, et {\`a} la technique d'{\'e}criture de programme de Dijkstra. Les diverses techniques sont abord{\'e}es sous l'angle de la comparaison. Outre leurs principales caract{\'e}ristiques, on trouvera les points communs qu'elles pr{\'e}sentent et leurs diff{\'e}rences fondamentales.", keywords = "set-theory languages, Z, B-Method, rewriting", } @InProceedings{Btoolkit, author = "anonymous", title = "{T}he {B}-{T}oolkit demonstration", year = "1995", ISBN = "3-540-59293-8", booktitle = "{TAPSOFT}'95: {T}heory and {P}ractice of {S}oftware {D}evelopment. 6th {I}nternational {J}oint {C}onference {CAAP}/{FASE}. {P}roceedings", abstract = "{T}he {B}-{T}oolkit is a suite of integrated programs which implement the {B}-{M}ethod for software development. {T}he {B}-{M}ethod is a collection of mathematical based techniques which give a formal basis to those activities of software development that range from software specification, through design and integration, to code generation and into maintenance. {T}he {B}-{T}oolkit's components tools are implemented in the {B} {T}heory {L}anguage and is interpreted by the {B}-{T}ool. {T}he {B} {T}heory {L}anguage is a special purpose language for writing software engineering tools including interactive and automatic proof assistants and other tools where pattern matching, substitution and rewrite mechanisms are used (e.g. translators, interpreters and generators). (0 {R}efs)", keywords = "B-Toolkit, demonstration, integrated program suite, B-Method, software development, mathematical based techniques, formal method, software specification, code generation, maintenance, B theory language, B-tool, special purpose language, software engineering tool writing, interactive proof assistants, automatic proof assistants, pattern matching, substitution, rewrite mechanisms, tools", } @InProceedings{BuechiICFEM98, author = "B{\"u}chi, Martin", title = "The {B} Bank: {A} Complete Case Study", booktitle = "Proceedings of ICFEM98, the Second International Conference on Formal Engineering Methods", publisher = "IEEE Press", URL = "http://www.abo.fi/~mbuechi/publications/BBank.html", pages = "190--199", month = dec, year = "1998", } @PhdThesis{Burdy-PhD, author = "Burdy, Lilian", title = "Traitement des expressions d{\'e}pourvues de sens de la th{\'e}orie des ensembles: Application {\`a} la m{\'e}thode {B}", school = "CEDRIC-{CNAM}", year = "2000", URL = "http://cedric.cnam.fr/PUBLIS/RC43.ps.gz", abstract = "Ce travail porte sur la d{\'e}finition d'une logique pour un langage avec fonctions partielles. Une interpr{\'e}tation tri-valu{\'e}e est choisie pour les formules. A partir de cette s{\'e}mantique, une relation de cons{\'e}quence est d{\'e}finie et deux syst{\`e}mes de d{\'e}duction incorporant les preuves de bonne definition sont propos{\'e}s, le dernier a l'avantage de ne pas melanger les preuves de bonne d{\'e}finition avec les preuves usuelles et donne ainsi {\`a} l'utilisateur l'impression de toujours travailler dans une logique {\`a} deux valeurs. Ces choix ont {\'e}t{\'e} guides par le fait que ce syst{\`e}me a pour objectif d'{\`e}tre implant{\'e} dans un outil d'aide {\`a} la preuve. Ce travail a ete etendu sur un langage avec fonction partielle qui est le langage logique sous jacent {\`a} la m{\'e}thode B. Un outil de generation d'obligations de preuve de bonne definition estsp{\'e}cifie. Ces preuves sont ajout{\'e}es aux preuves de validation des diff{\'e}rents composants B.", } @Article{Butler02, author = "Butler, Michael J.", title = "A System-based Approach to the Formal Development of Embedded Controllers for a Railway", journal = "Design Automation for Embedded Systems", year = "2002", volume = "6", number = "4", month = jul, note = "ISSN 0929-5585", URL = "http://eprints.ecs.soton.ac.uk/6233/", keywords = "railway", } @InProceedings{CADE15, author = "Cirstea, Horatiu and Kirchner, Claude", title = "Using Rewriting and Strategies for Describing the {B} Predicate prover", booktitle = "CADE-15 : Workshop on Strategies in automated deduction", keywords = "proof, provers, rewriting, ELAN, B-Method", pages = "25--36", year = "1998", address = "Lindau, Germany", month = jul, URL = "http://www.loria.fr/~cirstea/Papers/StrategiesB-99-R-249.ps.gz", } @InProceedings{CBD2002-Petit, author = "Petit, Dorian and Poirriez, Vincent and Mariano, Georges", title = "Development of {F}ormal {C}omponents {U}sing the {B} {M}ethod", booktitle = "Proceedings of the First COLOGNET Joint Workshop on Component-based Software Development and Implementation Technology for Computational Logic Systems", pages = "35--46", year = "2002", editor = "Carro, Manuel and Vaucheret, Claudio and Lau, Kung-Kiu", number = "CLIP4/02.0", month = sep, keywords = "B-Method, code generation, design-by-contract, BRILLANT", URL = "http://www.univ-valenciennes.fr/ROI/dpetit/Biblio", ps = "http://www.univ-valenciennes.fr/ROI/dpetit/Biblio/Pub/CBD2002/cbd.ps", abstract = "The aim of this paper is to merge two approaches of software development. The first one is the component approach. Developping software components is now a new challenge in the software industry. The second approach is the formal one. These approaches are not so distant if we consider B. Meyer's opinion: a component without contracts can not be reused (more rigorously, he said that it was more complicated to reuse such a component). One of the difficulties with the design by contract approach is to find the contracts. In some formal approach -we will use the {B} method in this paper- the software properties (the contracts) are expressed in the specifications. We present in this paper a tool we have developped to generate code from {B} specifications. We will see how we can link the notion of component and the {B} specifications.", } @InProceedings{CCL97-Cirstea, author = "Cirstea, Horatiu and Kirchner, Claude", title = "Theorem Proving Using Computational Systems: The Case of the {B} Predicate Prover", booktitle = "Workshop CCL'97", year = "1997", address = "SchloB Dagstuhl, Germany", URL = "http://www.loria.fr/~cirstea/Papers/TheoremProver.ps.gz", keywords = "proof, rewriting, ELAN", month = sep, } @Article{CDDM92, author = "Carnot, M. and DaSilva, C. and Dehbonei, B. and Mejia, F.", title = "Error-free Software Development for critical Systems using the {B}-Methodology", journal = "IEEE", year = "1992", pages = "274--281", abstract = "The paper describes the process of software developpement for critical systems using the {B}-methodology designed by {Abrial}, Jean-Raymond", keywords = "railway critical systems, B-Method, AMN, substitution, type checker, proof and automatic prover", } @Article{CLPSB:STTT, author = "Bouquet, Fabrice and Legeard, Bruno and Peureux, Fabien", title = "{CLPS} {A} constraint solver to animate a {B} specification", journal = "International Journal on Software Tools for Technology Transfer (STTT)", year = "2004", keywords = "testing", volume = "6", number = "2", pages = "143--157", month = aug, abstract = "This paper proposes an approach to evaluating B formal specifications using constraint logic programming with sets (CLPS). This approach is used to animate and generate test sequences from {B} formal specifications. The solver, called CLPS-B, is described in terms of constraint domains, consistency verification, and constraint propagation. It is more powerful than most constraint systems because it allows the domain of variable to contain other variables, which increases the level of abstraction. The constrained state propagates the nondeterminism of the B specifications and reduces the number of states in a reachability graph. We illustrate this approach by comparing the constrained state graph exploration with the concrete one in a simple example \u2013 process scheduler. We also describe the automated test generation method that uses the CLPS-B solver to better control combinational explosion.", } % Additional information: 29-30 October @InProceedings{Cha92, title = "Vital coded processor and safety related software design", author = "Chapront, P.", organization = "Div. of Transp., GEC Alsthom, Saint-Ouen, France", booktitle = "Safety of Computer Control Systems 1992 (SAFECOMP 92) Computer Systems in Safety-Critical Applications. Proceedings of the IFAC Symposium", pages = "141--145", editor = "Frey, H. H.", publisher = "Pergamon, Oxford, UK", year = "1992", month = oct, abstract = "The implementation of a vital coded processor is discussed. Constraints of safety critical software for a train control system are described, and a presentation of formal methods is made. The {B}-method is described with more details on specification and design. Corresponding tools are mentioned. Some results obtained in application are given. Production of software for the vital coded processor is described and the link with the {B}-method is made. Conclusions of GEC ALSTHOM experience are given. (4 Refs)", keywords = "computerised control, error handling, formal specification, railway, safety systems, software reliability, software tools, vital coded processor, safety-critical software, train control system, formal methods, B-Method, GEC ALSTHOM", } @PhdThesis{Colin-PhD, author = "Colin, Samuel", title = "Contribution \`a l'int\'egration de temporalit\'e au formalisme {B}~: utilisation du calcul des dur\'ees en tant que s\'emantique pour {B}", school = "Universit\'e de Valenciennes et du Hainaut-Cambr\'esis", keywords = "formal methods, B-Method, temporal logic, duration calculus, proof assistant, Coq", year = "2006", month = oct, URL = "", abstract = "In the field of automated systems where reliability is the first requirement, formal methods proved to be efficient for the design of safe software. The dependency towards such systems is increasing, and the constraints to be met by these systems become more and more various and precise, particularly timed constraints. Some formal methods, notably the B method, make designing difficult under these constraints, because this is not what they have been made for in the first place. We therefore propose to extend the B method so that it can help specifying and validating systems with complex timed constraints. We use calculi of durations in order to express the semantics of the {B} language and deduce a conservative extension allowing its use in both its original context and in the context of time-constrained systems. We also study the problem of using a generic proof tool for validating duration calculus formulas. The genericity of this kind of tool helps answering the growing number of formal methods, but introduces the problem of adapting the mathematical foundations of such formal methods to a generic tool. We thus propose to study the implementation of duration calculus as a shallow embedding in the Coq proof assistant. We draw from it more general conclusions about the implementation of a particular modal logic in a generic-oriented tool.", } @InProceedings{Couchot2003, author = "Couchot, J.-F. and Dadeau, F. and Deharbe, D. and Giorgetti, A. and Ranise, S.", title = "Proving and Debugging Set-Based Specifications.", booktitle = "Proc. of the 6th Workshop on Formal Methods", year = "2003", address = "Campina Grande, PB, Brazil", month = oct, URL = "http://www.loria.fr/\~ranise/pubs/rvgo2B.ps.gz", organization = "UFCG", } @Booklet{DDM91, author = "DaSilva, C. and Dehbonei, B. and Mejia, F.", title = "Formal Specification in the Development of Industrial Applications: The Subway Speed Control Mechanism", pages = "207--221", keywords = "railway subway", year = "1991", organization = "FORTE91", } @InProceedings{DM94, author = "Dehbonei, Babak and Mejia, Fernando", title = "Formal Development of Software in Railways Safety Critical Systems", pages = "213--219", year = "1994", booktitle = "Railway Operations", editor = "Murthy, B. T. K. S. and Mellitt, C. A. and Brebbia, G. and Sciutto, S.", volume = "2", publisher = "Computational Mechanics Publications", organization = "COMPRAIL94", abstract = "Software is increasingly involved in the new generation of railways signalling systems. In systems such as interlocking, train routing devices or automatic train protection, electronic or electromechanical devices that previously provided safety critical functions are being replaced by computers", keywords = "B-Method, safety-critical software, railway", } @InCollection{DM94b, author = "Dehbonei, Babak and Mejia, Fernando", title = "Formal Methods in the Railways Signalling Industry", booktitle = "FME'94 : Industrial Benefits of Formal Methods", series = LNCS, volume = "873", editor = "Springer-Verlag", year = "1994", keywords = "railway", pages = "26--34", } @TechReport{DSSE-TR-96-6, author = "Butler, Michael J.", title = "An Approach to the Design of Distributed Systems with {B} {AMN}", institution = "Declarative Systems \& Software Engineering Group, Department of Electronics and Computer Science, University of Southampton", year = "1996", URL = "http://www.dsse.ecs.soton.ac.uk/techreports/96-6.html", month = sep, abstract = "In this paper, we describe an approach to the design of distributed systems with {B} AMN. The approach is based on the action-system formalism which provides a framework for developing state-based parallel reactive systems. More specifically, we use the so-called {CSP} approach to action systems in which interaction between subsystems is by synchronised message passing and there is no sharing of data. We show that the abstract machines of {B} may be regarded as action systems and show how reactive refinement and decomposition of action systems may be applied to abstract machines. The approach fits in closely with the stepwise refinement method of B.", } @TechReport{DSSE-TR-99-2, author = "Butler, Michael J.", title = "{CSP2B}: {A} Practical Approach To Combining {CSP} and {B}", institution = "Declarative Systems \& Software Engineering Group, Department of Electronics and Computer Science, University of Southampton", year = "1999", URL = "http://www.dsse.ecs.soton.ac.uk/techreports/99-2.html", month = feb, abstract = "This paper describes the tool {CSP2B} which provides a means of combining {CSP}-like descriptions with standard {B} specifications. The notation of CSP provides a convenient way of describing the order in which the operations of a {B} machine may occur. The function of the tool is to convert {CSP}-like specifications into standard machine-readable B specifications which means that they may be animated and appropriate proof obligations may be generated. Use of {CSP2B} means that abstract specifications and refinements may be specified purely using {CSP} or using a combination of {CSP} and B. The translation is justified in terms of an operational semantics.", } @TechReport{Diller93b, author = "Diller, Antoni and Docherty, Rosemary", title = "A Comparison of {Z} and {A}bstract {M}achine {N}otation", institution = "University of Birmingham, School of Computer Science", number = "CSR-93-9", month = aug, year = "1993", abstract = "In this paper we compare the formal specification languages Z and Abstract Machine Notation (AMN); the later of which is due to Abrail. The strategy adopted is that of presenting the same specification both in Z and AMN and of commenting on salient differences as they arise. The specification chosen is a slightly revised version of the specification of an Internal Telephone Number Database found in Diller (1990), pp.35-55. the end of the paper some general conclusions are drawn.", } @TechReport{Docherty93, author = "Docherty, Rosemary and Diller, Antoni", title = "{CAVIAR} in {AMN}", institution = "University of Birmingham, School of Computer Science", number = "CSR-93-3", month = may, year = "1992", abstract = "This specification illustrates many aspects of Z - the interleaving of mathematical text with informal prose, and the facilities to parameterise specifications and to build descriptions of large systems from smaller ones.", } @Unpublished{EJC2000-JRA1, author = "Abrial, Jean-Raymond", title = "{B} : 2000 et plus", note = "{\'E}cole Jeunes chercheurs en programmation", address = "{\'E}cole Normale Sup{\'e}rieure de Lyon -- 46, All{\'e}e d'Italie 69364 LYON Cedex 07", key = "EJC2000-JRA1", month = mar, year = "2000", URL = "http://www-sop.inria.fr/EJC2000/programme.html", } @Unpublished{EJC2000-JRA2, author = "Abrial, Jean-Raymond", title = "Bridge", note = "{\'E}cole Jeunes chercheurs en programmation", address = "{\'E}cole Normale Sup{\'e}rieure de Lyon - 46, All{\'e}e d'Italie 69364 LYON Cedex 07", key = "EJC2000-JRA2", month = mar, year = "2000", URL = "http://www-sop.inria.fr/EJC2000/programme.html", } @Unpublished{EJC2000-JRA3, author = "Abrial, Jean-Raymond", title = "Event Driven Sequential Program construction", note = "{\'E}cole Jeunes chercheurs en programmation", address = "{\'E}cole Normale Sup{\'e}rieure de Lyon -- 46, All{\'e}e d'Italie 69364 LYON Cedex 07", key = "EJC2000-JRA3", keywords = "event-B", month = mar, year = "2000", URL = "http://www-sop.inria.fr/EJC2000/programme.html", } @InProceedings{Moulding95a, title = "{\'E}valuation of the {B} technology for formal requirements expression", author = "Moulding, M. R. and Newton, A. R. and Rushton, T. G. A.", volume = "1", year = "1995", pages = "21--9", booktitle = "{P}roceedings of the 4th {S}oftware {Q}uality {C}onference", abstract = "{T}he {B} technology is a novel mathematically-formal approach to the development of software, which has been devised primarily to address the stages from software design specification to executable program. {I}t comprises a formal specification language, called abstract machine notation ({AMN}), a {B} method and a {B} toolkit. {AMN} allows a large specification to be structured as a number of component specifications, and supports the progressive refinement of these components down to executable code. {T}he {B} method provides guidance on the use of {AMN} for a software development, and the {B} toolkit provides advanced facilities to support a formal {AMN} development, including specification construction, animation, proof and code generation. {T}his paper reports on a case study which has been undertaken as part of a {DTI}-funded project to evaluate the broader applicability of the {B} technology. {T}he case study is concerned with the use of {AMN} with the {CORE} requirements modelling method for a short term conflict alert ({STCA}) air traffic control function. {T}he paper provides a brief introduction to the {B} technology and the {STCA} {CORE} experiment, before discussing the overall results of the case study. {G}enerally, the {B} technology is considered to offer potential advantages over existing formal specification technologies, but enhancements are required to improve its effectiveness for the analysis and design stages of complex information systems; notably, in the handling of highly structured data. (5 {R}efs)", keywords = "B technology evaluation, formal requirements expression, mathematically-formal approach, software development, software design specification, executable program, formal specification language, AMN, B-Method, B-Toolkit, large specification, component specifications, specification construction, specification animation, specification proof, code generation, CORE requirements modelling method, short term conflict alert air traffic control function, complex information systems, highly structured data handling", } @TechReport{ESTAS-RT1999-25, author = "Mariano, Georges and Boulanger, Jean-Louis", title = "Mod{\'e}lisation formelle de circuits num{\'e}riques par la m{\'e}thode {B}", institution = "INRETS-ESTAS", year = "1999", URL = "http://www3.inrets.fr/Public/ESTAS/Mariano.Georges/1999-25-RT.ps.gz", number = "1999-25", address = "INRETS-ESTAS, 20 rue Elisee Reclus,59650 Villeneuve d'Ascq", month = dec, } @InBook{FACIT-Frappier, author = "Diab, Hassan and Frappier, Marc", editor = "Frappier, Marc and Habrias, Henri", book = "Software Specification Methods. An Overview Using a Case Study", title = "{B}: {A} Model-Based Method Using Generalised Substitutions", publisher = "Springer-Verlag", year = "2002", number = "ISBN: 1-85233-353-7", series = FACIT, } @InProceedings{FEM98-Waeselynck, author = "Waeselynck, H{\'e}l{\`e}ne and Behnia, Salimeh", title = "{B} model animation for external verification", booktitle = "Second International Conference on Formal Engineering Methods", pages = "36--45", year = "1998", editor = "Staples, J. and Hinchey, M. and Liu, S.", month = dec, publisher = "IEEE Computer Society Press", } @InProceedings{FM99-Behnia, author = "Behnia, Salimeh and Waeselynck, H{\'e}l{\`e}ne", title = "Test Criteria Definition for {B} Models", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", crossref = "FM99-I", keywords = "testing", pages = "509--529", } @InProceedings{FM99-Buchi, author = "B{\"u}chi, Martin and Back, Ralph", title = "Compositional Symmetric Sharing in {B}", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", crossref = "FM99-I", URL = "http://www.abo.fi/~mbuechi/publications/BSharing.html", pages = "431--451", abstract = "Sharing between {B} constructs is limited, both on the specification and the implementation level. The limitations stem from the single writer/multiple readers paradigm, restricted visibility of shared variables, and structural constraints to prevent interference. As a consequence, applications with inherent sharing requirements have to either be described as large monolithic constructs or be underspecified, leading to a loss of modularity respectively certain desirable properties being unprovable. We propose a new compositional symmetric shared access mechanism based on roles describing rely/guarantee conditions. The mechanism provides for multiple writers on shared constructs,...", } @InProceedings{FM99-Butler, author = "Butler, Michael J.", title = "{CSP2B} : {A} Practical Approach to Combining {CSP} and {B}", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", crossref = "FM99-I", URL = "http://www.dsse.ecs.soton.ac.uk/techreports/99-2.html", key = "490--508", } @InProceedings{FM99-Dunne, author = "Dunne, Steve", title = "The Safe Machine : {A} New Specification Construct for {B}", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", crossref = "FM99-I", pages = "472--489", } @Proceedings{FM99-I, title = "Proceedings of {FM}'99: World Congress on Formal Methods", year = "1999", editor = "Wing, Jeannette M. and Woodcock, Jim and Davies, Jim", number = "1709", series = LNCS, month = sep, publisher = "Springer-Verlag", } @Proceedings{FM99-II, title = "Proceedings of {FM}'99: World Congress on Formal Methods", year = "1999", editor = "Wing, Jeannette M. and Woodcock, Jim and Davies, Jim", number = "1708", series = LNCS, month = sep, publisher = "Springer-Verlag", } @InProceedings{FM99-MATRA, author = "Behm, Patrick and Benoit, Paul and Faivre, Alain and Meynadier, Jean-Marc", title = "{METEOR} : {A} successful application of {B} in a large project", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", pages = "369--387", keywords = "railway", crossref = "FM99-I", } @InProceedings{FM99-Matthews, author = "Matthews, Brian and Locuratolo, Elvira", title = "Formal Development of Databases in {ASSO} and {B}", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", crossref = "FM99-I", pages = "388--410", } @InProceedings{FM99-Meyer, author = "Meyer, Eric and Souqui{\`e}res, Jeanine", title = "Systematic Approach to Transform {OMT} Diagrams to a {B} Specification", booktitle = "FM'99 -- Formal Methods", keywords = "UML, OMT, UML2B", crossref = "FM99-I", pages = "875--895", } @InProceedings{FM99-Munoz, author = "Mun{\~o}z, C{\'e}sar and Rushby, John", title = "Structural embeddings : Mechanization with Method", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", crossref = "FM99-I", pages = "452--471", } @InProceedings{FM99-Rouzaud, author = "Rouzaud, Yann", title = "Interpreting the {B}-Method in the refinement calculus", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", crossref = "FM99-I", pages = "411--430", } @InProceedings{FM99-Sabatier, author = "Sabatier, Denis and Lartigue, Pierre", title = "The use of the {B} formal method for the design and the validation of the transaction mechanism for smart card applications", booktitle = "Proceedings of FM'99: World Congress on Formal Methods", crossref = "FM99-I", pages = "348--368", abstract = "This document describes an industrial application of the {B} method in smart card applications. In smart card memory, data modification may be interrupted due to a card withdrawal or a power loss. The EEPROM memory may result in an unstable state and the values subsequently read may be erroneous. The transaction mechanism provides a secure means for modifying data located in the EEPROM. As the security in smart card applications is paramount, the use of the {B} formal method brings high confidence and provides mathematical proof that the design of the transaction mechanism fulfills the security requirements.", } @InProceedings{FME03-Butler, author = "Leuschel, Michael and Butler, Michael J.", title = "{ProB}: {A} Model Checker for {B}", booktitle = "Proceedings of Formal Methods Europe 2003", pages = "855--874", month = sep, year = "2003", URL = "http://eprints.ecs.soton.ac.uk/8341/", editor = "Keijiro, Araki and Gnesi, Stefania and Dino, Mandrio", address = "Pisa, Italy", keywords = "model-checking, animation, logic programming, constraints, ProB, tools", abstract = "We present {ProB}, an animation and model checking tool for the {B} method. {ProB}'s animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the B-Toolkit, the user does not have to guess the right values for the operation arguments or choice variables. {ProB} contains a model checker and a constraint-based checker, both of which can be used to detect various errors in {B} specifications. We present our first experiences in using {ProB} on several case studies, highlighting that {ProB} enables users to uncover errors that are not easily discovered by existing tools.", } %%% XXX:stopped here @InProceedings{FME2001-Bellegarde, author = "Bellegarde, Fran{\c{c}}oise and Darlot, C. and Julliand, Jacques and Kouchnarenko, O.", title = "Reformulation: a way to combine dynamic properties and {B} refinement Conf{\'e}rence", booktitle = "International Symposium Formal Methods Europe 2001, FME 2001", pages = "2--19", year = "2001", volume = "2021", series = LNCS, month = mar, } @Misc{FME96-Lano, key = "FME-Lano96", author = "Lano, Kevin", title = "Formal Development in {B} {A}bstract {M}achine {N}otation : {FME'96 Tutorial}", year = "1996", } @InProceedings{FMP97, author = "Robinson, K. A.", title = "Specification and implementation of a random access data type: {A} case study using the {B}-Method", booktitle = "Formal Methods Pacific 97", year = "1997", pages = "313--314", address = "Wellington New Zealand", month = jul, URL = "http://www.mcs.vuw.ac.nz/comp/FMP97/papers-list#Work", abstract = "In this tutorial the specification, design and implementation of a random access data type is explored. The development is carried out within the discipline of the {B} Method and using the {B} Toolkit, and the paper is a tutorial on the use of the {B} Method's abstract machine notation for the specification and design of abtract datatypes. The treatment presented here is intended to be the first part of a unified treatment of data types, in which the basic functionality of the data types is emphasized. This constrasts with the treatment given in conventional intermediate data structure treatments in which data types are differentiated on the basis of implementation specific functionality.", } @InProceedings{FORMS04-Marcano, author = "Marcano-Kamenoff, Rafael and Mariano, Georges and Bon, Philippe", title = "{UML}-based design and formal analysis of railway traffic control systems", pages = "173--182", keywords = "B-Method, UML, UML2B", crossref = "FORMS04", } @InProceedings{FORMS04-Boulanger, author = "Boulanger, Jean-Louis and Bon, Philippe", title = "{BRAIL} Requirement analysis", keywords = "B-Method, UML, UML2B", crossref = "FORMS04", pages = "221--229", } @Proceedings{FORMS04, title = "Formal Methods and Automation and Safety in Railway and Automotive Systems", year = "2004", booktitle = "FORMS'2004 / FORMAT'2004", editor = "Schnieder, E. and Tarnai, G.", address = "Braunschweig, Germany", month = dec, } @InProceedings{FORMS2003-Petit, author = "Petit, Dorian and Mariano, Georges and Poirriez, Vincent and Boulanger, Jean-Louis", title = "Automatic {A}nnotated {C}ode {G}eneration from {B} {F}ormal {S}pecifications", booktitle = "Symposium on {F}ormal {M}ethods for {R}ailway {O}peration and {C}ontrol {S}ystems", year = "2003", keywords = "code generation, modularity, BRILLANT", editor = "Tarnai, G. and Schnieder, E.", series = "IEEE", abstract = "In this paper, we present a new approach to generating different codes from specifications developped with the {B} method. This code generator is based on the flattening algorithm and the use of a rewriting tool (an XSLT processor, for example). Currently, the commercial code generation processors are black box tools, and it is very difficult to modify them. We will show that our approach simplifies code generation specification, which makes the specification of new code generators for new target languages easier and faster. Another benefit of our approach is that it allows assertions to be added to the code generated. Assertions, are expressed in the specifications but they are forgot in the current code generation process.", } % Additional information: October 19-23 @InProceedings{Faivre99, author = "Faivre, Alain and Benoit, Paul", title = "Safety Critical Software of Meteor Developed with the {B} Formal Method and the Vital Coded Processor", booktitle = "WCRR'99", year = "1999", month = oct, keywords = "railway", organization = "World Congress on Railway Research, Tokyo, Japan", } @InProceedings{GSW93, title = "On the derivation of executable database programs from formal specifications", author = "Gunther, T. and Schewe, K.-D. and Wetzel, I.", organization = "Dept. of Comput. Sci., Hamburg Univ., Germany", booktitle = "FME93: Industrial-Strength Formal Methods. First International Symposium of Formal Methods Europe Proceedings", pages = "351--66", editor = "Woodcock, J. C. P. and Larsen, P. G.", publisher = "Springer-Verlag, Berlin, Germany", year = "1993", month = apr, abstract = "Achieving wide acceptance of formal methods in software development requires a smooth integration with requirements analysis, design and implementation. Especially for database application systems there exist well-known approaches to conceptual modeling as well as a sophisticated implementation technology on the basis of database programming languages. The work described is based on a scenario, where the {B} method is coupled with a conceptual modeling language TDL and a database programming language DBPL. Both these languages can be represented in {B}. The authors concentrate on the problem of characterizing those {B} specifications that are sufficiently refined in order to be transformed into equivalent DBPL programs. This gives rise to some kind of implementability proof obligation. Moreover, it is shown that the transformation itself can be regarded as a term rewriting task based on a representation by term algebras of the languages involved. For this task they exploit order-sorted algebra by using the OBJ system. (14 Refs)", keywords = "database management systems, formal specification, query languages, executable database programs, formal methods, software development, requirements analysis, implementation technology, database programming languages, B-Method, conceptual modeling language, TDL, DBPL, B specifications, implementability proof obligation, term rewriting task, order-sorted algebra, OBJ", } @TechReport{Gue95, author = "Guerlus, M. and Klay, F.", title = "Sp{\'e}cification formelle : exemple issu du projet {FR{\'E}GATE}.", institution = "CNET", year = "1995", abstract = "Postscript available at: http://estas1.inrets.fr:8001/ESTAS/BUG/Publis", } @InProceedings{HASE00-Requet, author = "Requet, Antoine and Casset, Ludovic and Grimaud, Gilles", title = "Application of the {B} Formal Method to the Proof of a Type Verification Algorithm", booktitle = "HASE 2000", keywords = "formal methods, B-Method, FACADE, smartcards", year = "2000", address = "Albuquerque (NM)", source = "GEMPLUS", month = nov, keywords = "smartcards, JavaCard", URL = "http://www.gemplus.com/smart/rd/publications/", abstract = "Smart cards are credit-card sized devices embedding a microprocessor. They are typically used to provide security to an information system. Open cards are smart cards able to download code after their issuance. The card security is usually ensured by a third part that sends a cryptographic certificate with the code to authenticate it. On card code verification could be a solution for improving card deployment flexibility. However, due to the small amount of resources, the verification process is generally done off card, and checking downloaded code on card is a real challenge. The FA{\c{c}}ADE architecture proposes to split the verification process in two parts and to embed a verifier on card. The type inference, the most expensive part, is performed off card, and a part of the result is sent with the code to the card. The card performs a linear type inference and uses the result to verify that the loaded code is well typed. This article proposes to model the second part of the FA{\c{c}}ADE verification process and to prove the correctness of the algorithm. As the precomputation used for the verification cannot be trusted, it is necessary to ensure that the verification algorithm will never accept an ill-typed program, even if the precomputation has been modified. We present the approach chosen to prove that if the program is accepted, then it is correct versus the FA{\c{c}}ADE semantics. We use the {B} method to abstract the algorithm and to prove it.", } @InProceedings{HL94a, author = "Haughton, Howard and Lano, Kevin", title = "Testing and Safety Analysis of {B} {AMN} Specifications", keywords = "testing", booktitle = "Refinement Workshop", month = jan, year = "1994", } @Book{Habrias2001, author = "Habrias, Henri", title = "Sp{\'e}cification formelle avec {B}", publisher = "Lavoisier-Herm{\`e}s", year = "2001", URL = "http://www.iut-nantes.univ-nantes.fr/{\~{}}habrias/SitWebLivreBr/index.html", } @Book{Haughton96, author = "Haughton, Howard", title = "Specification in {B}: An Introduction Using the {B} Toolkit", publisher = "World Scientific Publishing", year = "1996", ISBN = "1-86094-018-8", key = "Haughton96", } @InBook{Hoa95, author = "Hoare, J. P.", title = "Application of the {B}-Method to {CICS}", publisher = "Prentice Hall International", year = "1995", booktitle = "Applications of Formal Methods", editor = "Bowen, J. P. and Hinchey, M.", chapter = "6", keywords = "CICS, Z, B-Method", } @InProceedings{Hoare96, title = "Applying the {B} technologies to {CICS}", author = "Hoare, J. and Dick, J. and Neilson, D. and Sorensen, I.", booktitle = "{FME} '96: {I}ndustrial {B}enefit and {A}dvances in {F}ormal {M}ethods. {T}hird {I}nternational {S}ymposium of {F}ormal {M}ethods {E}urope. {P}roceedings", pages = "74--84", year = "1996", ISBN = "3-540-60973-3", abstract = "{T}his paper reports on the experiences of {IBM} {H}ursley in using the {Z} notation and the {B}-{M}ethod ({A}brial, 1993; 1995) in developing a new function for {IBM}'s {CICS} product. {A} major constraint on the project was the need to produce code that not only corresponded to its required function, but also met a number of stringent non-functional requirements in areas such as integration, performance and maintenance. {T}he {Z} notation was used to capture the required function, and the resulting specification was hand-translated into {AMN}. {T}he {B}-{T}oolkit, with project-specific extensions, was then used for the development down to {PL}/{X} code. {T}he success of this endeavour is discussed. {T}he use of {Z} and the {B}-{M}ethod were very successful in addressing the new functional requirements. {M}eeting the non-functional requirements, however, was more difficult. (13 {R}efs)", keywords = "CICS, IBM hursley, Z, B-Method, IBM, nonfunctional requirements, integration, performance, maintenance, specification, B-Toolkit, PL/X code, functional requirements, algebraic specification, AMN", } @InProceedings{IDPT2003-Petit, author = "Petit, Dorian and Poirriez, Vincent and Mariano, Georges", title = "The {B} method and the component-based approach", booktitle = "Formal {R}easoning on {S}oftware {C}omponents and {C}omponent {B}ased {S}oftware {A}rchitectures", year = "2003", note = "Special topic session of the Seventh Conference on Integrated Design and Process Technology.", keywords = "code generation, modularity, BRILLANT", abstract = "The aim of this paper is to merge two approaches of software development. The first one is the component approach. Developping software components is now a technique widely used by the software industry. The second approach is the formal one. These approaches are not so distant if we consider Bertrand Meyer's opinion: a component without contracts can not be reused (more exactly, he said that it was more complicated to reuse such a component). One of the difficulties with the design by contract approach is to find the contracts. In some formal approach -we will use the {B} method in this paper- the software properties (the contracts) are expressed in the specifications. We present in this paper an approach to generate code in the spirit of the component approach from {B} specifications.", } @InProceedings{IFM2000-Bert, author = "Bert, Didier and Cave, F.", title = "Construction of Finite Labelled Transition Systems from {B} Abstract Systems", booktitle = "Proc. of the Second International Conference Integrated Formal Methods, IFM'2000", pages = "235--254", year = "2000", number = "1945", series = LNCS, address = "Dagstuhl Castle", month = nov, note = "Springer-Verlag", keywords = "B abstract systems, case study", abstract = "Cet article pr{\'e}sente une {\'e}tude pour repr{\'e}senter le comportement de syst{\`e}mes abstraits {B} par des syst{\`e}mes de transitions {\'e}tiquet{\'e}es (STE). Nous choisissons de d{\'e}composer l'{\'e}tat d'un syst{\`e}me abstrait en plusieurs pr{\'e}dicats disjonctifs. Ces pr{\'e}dicats forment la base pour d{\'e}finir un ensemble d'{\'e}tats qui sont les noeuds du STE, tandis que les {\'e}v{\'e}nements forment les transitions. Nous illustrons la m{\'e}thode en d{\'e}veloppant le syst{\`e}me SCSI-2 d'entr{\'e}e-sortie (Small Computer Systems Interface). Les conclusions portent sur la faisabilit{\'e} de l'approche et sur les retomb{\'e}es possibles de cette repr{\'e}sentation en terme d'analyse de propri{\'e}t{\'e}s.", } @InProceedings{IFM2000-Julliand, author = "Julliand, Jacques and Masson, P-A. and Mountassir, H.", title = "Modular verification for a class of {PLTL} properties", booktitle = "International Workshop on Integrated Formal Methods, IFM'2000", key = "IFM2000-Julliand", pages = "398--419", year = "2000", volume = "1945", series = LNCS, address = "Dagstuhl, Saarland, Germany", month = nov, } @InProceedings{IFM2000-Meyer, author = "Meyer, {\'E}ric and Santen, Thomas", title = "Behavioural Conformance Verification in an Integrated Approach Using {UML} and {B}", booktitle = "Proc. of the Second International Conference Integrated Formal Methods, IFM'2000", year = "2000", number = "1945", series = LNCS, address = "Dagstuhl Castle", month = nov, keywords = "UML", note = "Springer-Verlag", } @InProceedings{JFLA2002-Petit, author = "Petit, Dorian and Mariano, Georges and Poirriez, Vincent", title = "Vers un syst\`eme de module \`a la {H}arper-{L}illibridge-{L}eroy pour les sp\'ecifications formelles {B}", booktitle = "JFLA : Journ\'ees Francophones des Langages Applicatifs", year = "2002", month = jan, note = "85--100", ps = "http://jfla.inria.fr/2002/actes/07-petit.ps", URL = "http://www.univ-valenciennes.fr/ROI/dpetit/Biblio/", abstract = "Nous nous proposons ici de r{\'e}utiliser un calcul des modules {\`a} la SML et de l'appliquer au calcul des modules du langage support de la m{\'e}thode {B}. En cherchant {\`a} exprimer la modularit{\'e} de {B} dans un calcul des modules {<<}{\`a} la Harper-Lillibridge-Leroy{>>} nous cherchons {\`a} obtenir une mod{\'e}lisation claire de celle-ci et \textsl{simultan{\'e}ment} un outillage. Cette {\'e}tude {\'e}tant exp{\'e}rimentale, nous nous limiterons {\`a} une partie du langage {B} : les composant dits {<<}d'impl{\'e}mentation{>>}.", } @InProceedings{LH94a, author = "Lano, Kevin and Haughton, H.", title = "Improving the Process of System Specification and Development in {B} {AMN}", booktitle = "Refinement Workshop", month = jan, year = "1994", } @InProceedings{LM02000-Marcano, author = "Marcano-Kamenoff, Rafael and Losavio, F.", title = "Sp{\'e}cification formelle de patterns d'architectures distribu{\'e}es en {UML} et {B}", booktitle = "LMO'2000, Langages et mod{\`e}les {\`a} objets", year = "2000", address = "Mont St Hilaire, Qu{\'e}bec", month = jan, URL = "http://www.prism.uvsq.fr/~nlevy/www/LMO2000.ps", publisher = "Herm{\`e}s Science Publications", keywords = "UML, UML2B, patterns, distributed architectures", } @InCollection{LS90, title = "Applying {VDM} to large developments", author = "Ledru, Y. and Schobbens, P. Y.", organization = "Unite d'Inf. Univ. Catholique de Louvain,Louvain-La-Neuve, Belgium", publisher = "SIGSOFT Software Engineering Notes", volume = "15-4", pages = "55--8", month = sep, year = "1990", booktitle = "International Workshop on Formal Methods in Software Development", abstract = "The paper focuses on the use of {VDM}. {Meta-IV}, the specification language of {VDM}, was proved successful to specify large systems. Although many specifications have been written in Meta-IV, only a few complete {VDM} developments have been achieved. Experiments with {VDM} and the {B} theorem prover have provided some insight on this problem. The author gives an overview of {VDM}; he points out several weaknesses of the approach in the perspective of large scale developments; and discusses the benefits of the use of the {B} tool. (19 Refs)", keywords = "formal specification, software engineering, VDM, large developments, Meta-IV, specification language, B theorem prover", } % Additional information: 21-25 Oct. @InProceedings{LS91, title = "{B}-Tool (formal specification)", author = "Lee, M. and Sorensen, I. H.", booktitle = "{VDM}91. Formal Software Development Methods. 4th International Symposium of {VDM} Europe Proceedings.", volume = "1", pages = "695--6", editor = "Prehn, S. and Toetenel, W. J.", publisher = "Springer-Verlag, Berlin, Germany", month = oct, year = "1991", abstract = "{B}-Tool provides the platform for solving the problem of specification and correct construction of software systems. It is a flexible inference engine which forms the basis of a computer-aided system for the formal construction of provably correct software. When used as a theorem proving assistant, {B}-Tool gives the software engineer the ability to verify the logical correctness of programs. (1 Refs)", keywords = "formal specification, inference mechanisms, program verification, theorem proving, specification, correct construction, software systems, flexible inference engine, computer-aided system, formal construction, provably correct software, theorem proving assistant, logical correctness of programs", } % Additional information: 9-11 Jan. @InProceedings{LSS91b, title = "Engineering real software using formal methods", author = "Lee, M. K. O. and Scharbach, P. N. and Sorensen, I. H.", booktitle = "4th Refinement Workshop. Proceedings of the 4th Refinement Workshop", pages = "6--33", editor = "Morris, J. M. and Shaw, R. C.", publisher = "Springer-Verlag, Berlin, Germany", year = "1991", month = jan, abstract = "{B} is a formal method for the incremental development of specifications are their refinements. A prototype set of software tools supporting the method has been developed. The tools support the method in the development of verifiably correct software over the spectrum of activities from early specification to coding. The platform of the toolkit is the {B} tool, an interactive proof assistant. The process followed using the method and tools is illustrated in the development of a document management system. The authors present some early indications of the productivity of the method. They intend to establish the practicality of fully applying formal techniques at all stages of software development. (7 Refs)", keywords = "document handling, formal specification, formal verification, software tools, real software engineering, refinement, formal methods, B-Method, incremental development, specifications, software tools, verifiably correct software, interactive proof assistant, document management system, software development", } @TechReport{LaFi96, author = "Lano, Kevin and Fiadeiro, J. and Dick, Jeremy", title = "Extending {B AMN} with concurrency", institution = "Dept. of Computing, Imperial College", URL = "ftp://theory.doc.ic.ac.uk/theory/papers/Lano/tfm_b.dvi", year = "1996", } @Book{LaHa96, title = "Specification in {B}: An Introduction Using the {B} Toolkit", author = "Lano, Kevin and Haughton, Howard", publisher = "Imperial College Press, London", pages = "248", ISBN = "1-86094-018-8", year = "1996", } @InProceedings{Lafontaine90, author = "Lafontaine, Christine and Ledru, Yves and Schobbens, Pierre-Yves", title = "An experiment in formal software development : using the {B} theorem prover on a {VDM} case study", booktitle = "ICSE'90 : Proceeding of th 12th international conference in Software engineering", pages = "34--42", year = "1990", editor = "IEEE Computer Society Press", address = "Los Alamitos, CA, USA", } @Article{Lafontaine91, author = "Lafontaine, Christine and Ledru, Yves and Schobbens, Pierre-Yves", title = "An experiment in formal software development : using the {B} theorem prover on a {VDM} case study", journal = "Communications of the {ACM}", year = "1991", volume = "34", number = "5", month = may, pages = "62--71", } @InBook{Laleau-2000, author = "Facon, Philippe and Laleau, R{\'e}gine and Nguyen, Hong Phuong", editor = "Frappier, Marc and Habrias, Henri", title = "From {OMT} Diagrams to {B} Specifications", book = "Software Specification Methods : an Overview Using a Case Study", publisher = "Springer, FACIT series", year = "2000", } @TechReport{Laleau00, author = "Laleau, Regine and Mammar, Amel", title = "Using a Formal Refinement to Derive Relational Database Implementations from {B} Specifications", institution = "{CNAM}-CEDRIC", year = "2000", abstract = "In this paper, an approach for refining {B} abstract specifications describing data-intensive applications into relational database implementations is presented. Using the refinement process of the {B} method, a set of generic refinement rules are described that take into account both data and operations. The last step consists of mapping the final refined component into a relational database implementation. The different rules have been checked with the AtelierB prover. The aim of the work is to automate the refinement steps. This is possible thanks to the genericity feature of the rules. The approach is illustrated through a running example.", month = feb, } @InProceedings{Laleau2001, author = "Laleau, R{\'e}gine and Polack, Fiona", title = "A Rigorous Metamodel for {UML} Static Conceptual Modelling of Information Systems", booktitle = "Advanced Information Systems Engineering", editor = "Dittrich, K. R. and Geppert, A. and Norrie, M. C.", volume = "2068", number = "2068", series = LNCS, year = "2001", publisher = "Springer-Verlag", address = "Interlaken, Switzerland", month = jun, pages = "402--416", keywords = "UML, static modelling", URL = "http://link.springer.de/link/service/series/0558/tocs/t2068.html", } @InProceedings{Lanet98, author = "Lanet, Jean-Louis and Lartigue, Pierre", title = "The Use of Formal Methods for SmartCards, a Comparison between {B} and {SDL} to Model the {T=1} Protocol", booktitle = "Proceedings of International Workshop on Comparing Systems Specification Techniques", year = "1998", address = "Nantes", month = mar, source = "GEMPLUS", abstract = "In order to obtain high confidence in the software embedded into a smart card, we evaluated different techniques like model checking and theorem proving. Nevertheless due to the low cost of smart cards and mechanical constraints, the amount of memory available on chips is small. The code generated by the tools must be compact enough to fit the constraints. In this paper we compare different code generators with a case study of a protocol dedicated to smart cards. We show that under some conditions, the model checking tools are able to generate code with an acceptable overhead for smart cards. Our work on the {B} method is in progress. The invariants are more difficult to express and to prove but we pointed out some ambiguities and errors contained in the standard.", keywords = "T=1 protocol, optimisation, formal specification, B-Method, SDL", URL = "http://www.gemplus.fr/smart/rd/publications", } @InProceedings{Lanet98b, author = "Lanet, Jean-Louis and Requet, Antoine", title = "Formal Proof of Smart Card Applets Correctness", booktitle = "Proceedings of the Third Smart Card Research and Advanced Application Conference (CARDIS'98)", pages = "85--97", source = "GEMPLUS", year = "1998", URL = "http://www.gemplus.fr/smart/rd/publications/", address = "Louvain-la-Neuve, (be)", month = sep, keywords = "smartcards, JavaCard", abstract = "The new Gemplus smart card is based on the Java technology, embedding a virtual machine. The security policy uses mechanisms that are based on Java properties. This language provides segregation between applets. But due to the smart card constraints a byte code verifier can not be embedded. Moreover, in order to maximise the number of applets the byte code must be optimised. The security properties must be guaranteed despite of these optimisations. For this purpose, we propose an original manner to prove the equivalence between the interpreter of the JVM and our Java Card interpreter. It is based on the refinement and proof process of the {B} formal method.", } @Article{Lano95, title = "Formal development in {B} {A}bstract {M}achine {N}otation", author = "Lano, K. and Haughton, H.", journal = "Information and Software Technology", volume = "37", number = "5-6", pages = "303--316", month = may # "--" # jun, year = "1995", abstract = "{T}he paper gives a comprehensive introduction to the {B} {A}bstract {M}achine {N}otation ({AMN}), a formal method which is based on {Z} and which is supported by an industrial quality toolset. {T}he paper describes development techniques for {AMN}, including the formalization of requirements, specification construction, design and implementation. {R}esults from a large scale safety critical development using the method are also given. (17 {R}efs)", keywords = "formal development, B-Method, AMN, formal method, Z, industrial quality toolset, development techniques, specification construction, large scale safety critical development, industrial application", } @Book{Lano96, author = "Lano, Kevin", title = "The {B} Language and Method: {A} guide to Practical Formal Development", publisher = "Springer-Verlag London Ltd.", year = "1996", ISBN = "3-540-76033-4", abstract = "{B} is a formal approach to software specification and development based on the {Z} specification language. It has been successfully applied in industry, and has robust, commerciallly available tool support for the entire development lifecycle, from specification through to code generation. {``}The {B} language and method{''} provides a comprehensive introduction to the {B} abstract machine notation, and how it can be used to support formal specification and development of high integrity systems. Beginning with a discussion of the history of {B}, it builds up a description of the notation from the basic mathematical notation for sets and sequences, through to the structuring mechanisms of the language, and how it supports {``}programming in the large{''}. Particular emphasis is placed on the use of {B} in the context of existing software development methods, including object-oriented analysis and design. Specifically designed to support the teaching of {B} at undergraduate and postgraduate level, the text includes a large number of worked examples and graduated exercises in {B} {AMN} specification. It also includes two extended case studies of the development process, and an appendix of proof techniques suitable for {B}.", } @InProceedings{Lee91, title = "The {B} formal software engineering technology and its technology transfer into industry", author = "Lee, M. K. O.", organization = "Dept. of Inf. Syst., City Polytech. of Hong Kong, Kowloon, Hong Kong", booktitle = "Computer, Communication and Networking Systems: An Integrated Perspective. Proceedings of the International Conference on Information Engineering - ICIE 91", pages = "332--40", volume = "1", editor = "Subramanian, K. R. and Seumahu, E. S.", publisher = "Elsevier, Amsterdam, Netherlands", year = "1991", month = dec, abstract = "The {B} Technology is a software development technology based on formal mathematical notions of set theory and predicate calculus and is used for the development and production of high precision, portable and maintainable software which is verifiably correct with respect to functional specification. The {B} Technology comprises three components, viz, the {B}-method, the {B} Toolkit, and the {B}-Tool. The {B}-method is a software development process based on Dijkstra's guarded command notation, with built-in structuring mechanisms for the construction of large systems. The {B} Toolkit is a fully integrated CASE toolset supporting the {B}-method from formal systems specification through automatic coding to correctness verification. The operating platform of the {B} Toolkit is a flexible symbolic inference engine which also acts as a theorem proving assistant. This paper gives a brief summary of the {B} Technology. (9 Refs)", keywords = "formal specification, inference mechanisms, program verification, software engineering, theorem proving, formal software engineering technology, technology transfer, B technology, mathematical notions, set theory, predicate calculus, maintainable software, functional specification, B-Method, B-Toolkit, structuring mechanisms, CASE toolset, systems specification, automatic coding, correctness verification, flexible symbolic inference engine, theorem proving assistant", } @InProceedings{Levy02a, author = "L{\'e}vy, Nicole and Marcano-Kamenoff, Rafael and Souqui{\`e}res, Jeanine", title = "From requirements to Formal Specification using {UML} and {B}", booktitle = "2nd International Conference in Computer Systems and Technologies CompSysTech2002", address = "Sofia, Bulgaria", keywords = "UML, UML2B", URL = "http://www.prism.uvsq.fr/recherche/themes/sial/arlog/publications/CST2002.pdf", month = jun, year = "2002", } @InProceedings{Marcano00c, author = "Marcano-Kamenoff, Rafael", title = "Formalizing Patterns Applicability: An approach based on {UML} and {B}", booktitle = "Automated Software Engineering (ASE'2000) Doctoral Symposium", address = "Grenoble, France", publisher = "Technical report number PI-1353, IRISA", keywords = "UML, UML2B", URL = "http://www.prism.uvsq.fr/recherche/themes/sial/arlog/publications/ASE'2000.pdf", month = sep, year = "2000", } @InProceedings{Marcano02a, author = "Marcano-Kamenoff, Rafael and L{\'e}vy, Nicole", title = "Using {B} formal specifications for analysis and verification of {UML/OCL} models", booktitle = "Workshop on consistency problems in UML-based software development. 5th International Conference on the Unified Modeling Language", address = "Dresden, Germany", keywords = "UML, OCL, UML2B", URL = "http://www.prism.uvsq.fr/recherche/themes/sial/arlog/publications/UML2002a.pdf", month = sep, year = "2002", } @InProceedings{Marcano02b, author = "Marcano-Kamenoff, Rafael and L{\'e}vy, Nicole", title = "Transformation rules of {OCL} constraints into {B} formal expressions", booktitle = "CSDUML'2002, Workshop on critical systems development with UML. 5th International Conference on the Unified Modeling Language", keywords = "UML, OCL, UML2B", address = "Dresden, Germany", URL = "http://www.prism.uvsq.fr/recherche/themes/sial/arlog/publications/CSDUML'2002.pdf", month = sep, year = "2002", } @PhdThesis{Marcano-PhD, author = "Marcano-Kamenoff, Rafael", title = "Sp{\'e}cification formelle {\`a} objets en {UML/OCL} et {B} : Une approche transformationnelle", school = "Universit{\'e} de Versailles -- PRiSM", year = "2002", keywords = "UML, OCL, UML2B, patterns", month = dec, } @PhdThesis{Mariano-PhD, author = "Mariano, Georges", title = "{\'E}valuation de logiciels critiques d{\'e}velopp{\'e}s par la m{\'e}thode {B} : une approche quantitative", school = "Universit{\'e}e de Valenciennes et du Hainaut-Cambr{\'e}sis", year = "1997", pages = "160", URL = "http://www3.inrets.fr/estas/mariano/MaThese", month = dec, } @InProceedings{Mariano96, author = "Mariano, Georges and El Koursi, El Miloudi", title = "Formal Methods and Metrics: Application to {B} Development Assessment", key = "Mariano96", booktitle = "Proceedings of the 5th Software Quality Conference", year = "1996", editor = "Samson, W. B. and Marshall, I. M. and Edgar-Nevill, D. G.", pages = "37--55", address = "University of Abertay Dundee, Bell Street, Dundee DD1 HG", month = jul, } @PhdThesis{Masson-2001, author = "Masson, Pierre-Alain", title = "{V}{\'e}rification par model-checking modulaire de propri{\'e}t{\'e}s dynamiques {PLTL} exprim{\'e}es dans le cadre de sp{\'e}cifications {B} {\'e}v{\'e}nementielles.", school = "UFR des Sciences et Techniques de Besan{\c{c}}on, Universit{\'e} de Franche-Comt{\'e}", year = "2001", month = dec, keywords = "formal verification, model-checking, event system, temporal logic, Buchi automata, modular verification", abstract = "Le travail pr{\'e}sent{\'e} dans cette th{\`e}se prend pour cadre la sp{\'e}cification de syst{\`e}mes r{\'e}actifs sous forme d'{\'e}v{\'e}nements B. A une sp{\'e}cification B {\'e}v{\'e}nementielle, on int{\`e}gre l'expression de propri{\'e}t{\'e}s dynamiques d{\'e}crites en termes de formules de logique temporelle lin{\'e}aire propositionnelle (PLTL). La v{\'e}rification de ces propri{\'e}t{\'e}s par une technique de preuve n'est pas automatisable, aussi nous proposons d'effectuer leur v{\'e}rification par model- checking. Afin de faire face au probl{\`e}me de l'explosion combinatoire li{\'e} {\`a} l'utilisation du model- checking, nous proposons de d{\'e}couper par partition le graphe d'accessibilit{\'e} issu de la sp{\'e}cification en un ensemble de modules de petite taille, et de mener la v{\'e}rification sur chacun des modules de mani{\`e}re s{\'e}par{\'e}e. Cette m{\'e}thode est appel{\'e}e V{\'e}rification Modulaire. Nous voulons {\^e}tre en mesure, {\`a} partir de la v{\'e}rification s{\'e}par{\'e}e d'une propri{\'e}t{\'e} sur chacun des modules, de d{\'e}cider si la propri{\'e}t{\'e} est v{\'e}rifi{\'e}e globalement. Toutes les propri{\'e}t{\'e}s ne se pr{\^e}tent pas {\`a} une telle v{\'e}rification car certaines d'entre elles peuvent {\^e}tre fausses globalement bien que vraies sur chacun des modules. Nous d{\'e}finissons alors les propri{\'e}t{\'e}s qui se pr{\^e}tent {\`a} une telle v{\'e}rification de la mani{\^e}re suivante (ces propri{\'e}t{\'e}s sont dites modulaires) : une propri{\'e}t{\'e} est modulaire si et seulement si le fait qu'elle est vraie sur chaque module implique qu'elle est vraie globalement. Il faut noter {\'e}galement que tous les d{\'e}coupages n'auront pas la m{\^e}me efficacit{\'e} relativement {\`a} la v{\'e}rification des propri{\'e}t{\'e}s. En effet, la propri{\'e}t{\'e} a besoin d'{\^e}tre vraie sur chaque module pour que nous puissions conclure. Or, un d{\'e}coupage al{\'e}atoire aurait de fortes chances de voir {\'e}chouer la v{\'e}rification d'une propri{\'e}t{\'e} dans un ou plusieurs modules, du fait que certains chemins qui rendent la propri{\'e}t{\'e} vraie pourraient {\^e}tre coup{\'e}s. Le probl{\`e}me est donc de produire un d{\'e}coupage modulaire en accord avec les propri{\'e}t{\'e}s que l'on cherche {\`a} v{\'e}rifier. En r{\'e}sum{\'e}, nous tentons de r{\'e}pondre aux questions suivantes : * Quelles sont les propri{\'e}t{\'e}s v{\'e}rifiables modulairement ? * Comment produire un {<<}bon{>>} d{\'e}coupage modulaire ? En r{\'e}ponse {\`a} la premi{\`e}re question, nous prouvons formellement que les propri{\'e}t{\'e}s PLTL issues des 3 sch{\'e}mas de contraintes dynamiques introduits par J.-R. Abrial et L. Mussat sont v{\'e}rifiables de mani{\`e}re modulaire. Nous prouvons {\'e}galement que tout une classe de propri{\'e}t{\'e}s PLTL, incluant les 3 sch{\'e}mas pr{\'e}cit{\'e}s, est v{\'e}rifiable de mani{\`e}re modulaire. Nous exhibons une condition suffisante de modularit{\'e} d'une propri{\'e}t{\'e}. Cette condition de modularit{\'e} repose sur l'analyse syntaxique de l'automate de B{\"u}chi qui code la n{\'e}gation d'une propri{\'e}t{\'e} PLTL. Elle est donc facilement automatisable. Afin de r{\'e}pondre {\`a} la deuxi{\`e}me question, nous proposons de guider la d{\'e}composition modulaire par le raffinement B, ce qui offre l'avantage de produire un d{\'e}coupage s{\'e}mantique du graphe d'accessibilit{\'e} {\`a} chaque niveau du raffinement. Nous faisons alors la distinction entre les nouvelles propri{\'e}t{\'e}s, introduites {\`a} un niveau donn{\'e} de raffinement, et les anciennes propri{\'e}t{\'e}s, {\'e}tablies aux niveaux pr{\'e}c{\'e}dents de raffinement et conserv{\'e}es par celui-ci. La v{\'e}rification modulaire porte sur les nouvelles propri{\'e}t{\'e}s.", } @Article{Mejia93, author = "Dehbonei, Babak and Mejia, Fernando", journal = "ACM SIGPLAN Notices", month = nov, pages = "16--21", title = "Verification of Proofs for the {B} Formal Development Process", volume = "28", year = "1993", number = "11", abstract = "Formal methods are more frequently used in the realization of industrial safety-critical systems. From the specification through a refinement process, all the steps are mathematically proved, generally with the help of automatic tools such as provers. This papers adresses the problem of the verification of such tools in the framework of the {B} formal development technique. The tools are written in the language called {\em Theory Language} for wich the basic proof mechanism is pattern-matching. We propose a technique, based on a unification mechanism, for verifying programs written in this language. Some figures concerning the experimentation of this technique on real-life programs are given.", } @InBook{Mejia97, author = "Mejia, Fernando", title = "La m{\'e}thode {B}", chapter = "18", pages = "231--246", crossref = "arago20", } @TechReport{Mermet96, author = "Mermet, Bruno", title = "Extension of the {B} Method to the Specification of Distributed Systems", institution = "CRIN-CNRS and INRIA Lorraine", year = "1996", } @PhdThesis{Meyer-PhD, author = "Meyer, Eric", title = "{D}{\'e}veloppement formel par objets : utilisation conjointe de {B} et {UML}", keywords = "UML", school = "Universit{\'e} de Nancy", year = "2001", } @InProceedings{Motre-Teri, author = "Motr{\'e}, St{\'e}phanie and T{\'e}ri, Corinne", title = "Using Formal and Semi-formal Methods for a Common Criteria Evaluation", booktitle = "Eurosmart", year = "2000", source = "GEMPLUS", address = "Marseille (France)", month = jun, keywords = "smartcards, CC certification process, B-Method, UML, SDL", URL = "http://www.gemplus.fr/smart/rd/publications/", abstract = "A smart card is an embedded system that is generally used to supply security to an information system. Traditionally the application and the OS were developed in a secure environment by the card issuer. For a few years, open platforms (e.g., Java Card, MultOS and Smart Card for Windows) have provided new facilities for application developers. They allow dynamic storage and execution of downloaded executable code. Such architecture introduces new risks: it offers the possibility to attack the card from an applet by exploiting some implementation faults. This document provides a practical overview of a Common Criteria (CC) high Evaluation Assurance Level (EAL) of a Java Card. It is not dedicated to smart card specialist as it presents the security stakes of such a technology. We present the motivation for a Java Card evaluation: reach the same security level for the new open smart card than for traditional embedded platforms. We introduce the SDL, {UML} and the {B} method to illustrate the semi-formal and formal models required for a high level evaluation. The {B} method has been already used in GEMPLUS to formal model security parts of the Java Card: bytecode verifier, interpreter and firewall. These case studies reveal the interest to use the {B} method to formalise the Java Card Virtual Machine (JCVM). SDL and {UML} are both semi-formal modelling languages that could be used in a high EAL. This document also proposes a comparison between these two languages based on the analysis of the Java Card security mechanisms specification. In a CC evaluation the use of semi-formal and formal techniques is required to obtain the assurance of a high security level.", } @InProceedings{Motre2000, author = "Motr{\'e}, St{\'e}phanie", title = "A {B} Automaton for Authentication Process", booktitle = "WITS'2000", keywords = "automaton, security policy, authentication, B-Method", year = "2000", address = "Geneva (Switzerland)", month = jul, source = "GEMPLUS", URL = "http://www.gemplus.fr/smart/rd/publications/", abstract = "An authentication procedure can be used in various occasions. Nowadays, you have to show your personal badge to enter your firm building, your car is identified by an electronic tag on its windshield at the parking entrance, your retina is scanned at your desk door, and a finger prints analyzer permits you to access confidential network from your computer. All these procedures are applications that include information collection (tag information obtaining, retina picture construction...), client server information exchanges (Who corresponds to the collected information? Which permissions are granted to the person that has been identified?), and an authentication policy. The security policy describes the constraints that should be enforced by any execution of the authentication procedure. It is represented by a security automaton, which shall be global to any authentication mechanism. F. Schneider [She-99] exposes that a security automaton can be applied to access control, information flow or resources availability processes. In this document, he describes the execution monitoring as a way to supervise an application execution and to detect any illegal action. D. Walker [Wal-00] has given a way to type those automata using formal semantics.", keywords = "authentication", } @InProceedings{NFM96-DT, author = "Draper, Jonathan and Treharne, Helen", title = "The Refinement of Embedded Software with the {B}-Method", booktitle = "Northern Formal Methods Workshops in Computer Science", year = "1996", month = nov, address = "Bradford", series = "Workshops in Computing", publisher = "Springer-Verlag", URL = "http://www.cs.rhbnc.ac.uk/~helent", abstract = "The paper described the use of formal refinement within the MIST project. MIST (Measurable Improvement in Specification Techniques) was ESSI application experiment 10228. It details a specification style developed by the project that models embedded software within a system context.", annote = "Submitted by H. Treharne, 1999-09-01", } % Additional information: 17-18 Dec @InProceedings{Nei91, title = "Machine support on {Z}: the zed{B} tool", author = "Neilson, D.", booktitle = "Z User Workshop, Oxford 1990. Proceedings of the Fifth Annual {Z} User Meeting", pages = "105--28", editor = "Nicholls, J. E.", publisher = "Springer-Verlag, Berlin, Germany", year = "1991", month = dec, abstract = "Many operations on schemas are purely systematic processes; for example, decoration, expansion, evaluation of Delta and Xi schemas, and the calculation of schema composition, hiding, and precondition, up to the application of the so-called one-point rule. Each of these activities may therefore be fully automated. The ITRU (Information Technology Research Unit) at BP Research is engaged in research into formal software development methods has developed {B}: a formal method built on the {B} tool. The author describes an application of the {B} tool which provides a theorem proving environment for the analysis of {Z} specifications, incorporating the full automation of many schema operations. (11 Refs)", keywords = "formal specification, software tools, specification languages, ZedB tool, schemas, schema composition, hiding, precondition, formal software development methods, B tool, theorem proving environment, Z specifications", } @InProceedings{Neilson94, title = "{T}he {B}-{T}echnologies: a system for computer aided programming", author = "Neilson, D. S. and Sorensen, I. H.", pages = "18--35", year = "1994", booktitle = "{P}roceedings 6th {N}ordic {W}orkshop on {P}rogramming {T}heory", abstract = "{T}he paper introduces the {B}-{T}echnologies, a mathematically based formal method and a toolset for computer aided software engineering. {T}he {B}-{T}echnologies (comprising three components-the {B}-{M}ethod, the {B}-{T}ool and the {B}-{T}oolkit) have been designed to scale up formal methods for practical application. {T}he {B}-{M}ethod and the {B}-{T}oolkit are described. {T}he {B}-{M}ethod is designed to provide a notation and a methodology for the formal specification, design, implementation and maintenance of industrial-scale software systems. {T}he features of incremental construction of layered software as well as its incremental verification have been guiding principles in the development of the {B}-{M}ethod. {T}he method uses {A}brial's (1993) {A}bstract {M}achine {N}otation ({AMN}) as the language for specification, design and implementation within the software process. {AMN} is is based on an extension of {D}ijkstra's (1976) guarded command notation, with built-in structuring mechanisms for the construction of large systems. {T}he {B}-{T}oolkit supports the method over the entire spectrum of activities from specification through design and implementation into maintenance. {T}he {B}-{T}oolkit comprises automatic and interactive theorem-proving assistants, a proof printer and a set of software development tools: an {AMN} syntax and type checker, a specification animator and generators promoting an object oriented approach at all stages of development, and the reuse of specification models/software modules. {A}ll tools are integrated with the proof assistants into a window-based development environment. (22 {R}efs)", keywords = "computer-aided programming, B-technologies, mathematically based formal method, toolset, computer-aided software engineering, B-Method, B-tool, B-Toolkit, formal specification, software design, software implementation, software maintenance, industrial-scale software systems, incremental construction, layered software, incremental verification, AMN, guarded command notation, built-in structuring mechanisms, automatic theorem-proving assistants, interactive theorem-proving assistants, proof printer", } @Unpublished{PRA95b, author = "Pratten, C. H.", title = "The {AMN-PROOF} Tool: Proving {AMN} Specifications with the {HOL} Theorem Prover", year = "1995", note = "http://louis.ecs.soton.ac.uk/~chp/papers.html", URL = "http://louis.ecs.soton.ac.uk/~chp/papers.html", month = may, } @PhdThesis{Parreaux-PhD, author = "Parreaux, Beno{\^\i}t", title = "{V}{\'e}rification de syst{\`e}mes d'{\'e}v{\'e}nements {B} par model-checking {PLTL} ; Contribution {\`a} la r{\'e}duction de l'explosion combinatoire en utilisant de la r{\'e}solution de contraintes ensemblistes.", school = "Laboratoire d'Informatique de l'Universit{\'e} de Franche-Comt{\'e} (L.I.F.C.)", year = "2000", } @PhdThesis{Petit-PhD, author = "Petit, Dorian", title = "{G}\'en\'eration automatique de composants logiciels s\^urs {\`a} partir de sp\'ecifications formelles {B}", school = "Universit\'e de Valenciennes et du Hainaut-Cambr\'esis", keywords = "automatic code generation, modularity, HLL, BRILLANT", year = "2003", month = dec, } @TechReport{Plosila-2000, author = "Plosila, Juha and Sere, Kaisa and Wald{\'e}n, Marina", title = "Component-Based Asynchronous Circuit Design in {B}", institution = "Turku Center for Computer Science", year = "1999", number = "377", month = dec, keywords = "hardware, asynchronous circuits, B-Method, action systems, data refinement, circuit design", URL = "http://www.tucs.abo.fi/publications/techreports/TR377.html", abstract = "Action systems offer a component-based approach to circuit design. Component-based approaches are well established in hardware design, but are only recently more established in software design. However, software oriented methods allow a higher level of abstraction than the often quite low-level hardware design methods used today. We propose a method to organise a large circuit derivation within the {B} Method via its library facilities as provided by the tools. The developer proceeds from an abstract high-level specification of the intended behaviour of the target circuit via correctness-preserving transformation steps towards an implementable circuit description. At each step some part of the specification is implemented using a library component chosen by the designer and the correctness of the step is proved using the tool support of the {B} Method. We develop the needed program transformation rules that the designer can appeal to when using library components in his or her design.", } @InCollection{RBH94, title = "{E}xperiences in using the {A}bstract {M}achine {N}otation in a {GKS} case study", author = "Ritchie, B. and Bicarregui, J. and Haughton, H.", booktitle = "FME'94 : Industrial Benefits of Formal Methods", series = LNCS, volume = "873", ISBN = "3-540-58555-9", editor = "Springer-Verlag", year = "1994", pages = "93--104", abstract = "{T}he paper discusses the authors' experiences in reengineering and subsequently refining part of a {Z} style specification of the {G}raphics {K}ernel {S}ystem using the {A}bstract {M}achine {N}otation as supported in the {B} {T}oolkit. (10 {R}efs)", keywords = "AMN, GKS, case study, Z style specification, graphics kernel system, B-Toolkit", } @InProceedings{Requet00, author = "Requet, Antoine", title = "A {B} Model for Ensuring Soundness of the {Java} Card Virtual Machine", booktitle = "FMICS'2000", year = "2000", address = "Berlin", month = mar, keywords = "smartcards, JavaCard, certification process, B-Method, byte code, semantics, virtual machine", source = "GEMPLUS", URL = "http://www.gemplus.fr/smart/rd/publications/", abstract = "Java Cards are a new generation of smart cards that use the Java programming language. As smart cards are usually used to supply security to a system, security requirements are very strong and certification can become a competitive advantage. Such a certification to a high Common Criteria or ITSEC level requires the proof of all the security mechanisms. Those security mechanisms include the byte code interpreter and verifier of the virtual machine. Previous works have been done on methodology for proving the soundness of the byte code interpreter and verifier using the {B} method. It refines an abstract defensive interpreter into a byte code verifier and a byte code interpreter. However, this work had only been tested on a very small subset of the Java Card instruction set. This paper presents a work aiming at verifying the scalability of this previous work. The original instruction subset of about ten instructions has been extended to more than one hundred instructions, and the additional cost of the proof has been managed by modifying the specification in order to group opcodes by properties.", } @InProceedings{Robinson97, author = "Robinson, K. A.", title = "The {B}-Method and the {B}-Toolkit", pages = "576--580", booktitle = "Sixth International Conference, Algebraic Methodology and Software Technology", year = "1997", organization = "Sydney", publisher = "Springer", month = dec, abstract = "The {B} Method is a full spectrum formal software development method that covers the software process from specification to implementation. The method uses state machines, defined using logic and set theory with a notation similar to that of Z, that export operations. The method supports a notion of refinement and implementation, which is based on the notion of refinement in the refinement calculus with the exception that there is no distinction between procedural and data refinement. The {B} Toolkit is a configuration tool that manages developments under the {B} Method, generating proof obligations and supporting tools for the discharge of those proof obligations. There is also support for the generation of documentation, and for the browsing of developments.", } % Additional information: July 18-21 @InProceedings{SCI04-Boulanger, author = "Boulanger, Jean-Louis", title = "{BHDL} - An example", booktitle = "SCI 2004 - The 8th World Multi-Conference on Systemics, Cybernetics and Informatics, Orlando, Florida, USA", pages = "150--155", year = "2004", volume = "IX", keywords = "hardware formal specification, BHDL, codesign", month = jul, organization = "International Institute of Informatics and Systemics", } @InCollection{SH94, title = "{A} strategy for the production of verifiable code using the {B} {M}ethod", author = "Storey, A. C. and Haughton, H. P.", year = "1994", editor = "Springer-Verlag", ISBN = "3-540-58555-9", booktitle = "{FME} '94: {I}ndustrial {B}enefit of {F}ormal {M}ethods. {S}econd {I}nternational {S}ymposium of {F}ormal {M}ethods {E}urope", abstract = "{T}he purpose of this paper is to describe extensions to the {B} {M}ethod in order to facilitate the generation of provably correct {SPARK} {A}da, code. {T}wo strategies are provided. {F}irstly, a process model for the {B} {M}ethod is stated that allows the semi- automatic production of refinements through the use of standard library machines. {S}econdly, transformation rules are given for the automatic generation of {SPARK} {A}da code from these refinement's. {F}inally, an overview is given of how the semantics of {A}bstract {M}achine {N}otation and {SPARK} {A}da can be used in order to verify these transformation rules. (7 {R}efs)", keywords = "verifiable code, B-Method, provably correct SPARK Ada, process model, semi-automatic production, refinement, standard library machines, transformation rules, automatic code generation, SPARK Ada code, AMN", } @InProceedings{SOFSEM95, author = "Bicarregui, J. C. and Matthews, B. M.", title = "Formal Methods in Practice: a comparison of two support systems for proof.", editor = "Bartosek and al.", year = "1995", volume = "1012", URL = "http://theory.doc.ic.ac.uk:80/~jcb1/vdmbpapers.html", series = LNCS, booktitle = "SOFSEM'95: Theory and Practice of Informatics", publisher = "Springer-Verlag", abstract = "http://theory.doc.ic.ac.uk:80/~jcb1/sofsem95.ps", URL = "http://theory.doc.ic.ac.uk:80/~jcb1/sofsem95.ps", } @Book{Schneider2002, author = "Schneider, Steve", title = "The {B-Method}: An Introduction", publisher = "Palgrave", year = "2002", abstract = "This book provides a comprehensive introduction to the B-Method, which is a rigorous methodology for the development of correct software, underpinned by powerful state-of-the-art tool support. It covers the {B} approach to software development from specification through refinement, down to implementation and automatic code generation, with verification at each stage. The book assumes no prior knowledge and is written in a tutorial style, containing numerous illustrative examples, exercises and self-tests with answers. http://www.palgrave.com/science/computing/schneider/", URL = "http://www.palgrave.com/science/computing/schneider/", } @InProceedings{Snook-2002, author = "Snook, Colin", title = "Combining {UML} and {B}", booktitle = "In Proceedings of Forum on Specification \& Design Languages, Marseille", year = "2002", organization = "FDL 2002", abstract = "Formal specification is recognised as a difficult task (Snook \& Harrison, 2001) and the adaptation of semi-formal object oriented modelling tools has been proposed by several authors including Meyer \& Souquieres (1999). Here we give an overview of a prototype tool for converting annotated {UML} (OMG, 2001) class and state diagrams into the B notation. The tool was developed during the {``}MATISSE{''} project in a healthcare case study (Petre, Troubitsyna, and Wald{\'e}n, 2002). In this case study, B-Action systems were used to analyse the safety of a pharmaceutical laboratory instrument in several stages of refinement. B-Action systems (Butler and Wald{\'e}n, 1998, Wald{\'e}n and Sere, 1998) are specifications of distributed systems written in the {B} Method (Abrial, 1996) using a style based on stepwise refinement of event based models. The tool enabled each stage of refinement to be specified in a clear visual ({UML} based) form prior to conversion to {B} for verification. The U2B translator converts Rational Rose (Rational 2000) {UML} Class diagrams and attached state charts, into the {B} notation.", keywords = "UML, B-Method, B2UML, Rational Rose, U2B, action systems", } @InProceedings{Snook-2003, author = "Snook, Colin and Sandstr{\"o}m, Kim", title = "Using {UML-B} and {U2B} for formal refinement of digital components", booktitle = "In Proceedings of Forum on specification \& design languages, Frankfurt", year = "2003", organization = "FDL2003", abstract = "In this paper we look at using formal methods to verify the transformation of a digital design from abstract functional specification to bit level implementation. As both authors are in-experienced in formal proof we saw this as a test of the practicality of introducing proof tools in an industrial setting rather than an exemplar of such methods Rigorous verification is desirable in digital design because mistakes can be extremely costly. However, there are drawbacks and barriers to introducing formal notations. Formal notations are abstraction hungry, viscous and require insight, experience and look-ahead. Hence we specialise the {UML} to alleviate these problems by providing a semi-graphical form of the formal notation {B} based on existing visual modelling tools. With a small case study, we show the use of B-{UML} using an event style of modelling to refine a macro level function into a cascade of single bit cells. We attempt to prove the refinement with the assistance of available proof tools but find that the problem is deceptively difficult", keywords = "UML, B-Method, B2UML, hardware, RTL level", } @InProceedings{Sorensen94, title = "{D}emonstration of the {B}-{T}oolkit", author = "Sorensen, I. H.", year = "1994", booktitle = "{P}roceedings 6th {N}ordic {W}orkshop on {P}rogramming {T}heory", abstract = "{T}he {B}-{T}oolkit is a suite of integrated programs which implement the {B}-{M}ethod for software development. {T}he {B}- {M}ethod is a collection of formal techniques which give a basis to those activities of software development that range from technical software specification, through design and integration, to code generation and into maintenance. {T}he {B}-{M}ethod and the specification language {AMN} ({A}bstract {M}achine {N}otation) are in many respects similar to other {``}model oriented{''} formal methods. {T}hey employ a conventional {``}pseudo{''} programming style. {T}he {B}-{T}ool is a language interpreter for the {B} {T}heory {L}anguage. {T}his language is a special purpose language for writing interactive and automatic proof assistants and other systems where pattern matching, substitution and re-write mechanisms can be used. {T}he {B}-{T}oolkit's component tools are implemented in the {B} {T}heory {L}anguage and is interpreted by the {B}-{T}ool. (0 {R}efs)", keywords = "software tool software development, software package, B-Toolkit, integrated program suite, B-Method, formal technique, software specification, design, integration, code generation, maintenance, AMN, pseudoprogramming, B-tool, language interpreter, B theory language, automatic proof assistant, pattern matching, substitution, rewrite mechanisms", } @Article{Sto92, title = "A Specification Case Study using the {B}-methodology", author = "Storey, A.", journal = "Software Testing, Verification and Reliability", volume = "2", number = "4", pages = "187--202", month = dec, year = "1992", abstract = "The {B}-Method is a complete formal development process for mathematically transforming software systems from specification through to code. This article provides the reader with an overview of the process including a description of the language used for specifying systems (Abstract Machine Notation) and demonstrates its application by a simple, real-life case study. The method has tool support in the form of a tool-kit which is described and applied to the case study. The results of the case study show how a system can be validated and verified in the early stages of its development through proof of the mathematical specification and an animating tool. (12 Refs)", keywords = "formal specification, program testing, program verification, software engineering, software tools, specification languages, computer software verification, specification case study, B-Method, complete formal development process, mathematical transformation, software tool, AMN, mathematical specification, animating tool", } @InProceedings{Stoddart94, title = "Forth as an Abstract Machine", author = "Stoddart, Bill", booktitle = "euroForth '94 Conference Proccedings", month = Nov, year = "1994", address = "MPE Ltd, 133 Hill Lane, Southampton SO1 5AF, UK", organization = "Forth Interest Group", abstract = "This is a work in progress paper on producing a formal equivalent to the Forth ANSI Standard. The chosen notation is AMN (Abstract Machine Notation). The paper gives some comments on the formalisation process and on some features of AMN.", } @Article{Stoddart99, author = "Stoddart, Bill and Dunne, Steve and Galloway, Andy", title = "Undefined Expressions and Logic in {Z} and {B}", journal = "Formal Methods in System Design: An International Journal", year = "1999", volume = "15", number = "3", pages = "201--215", month = nov, } @Article{TSI21-Boite, author = "Boite, Olivier", title = "Automatiser les preuves d'un sous-langage de la m{\'e}thode {B}", journal = TSI, year = "2002", volume = "21", number = "8", keywords = "automatic proof", } @Article{TSI20-Julliand, author = "Julliand, J. and Masson, P.-A. and Mountassir, H.", title = "{V}{\'e}rification par model-checking modulaire des propri{\'e}t{\'e}s dynamiques introduites en {B}", journal = "TSI (Technique et Science Informatiques)", year = "2001", volume = "20", number = "7", pages = "927--957", } @InProceedings{TTV96, author = "Taouil-Traverson, S. and Vignes, S.", title = "A Preliminary Analysis Cycle for {B} development", organization = "EUROMICRO 96, Prague, Czech Republic", booktitle = "Beyong 2000: Hardware and Software Design Strategies", month = sep, pages = "319--325", year = "1996", } @TechReport{TUCS-TR-53, author = "Butler, Michael J. and Wald{\'e}n, M.", title = "Distributed System Development in {B}", institution = "Turku Centre for Computer Science, Finland", year = "1996", URL = "http://www.tucs.abo.fi/publications/techreports/TR53.html", number = "53", month = oct, abstract = "The B-Method is a method for the stepwise derivation of sequential programs. In this paper we show how the B-Method can be used for designing distributed systems by embedding action systems within this method. The action system formalism is designed for the construction of parallel and distributed systems in a stepwise manner within the refinement calculus. We describe how action systems are written in {B} AMN. We also show the correspondence between refinement rules for action systems and the proof obligations generated in the B-Method. Furthermore, we propose an extension of the B-Method to cover parallel and distributed systems. Familiarity with B AMN is assumed.", } @InProceedings{Tatibouet2001, author = "Tatibou{\"e}t, Bruno and Voisinet, J. C.", title = "j{BT}ools and {B2UML}: a platform and a tool to provide a {UML} Class Diagram since {\`a} {B} specification", keywords = "UML, B2UML", booktitle = "ICSSEA'2001 -- 14th Int. Conf. on Software Systems Engineering and Their Applications", year = "2001", volume = "2", address = "{CNAM}, Paris, France", month = dec, } @InProceedings{Tatibouet2003, author = "Tatibou{\"e}t, Bruno and Requet, Antoine and Voisinet, Jean-Christophe and Hammad, Ahmed", title = "Java Card code generation from {B} specifications", booktitle = "ICFEM", pages = "306--318", keywords = "smartcards, JavaCard", year = "2003", editor = "Dong, J. S. and Woodcock, J.", volume = "2885", organization = "Formal Methods and Software Engineering", publisher = "Springer-Verlag", } @PhdThesis{Traverson-PhD, author = "Taouil-Traverson, Sou{\^a}d", title = "Strat{\'e}gie d'int{\'e}ration de la m{\'e}thode {B} dans la construction de logiciel critique", school = "Ecole Nationale Sup{\`e}rieure des T{\'e}l{\'e}communications", year = "1997", pages = "160", } @InProceedings{Traverson97, author = "Traverson, Souad and Vignes, Sylvie", title = "Int{\'e}gration de la m{\'e}thode {B} dans la construction de logiciels critiques", number = "46", series = "G{\'e}nie Logiciel", pages = "100--106", booktitle = "Le G{\'e}nie Logiciel est ses Applications -- 1o eme Journ{\'e}es Internatinales - ACTES", year = "1997", month = dec, } @TechReport{Treharne99a, author = "Treharne, Helen and Schneider, Steve", title = "Using a Process Algebra to control {B} \textbf{OPERATIONS}", institution = "Royal Holloway, Department of Computer Science, University of London", year = "1999", number = "CSD-TR-99-01", address = "Egham, Surrey TW20 0EX, England", URL = "http://www.cs.rhbnc.ac.uk/~helent", month = jun, } @TechReport{Treharne99b, author = "Treharne, Helen and Schneider, Steve", title = "Capturing timing requirements formally in {AMN}", institution = "Royal Holloway, Department of Computer Science, University of London", year = "1999", number = "CSD-TR-99-06", keywords = "time requirements", address = "Egham, Surrey TW20 0EX, England", URL = "http://www.cs.rhbnc.ac.uk/~helent", month = jun, } @InProceedings{Treharne:IFM99, author = "Treharne, Helen and Schneider, Steve", title = "Using a Process Algebra to Control {B} {OPERATIONS}", booktitle = "IFM'99 1st International Conference on Integrated Formal Methods", keywords = "B-Method, CSP, embedded systems, programming calculi, combining formalisms", pages = "437--457", year = "1999", address = "York", month = jun, publisher = "Springer-Verlag", URL = "http://www.cs.rhbnc.ac.uk/~helent", abstract = "The B-Method is a state-based formal method that describes system behaviour in terms of {\bf MACHINES} whose state changes under {\bf OPERATIONS}. The process algebra {CSP} is an event-based formalism that enables descriptions of patterns of system behaviour. This paper is concerned with the combination of these complementary views, in which {CSP} is used to describe the control executive for a {B} Abstract System. We discuss consistency between the two views and how it can be formally established. A typical avionics system motivates the work. Its specification and control executive are presented in the paper. The relationship with other approaches is also discussed.", annote = "Submitted by H. Treharne, 1999-09-01", } % Additional information: 11-16 Sept @Proceedings{VDM88, title = "{VDM} 88. {VDM} - The Way Ahead. 2nd {VDM}-Europe Symposium. Proceedings", editor = "Bloomfield, R. and Marshall, L. and Jones, R.", publisher = "Springer-Verlag, Berlin, West Germany", year = "1988", month = sep, keywords = "character sets, computer graphics, formal logic, formal specification, program compilers, program verification, software tools, specification languages, standardisation VDM, VDM, specification languages, B tool, compiler prototyping, NUSL, formal reasoning, flagship, Modula-2, VIP, SAMPLE, three-valued logic, predicates, MetaSoft, algebraic domain equations, proof rules, muffin, RAISE, term rewriting, software support, chinese characters", } % Additional information: 21-25 Oct @Proceedings{VDM91, title = "{VDM91}. Formal Software Development Methods. 4th International Symposium of {VDM} Europe Proceedings. Vol.2: Tutorials", editor = "Prehn, S. and Toetenel, W. J.", publisher = "Springer-Verlag, Berlin, Germany", month = oct, year = "1991", keywords = "formal logic, formal specification, programming theory, software reliability, specification languages, VDM, formal software development, LARCH, LCL specification languages, RAISE, ABEL formal development, PROSPECTRA methodology, refinement calculus, B-Method, mathematical methods, reliable systems development", } % Additional information: October 24-27 @InProceedings{WB95, title = "The Role of Testing in the {B} Formal Development Process", author = "Wa{\"e}selynck, H{\'e}l{\`e}ne and Boulanger, Jean-Louis", organization = "Toulouse", pages = "205--28", year = "1995", booktitle = "Proceedings of 6th International Symposium on software Reliability Engineering (ISSRE'95)", month = oct, publisher = "IEEE Comput. Soc. Press, Los Alamitos, CA, USA", abstract = "The {B} method is a formal approach covering all the software development process, through a series of proved refinement steps. An on-going debate in the {B} community is the removal of some classical verification steps of the design, e.g.\ unit and integration testing: this paper is aimed to support the maintaining stringent testing policies. We first recall previous work that addresses the general question of the limits of formal methods for ultra-high dependability. Then, the discussion is focused on the case of the {B} method. Although the method significantly contributes to fault avoidance, it is shown that additional verifications are still required throughout the development process, whether inspections or tests. (20 {R}efs)", keywords = "testing, B formal development process, B-Method, formal approach, software development process, proved refinement steps, classical verification steps, integration testing, stringent testing policies, ultra high dependability, fault avoidance", } @TechReport{Waeselynck97a, author = "Waeselynck, H{\'e}l{\`e}ne and Behnia, Salimeh", title = "{B} model animation for external verification", institution = "LAAS (TSF) -- INRETS (ESTAS)", year = "1997", pages = "15", number = "97392", } @TechReport{Waeselynck97b, author = "Waeselynck, H{\'e}l{\`e}ne and Behnia, Salimeh", title = "Towards a framework for testing {B} models", institution = "LAAS (TSF) -- INRETS (ESTAS)", keywords = "testing", year = "1997", pages = "22", number = "97225", } @PhdThesis{Watrin01, author = "Watrin, David", title = "Formalisation des mod{\`e}les d'information d'administration de r{\'e}seaux {\`a} l'aide de la m{\'e}thode {B} : Application au langage {GDMO}", school = "Ecole nationale sup{\'e}rieure des t{\'e}l{\'e}communications (Paris)", year = "2001", abstract = "Suite {\`a} la lib{\'e}ralisation des march{\'e}s de t{\'e}l{\'e}communications et {\`a} la multiplication de l'offre de services, l'Administration de R{\'e}seaux de T{\'e}l{\'e}communications conna\^{\i}t un r{\'e}el essor. A l'exception de SNMP, les diff{\'e}rentes technologies qui adressent cette activit{\'e} ont fait le choix de langages orient{\'e}s objets afin de d{\'e}crire leurs mod{\`e}les d'information. Ce choix est motiv{\'e} par des consid{\'e}rations d'{\'e}volutivit{\'e} bien connues. Cependant une constante se d{\'e}gage {\`a} travers ces langages: I'utilisation du langage naturel pour d{\'e}crire les contraintes et les comportements des objets g{\'e}r{\'e}s, des attributs et autres {<<}templates{>>}. Ce choix induit l'introduction d'ambigu{\"{}\i}t{\'e}s dans la sp{\'e}cification et n'autorise pas de traitement automatique afin de simuler ou tester le comportement, de v{\'e}rifier la coh{\'e}rence du mod{\`e}le ou de produire un code ex{\'e}cutable. Enfin les mod{\`e}les sont difficiles {\`a} appr{\'e}hender en raison d'une distribution anarchique de l'inforrnation. Ce travail de th{\`e}se propose une solution bas{\'e}e sur la formalisation des mod{\`e}les {\`a} l'aide de la m{\'e}thode B. Cette derni{\`e}re offre en effet un langage rigoureux et automatise les concepts de preuve formelle et de raffinement. Afin de d{\'e}finir une solution g{\'e}n{\'e}rique, les propri{\'e}t{\'e}s communes aux mod{\`e}les d'information de gestion de r{\'e}seaux ont {\'e}t{\'e} isol{\'e}es. Un ensemble de r{\`e}gles de traduction vers le formalisme {B} couvrant les structures de donn{\'e}es et les mod{\`e}les statique et dynamique est propos{\'e}. Des variantes sont avanc{\'e}es et analys{\'e}es lorsque aucune r{\`e}gle n'est pleinement satisfaisante. Ces r{\`e}gles ont {\'e}t{\'e} appliqu{\'e}es avec succ{\`e}s {\`a} un mod{\`e}le GDMO. La sp{\'e}cification {B} obtenue permet de prouver la coh{\'e}rence interne du mod{\`e}le et d'amorcer le processus de raffinement. En outre, un traducteur automatique depuis un mod{\`e}le GDMO vers une sp{\'e}cification {B} a {\'e}t{\'e} d{\'e}velopp{\'e}. Il offre une large couverture du langage et permet de saisir des propri{\'e}t{\'e}s formelles via une interface graphique. Il contribue {\`a} un enrichissement du mod{\`e}le d'information.", keywords = "network administration, formalisation, B-Method, GDMO, modelling, reliability, QoS, object-oriented method, formal language", } @InProceedings{Watson97, author = "Watson, Geoffrey Norman", title = "A comparison of modularity in {B} and {Cogito}", booktitle = "Formal Methods Pacific", pages = "263--286", year = "1997", editor = "Reeves, S. and Groves, L.", } @Book{Wordsworth96, author = "Wordsworth, John", title = "Software Engineering with {B}", publisher = "Addison-Wesley", year = "1996", ISBN = "0-201-40356-0", month = sep, } @InProceedings{Z2B-BDW95, author = "Bicarregui, Juan and Dick, Jeremy and Woods, Eoin", title = "Supporting the length of formal development : from diagrams to {VDM} to {B} to {C}", booktitle = "Proc. {Z} Twenty Years on - What is its Future", editor = "Habrias, Henri", ISBN = "2-906082-19-8", year = "1995", organization = "IRIN-IUT de Nantes", month = oct, pages = "63--75", URL = "http://theory.doc.ic.ac.uk:80/~jcb1/vdmbpapers.html", abstract = "This paper reports on the experience gained in the MaFMeth project which is undertaking a formal development with tool support for several parts of the life cycle from requirements capture through to C code generation. A number of issues arise from the limitations of different notations and tools and from their combination when applied to the development of software components destined to be integrated into a broader system context. We describe the problems we encountered, the mistake we made, and the solutions we adopted, for the benefit of both these applying formal methods to real product development, and for the creators and designers of methods and tools.", } @InProceedings{Z2B-Chauvet95, author = "Chauvet, J. Y.", title = "Le cas {<<}legislation vieillesse{>>}", booktitle = "Proc. {Z} Twenty Years on - What is its Future", editor = "Habrias, Henri", ISBN = "2-906082-19-8", year = "1995", organization = "IRIN-IUT de Nantes", month = oct, pages = "242--264", } @InProceedings{Z2B-Docherty95, author = "Docherty, Rosemary F.", title = "Translation from {Z} to {AMN}", crossref = "B96-Habrias", year = "1995", month = oct, pages = "205--228", abstract = "This paper gives details of a {B}-rulebase which I have written to translate Z specifications into Abstract Machine Notation (AMN). Although some Z constructs translate easily, others cause problems and the theory behind the conversion rules is given. The rulebase cannot translate certain Z constructs and the reasons for this are explained. The paper ends with some conclusions on the different manner and advantages specification in the two languages.", } @InProceedings{Z2B-Pratten95, author = "Pratten, C. H.", title = "An introduction to proving {AMN} Specifications with {PVS} and the {AMN-PROOF} Tool", booktitle = "Proc. {Z} Twenty Years on - What is its Future", editor = "Habrias, Henri", ISBN = "2-906082-19-8", year = "1995", organization = "IRIN-IUT de Nantes", month = oct, pages = "149--165", abstract = "The AMN-PROOF Tool generates proof obligations for AMN specification consistency and refinement validity in a form suitable for consideration by the PVS and HOL theorem provers. In this paper, we discuss our PVS representation of AMN proof obligations and introduce the PVS facilities of the AMN-PROOF Tool. We consider an example refinement, for which the proof obligations have been generated by the Tool and proved by PVS.", URL = "www.dsse.ecs.soton.ac.uk/{\~{}}chp/amn\_proof/doc/papers.html", keywords = "AMN specification proving, AMN-PROOF tool, proof obligations, AMN specification consistency, refinement validity, HOL theorem provers, PVS facilities", } @InProceedings{ZB00-Banach, author = "Banach, R. and Poppleton, M.", title = "Retrenchment, Refinement and Simulation", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", URL = "http://www.cs.man.ac.uk/~banach/some.pubs/Retrench.Ref.Sim.ps.gz", pages = "304--323", keywords = "axiomatic specifications, model based specifications", crossref = "ZB00", } @InProceedings{ZB00-Bellegarde, author = "Bellegarde, Fran{\c{c}}oise and Darlot, C. and Julliand, Jacques and Kouchnarenko, O.", title = "Reformulate Dynamic Properties during {B} Refinement and Forget Variants and Loop Invariants", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", crossref = "ZB00", pages = "230--249", year = "2000", } @InProceedings{ZB00-Bontron, author = "Bontron, Pierre and Potet, Marie-Laure", title = "Automatic Construction of Validated {B} components from Structured Developments", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", crossref = "ZB00", pages = "127--147", year = "2000", } @InProceedings{ZB00-Butler, author = "Butler, Michael J. and Meagher, Mairead", title = "Performing Algorithmic Refinement before Data Refinement in {B}", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", URL = "http://www.dsse.ecs.soton.ac.uk/techreports/2000/dsse-tr-2000-5.ps.gz", pages = "324--343", crossref = "ZB00", keywords = "methodology, refinement", } @InProceedings{ZB00-Cansell, author = "Cansell, Dominique and M{\'e}ry, Dominique", title = "Playing with abstraction and refinement for managing features interactions. {A} methodological approach to feature interaction problem", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", crossref = "ZB00", pages = "148--167", year = "2000", } @InProceedings{ZB00-Dimitrakos, author = "Dimitrakos, Theo and Bicarregui, Juan and Matthews, Brian and Maibaum, Tom and Robinson, Ken", title = "Compositional structuring in the {B} Method: {A} Logical Viewpoint of the Static Context", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", crossref = "ZB00", pages = "107--126", URL = "http://theory.doc.ic.ac.uk:80/~jcb1/zb2000.ps", } @InProceedings{ZB00-Laleau, author = "Laleau, Regine and Mammar, Amel", title = "A Generic Process to Refine a {B} Specification into a Relational Database Implementation", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", pages = "22--41", crossref = "ZB00", keywords = "refinement, methodology, relational databases", year = "2000", } @InProceedings{ZB00-Lanet, author = "Lanet, Jean-Louis", title = "Are Smart Cards the Ideal Domain for Applying Formal Methods?", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", pages = "363--374", source = "GEMPLUS", year = "2000", keywords = "smartcards, JavaCard", abstract = "The need of formal methods in the smart card domain has three origins: mastering the complexity of the new operating systems (fault avoidance), certifying at a high level a part of the smart card and reducing the cost of the test. In a first part, after presenting the smart card and its security requirements, we explain the certification process that appears to be the most important vector for introducing formal methods in the software development cycle. Then we present some attempts to formalise complex software elements of smart cards. The use of model checkers in order to automatically generate the test suites can notably increase the productivity of applet development. The second part of this paper explains why smart cards are not currently the expected success story of formal methods. Then we present some clues to help integration of these methods in the software development cycle.", } @InProceedings{ZB00-Lopez, author = "Lopez, Nestor and Simonot, Marianne and Viguie Donzeau-Gouge, Veronique", title = "Deriving Software Specifications from Event Based Models", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", year = "2000", keywords = "event-B", crossref = "ZB00", pages = "209--229", URL = "http://cedric.cnam.fr/PUBLIS/RC42.ps", } @InProceedings{ZB00-Robinson, author = "Robinson, Ken", title = "Reconciling Axomatic and Model\-based Specifications Using the {B} Method", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", pages = "95--106", keywords = "axiomatic specifications, model based specifications", crossref = "ZB00", } @InProceedings{ZB00-Stoddart, author = "Stoddart, Bill", title = "An Execution Architecture for {GSL}", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", crossref = "ZB00", year = "2000", pages = "394--413", keywords = "B-Method, animation, virtual machines, reversible computation", } @InProceedings{ZB00-Treharne, author = "Treharne, Helen and Schneider, Steve", title = "How to drive a {B} Machine", booktitle = "ZB'2000 -- International Conference of {B} and {Z} Users", crossref = "ZB00", pages = "188--208", year = "2000", } @Proceedings{ZB00, title = "{ZB}'2000 -- International Conference of {B} and {Z} Users", year = "2000", address = "Helsington, York, UK YO10 5DD", series = LNCS, volume = "1878", URL = "http://link.springer.de/link/service/series/0558/tocs/t1878.htm", month = Aug, ISBN = "3-540-67944-8", editor = "DCS-York", } @InProceedings{ZB02-Abrial, author = "Abrial, Jean-Raymond and Mussat, Louis", title = "On Using Conditional Definitions in Formal Theories", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "242--269", year = "2002", abstract = "In this paper, our intention is to explore the notion of definition in formal theories and, in particular, that of conditional definitions. We are also interested in analyzingthe consequences of the latter on the structure of corresponding proof systems. Finally, we shall investigate the various ways such proof systems can be simplified.", } @InProceedings{ZB02-Abrial2, author = "Abrial, Jean-Raymond and Cansell, Dominique and Lafitte, Guy", title = "{``}{H}igher-order{''} Mathematics in {B}", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "370--393", year = "2002", abstract = "In this paper, we investigate the possibility to mechanize the proof of some real complex mathematical theorems in B [1]. For this, we propose a little structure language which allows one to encode mathematical structures and their accompanying theorems. A little tool is also proposed, which translates this language into B, so that Atelier B, the tool associated with B, can be used to prove the theorems. As an illustrative example, we eventually (mechanically) prove the Theorem of Zermelo [6] stating that any set can be well-ordered. The present study constitutes a complete reshaping of an earlier (1993) unpublished work (referenced in [4]) done by two of the authors, where the classical theorems of Haussdorf and Zorn were also proved.", } @InProceedings{ZB02-Bellegarde, author = "Bellegarde, Fran{\c{c}}oise and Julliand, Jacques and Kouchnarenko, Olga", title = "Synchronised Parallel Composition of Events Systems in {B}", keywords = "event-B", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "436--457", year = "2002", abstract = "A large system typically is or can be decomposed as a composition of components. Usually, these components have to cooperate so, their composition is a synchronized parallel composition. Components are often reactive systems. In the B method, each component is an event system. Then, two development paradigms -- refinement and component composition -- can be used. To provide both paradigms we have a compositionality result of a synchronized parallel composition with respect to refinement. We make use of this result to get an eficient approach to verify the refinement of a synchronized parallel composition between components. Therefore, our proposal allows introducing a second development paradigm in B, the component paradigm.", } @InProceedings{ZB02-Bellegarde2, author = "Bellegarde, Fran{\c{c}}oise and Chouali, Samir and Julliand, Jacques", title = "{V}{\'e}rification of Dynamic constraints for {B} Event Systems under Fairness Assumptions", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", keywords = "event-B", pages = "477--496", year = "2002", abstract = "A B event systems is supposed to specify a closed system, i.e., the system is meant to be specified in isolation. So, the specifi- cation includes the specification of the system of interest and of its environment. Often, the environment supposes fairness constraints. Therefore, classically in a B system approach, we express the fairness of the environment by the specification of fair scheduler together with the events of the system of interest. This leads to an infinite state model even when the system is finite state by nature. This does not facilitate PLTL properties verification by model checking which is only effective on finite state models. In this paper, we propose to keep separate the fairness of the environment from the specification of the system of interest by a B event system. Then, the fairness is expressed as events which have to be fairly fired. So, a finite state system of interest has a finite state model. The chosen model is a finite labeled transition system which allows the model checking of PLTL properties using the fair events as assumptions. In the paper, we make diverse proposals-some of them are proposed as perspectives-for a verification under fairness assumptions. We use the protocol T=1 as a running example.", } @InProceedings{ZB02-Blow, author = "Blow, James and Galloway, Andy", title = "Generalised Subtitution Language and Differentials", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "396--415", year = "2002", abstract = "Embedded continuous control systems can be thought of as implementing complex(piecewise and pipelined) differential functions. Each 'piece' of the function may be preconditioned with a {``}domain of applicability{''}, which prescribes the circumstances the piece was designed to handle. The preconditions often involve rate of change, i.e. differentials, as well as range constraints. In this paper we present an adaptation of the substitution calculus which can be used to reason about such systems. Our approach is based on generalising the traditional view that a component is a fragment of a sequential programme. We consider a component to be an autonomous transformation which is 'clocked' to perform its computation at regular intervals, over and over again. In the case of such a component we can generalise the notion of weakest precondition to traces (sequences of values) of inputs and outputs. In our approach we characterise such traces by 'step' predicates over adjacent elements in the trace. We also generalise our calculus to cover nth order differentials. Since analysis can be performed at a comparable complexity to regular wp, our techniques are a powerful tool in the validation of continuous control systems.", } @InProceedings{ZB02-Bodeveix, author = "Bodeveix, Jean-Paul and Filali, Mamoun", title = "Type Synthesis in {B} and the translation of {B} to {PVS}", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "350--369", keywords = "type synthesis, PVS", year = "2002", abstract = "In this paper, we study the design of a typed functional semantics for B. Our aim is to reuse the well known logical frameworks based on higher order logic, e.g., Isabelle, Coq and PVS as proving environments for B. We consider type synthesis for B and study a semantics and some of its composition mechanisms by translation to PVS.", } @InProceedings{ZB02-Cansell, author = "Cansell, Dominique and Gopalakrishnan, Ganesh and Jones, Mike and M{\'e}ry, Dominique", title = "Incremental Proof of the Producer/Consumer Property for the {PCI} Protocol", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", keywords = "protocol", pages = "22--41", year = "2002", abstract = "We present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem [13],[15], the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.", } @InProceedings{ZB02-Chartier, author = "Chartier, Pierre", title = "{ABS} project, merging the best practices in software design from railway and aicraft industries", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", keywords = "Lustre", year = "2002", abstract = "The design of safety critical systems requires specific methods and tools to reach the safety level required. In the Railway Industry the B Method supported by the Atelier B have been used with success for several years now as shown by the emblematic METEOR metro system. In the Aircraft Industry the use of synchronous declarative languages like Lustre supported by the SCADE tool improves the quality of softwares and saves costs.", } @InProceedings{ZB02-Doche, author = "Doche, Marielle and Gravell, Andrew", title = "Extraction of Abstraction Invariants for Data Refinement", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "120--139", keywords = "data refinement, fundamentals", year = "2002", } @InProceedings{ZB02-Dunne, author = "Dunne, Steve", title = "A Theory of Generalised Substitutions", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "270--290", year = "2002", abstract = "We augment the usual wp semantics of substitutions with an explicit notion of frame, which allows us to develop a simple selfcontained theory of generalised substitutions outside their usual context of the B Method. We formulate three fundamental healthiness conditions which semantically characterise all substitutions, and from which we are able to derive directly, without need of any explicit further appeal to syntax, a number of familiar properties of substitutions, as well as several new ones specifically concerning frames. In doing so we gain some useful insights about the nature of substitutions, which enables us to resolve some hitherto problematic issues concerning substitutions within the B Method.", } @InProceedings{ZB02-Laleau, author = "Laleau, R{\'e}gine and Polack, Fiona", title = "Coming and Going from {UML} to {B} : {A} Proposal to support Traceability in Rigorous {IS} Development", keywords = "UML", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "517--534", year = "2002", } @InProceedings{ZB02-Legeard, author = "Legeard, Bruno and Peureux, Fabien and Utting, Mark", title = "A Comparison of the {BTT} and {TTF} Test-generation Methods", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "309--329", keywords = "test generation, testing", year = "2002", } @InProceedings{ZB02-Mikhailov, author = "Mikhailov, Leonid and Butler, Michael J.", title = "An Approach to Combining {B} and {A}lloy", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "140--161", keywords = "Alloy, model-checking", year = "2002", abstract = "In this paper we propose to combine two software verification approaches, theorem proving and model checking. We focus on the B-method and a theorem proving tool associated with it, and the Alloy specification notation and its model checker {``}Alloy Constraint Analyser{''}. We consider how software development in B can be assisted using Alloy and how Alloy can be used for verifying refinement of abstract specifications. We demonstrate our approach with an example.", } @InProceedings{ZB02-Papatsaras, author = "Papatsaras, Antonis and Stoddart, Bill", title = "Global and Communicating State Machine Models in Event Driven {B}: {A} Simple Railway Case Study", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", keywords = "event-B, railway", pages = "458--476", year = "2002", abstract = "We present a case study of a simple railway system to investigate and compare two ways of modelling a system in {``}event driven B{''}. We are interested in the specification of a system as a global model as well as the formulation of a distributed state machine model where individual components exchange information by means of shared events. In this paper we investigate the issues of {``}parameter hiding{''} and {``}scaling{''} as well as the parameterisation of events of the communicating components of such systems. We use two methods for expressing a class of components; we either create indexed B machines that can be instantiated or we represent the state of all components within a given class by means of a function.", } @InProceedings{ZB02-Poppleton, author = "Poppleton, Michael and Banach, Richard", title = "Controlling Control Systems: An Application of Evolving Retranchement", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", URL = "http://www.ecs.soton.ac.uk/~mrp/mrp_pubs/Retrench.Control.Evol.ZIP", pages = "42--61", year = "2002", } @InProceedings{ZB02-Schneider, author = "Schneider, Steve and Treharne, Helen", title = "Communicating {B} {MA}chines", booktitle = "ZB'2002 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB02", pages = "416--435", keywords = "CSP, concurrency, combining formalisms", year = "2002", abstract = "This paper describes a way of using the process algebra CSP to enable controlled interaction between B machines. This approach supports compositional verification: each of the controlled machines, and the combination of controller processes, can be analysed and verified separately in such a way as to guarantee correctness of the combined communicating system. Reasoning about controlled machines separately is possible due to the introduction of guards and assertions into description of the controller processes in order to capture assumptions about other controlled machines and provide guarantees to the rest of the system. The verification process can be completely supported by difierent tools. The use of separate controller processes facilitates the iterative development and analysis of complex control flows within the system. The approach is motivated and illustrated with a non-trivial running example.", } @Proceedings{ZB02, title = "{ZB}'2002 -- Formal Specification and Development in {Z} and {B}", year = "2002", address = "Grenoble, France", series = LNCS, volume = "2272", URL = "http://link.springer.de/link/service/series/0558/tocs/t2272.htm", month = Jan, ISBN = "3-540-43166-7", editor = "Bert, Didier and Bowen, Jonathan P. and Henson, Martin C. and Robinson, Ken", organization = "{LSR-IMAG}", } @Proceedings{ZB03, title = "{ZB}'2003 -- Formal Specification and Development in {Z} and {B},International Conference of {B} and {Z} Users, Turku, Finland, June 4-6, 2003, Proceedings", year = "2003", address = "Turku, Finland", publisher = "Springer", series = LNCS, volume = "2651", month = Jun, ISBN = "3-540-40253-5", editor = "Bert, Didier and Bowen, Jonathan P. and King, S. and Wald{\'e}n, M.", } @InProceedings{ZB03-Abrial, author = "Abrial, Jean-Raymond", title = "{B}\# : Toward a Synthesis between {Z} and {B}", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB03", pages = "168--177", year = "2003", abstract = "In this paper, I present some ideas and principles underlying the realization of a new project called B\#. This project follows the main ideas and principles already at work in B, but it also follows a number of older concepts developed in Z. In B\#, the intent is to have a formal system to be used to model complex system in general, not only software systems.", } @InProceedings{ZB03-Abrial2, author = "Abrial, Jean-Raymond and Cansell, Dominique and M{\'e}ry, Dominique", title = "Formal Derivation of Spanning Trees Algorithms", keywords = "spanning tree, event-B", crossref = "ZB03", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", year = "2003", pages = "457--476", abstract = "Graphs algorithms and graph-theoretical problems provide a challenging battle field for the incremental development of proved models. The {B} event-based approach implements the incremental and proved development of abstract models which are translated into algorithms; we focus our methodology on the minimum spanning tree problem and on Prim's algorithm. The correctness of the resulting solution is based on properties over trees and we show how the greedy strategy is efficient in this case. We compare properties proven mechanically to the properties found in a classical algorithms textbook.", } @InProceedings{ZB03-Aguirre, author = "Aguirre, Nazareno and Bicarregui, Juan and Dimitrakos, Theo", title = "Towards Dynamic Population Management of Abstract Machines in the {B Method}", keywords = "structuring mechanisms, modularisation, object-oriented, dynamic reconfiguration", crossref = "ZB03", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", year = "2003", pages = "528--545", abstract = "We study some restrictions associated with the mechanisms for structuring and modularising specifications in the {B} abstract machine notation. We propose an extension of the language that allows one to specify machines whose constituent modules (other abstract machines) may change dynamically, i.e., at run time. In this way, we increase the expressiveness of {B} by adding support for a common activity of the current systems design practice. The extensions were made without having to make considerable changes in the semantics of standard B. We provide some examples to show the increased expressive power, and argue that our proposed extensions respect the methodological principles of the {B} method.", } @InProceedings{ZB03-Blazy, author = "Blazy, Sandrine and Gervais, Fr{\'e}d{\'e}ric and Laleau, R{\'e}gine", title = "Reuse of Specification Patterns with the {B Method}", keywords = "design pattern, specification pattern, reuse", crossref = "ZB03", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", year = "2003", pages = "40--57", abstract = "This paper describes an approach for reusing specification patterns. Specification patterns are design patterns that are expressed in a formal specification language. Reusing a specification pattern means instantiating it or composing it with other specification patterns. Three levels of composition are defined: juxtaposition, composition with inter-patterns links and unification. This paper shows through examples how to define specification patterns in B, how to reuse them directly in B, and also how to reuse the proofs associated with specification patterns.", } @InProceedings{ZB03-Burdy, author = "Burdy, Lilian and Requet, Antoine", title = "Extending {B} with Control Flow Breaks", keywords = "B extension, control flow", crossref = "ZB03", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", year = "2003", pages = "513--527", abstract = "This paper describes extensions of the {B} language concerning control flow breaks in implementations and specification of operations with exceptional behaviors. It does not claim to define those extensions in a pure formal and complete way. It is rather a presentation of what could be done and how it could be done. A syntax is proposed and proof obligations are defined using a weakest precondition calculus extended to deal with abrupt termination. Examples emphasizing the advantages of these extensions are also given.", } @InProceedings{ZB03-Dunne, author = "Dunne, Steve", title = "Introducing Backward Refinement into {B}", crossref = "ZB03", booktitle = "ZB 2003: Formal Specification and Development in {Z} and {B}", pages = "178--196", year = "2003", abstract = "The {B} Method exploits a direct first-order wp predicate-transformer formulation of downward simulation to generate its proof obligations for a refinement, so B's notion of refinement is restricted to that of forward refinement. Therefore some refinements we would intuitively recognise as valid cannot be proved so in B. While relational formulations of upward simulation abound in the refinement literature, the only predicate-transformer formulations proposed hitherto have been higher-order ones quantified over all postconditions, which cannot be conveniently exploited by the {B} Method. Here, we propose a new first-order predicate-transformer formulation of upward simulation suitable to be adopted by {B} for backward refinement.", } @InProceedings{ZB03-Ferreira, author = "Ferreira, Carla and Butler, Michael J.", title = "Using {B} Refinement to Analyse Compensating Business Processes", keywords = "refinement, business process, StAC", crossref = "ZB03", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", year = "2003", pages = "477--496", abstract = "This paper explores the refinement of compensating business processes, which are modelled in a heterogeneous notation that combines StAC and B. In our refinement approach, the StAC behavioural and compensation information are explicitly embedded in a {B} machine. As the resulting machine is standard {B} one can use the {B} notion of refinement to prove the refinement of business processes. We also show how the Atelier-B prover can help in constructing the gluing invariant.", } @InProceedings{ZB03-Frappier, author = "Frappier, Marc and Laleau, R{\'e}gine", title = "Proving Event Ordering Properties for Information Systems", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB03", pages = "421--436", year = "2003", abstract = "This paper presents an approach to prove event ordering properties for {B} specifications of information systems. The properties are expressed using the E3 notation, where input event ordering properties are defined using a process algebra similar to {CSP} and output events are specified by recursive functions on the input traces associated to the process expression. By proving that the E3 specification is refined by the {B} specification, using the {B} theory of refinement, we ensure that both specifications accept and refuse exactly the same event traces. The proof relies on an extended labeled transition system, generated using the operational semantics of the process algebra, in order to deal with unbounded systems. The gluing invariant is generated from the E3 recursive functions.", keywords = "E3, B-Method, process algebra, trace-based specifications, refinement", } @InProceedings{ZB03-Hallerstede, author = "Hallerstede, Stefan", title = "Parallel Hardware Design in {B}", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB03", pages = "101--102", year = "2003", keywords = "hardware, event-B", abstract = "We present the design of a parallel synchronous hardware component from a purely functional description of its behaviour. Starting from an abstract specification of a linear time-invariant (LTI) system in {Event-B} a pipelined implementation is developed. The presented approach is applicable to LTI systems that can be represented as linear constant-coefficient difference equations. In the development of embedded systems space requirements and performance of used circuits are often the two most important constraints. To achieve high performance a high degree of parallelism is needed. At the same time, space requirements demand the use of as few components as possible. In this study we show how the {B} method may be used to design systems that meet these requirements. We use a variant of the {B} method called {Event-B}. {Event-B} has been conceived particularly for the modelling of abstract systems. Such systems are closed in the sense that they do not interact with some kind of environment. The environment is part of the specification. {Event-B} has been used to construct proved circuits. We follow a similar approach in this study.", } @InProceedings{ZB03-MacIver, author = "McIver, Annabelle and Morgan, Carroll and Hoang, Thai Son", title = "Probabilistic Termination in {B}", crossref = "ZB03", booktitle = "ZB 2003: Formal Specification and Development in Z and B", pages = "216--239", year = "2003", keywords = "probabilistic B, pAMN, operators", abstract = "The {B} Method does not currently handle probability. We add it in a limited form, concentrating on {``}almost-certain{''} properties which hold with probability one; and we address briefly the implied modifications to the programs that support B. The Generalised Substitution Language is extended with a binary operator $\oplus$ representing {``}abstract probabilistic choice{''}, so that the substitution $prog_1 \oplus prog_2$ means roughly {``}choose between prog1 and prog2 with some probability neither one nor zero{''}. We then adjust B's proof rule for loops -- specifically, the variant rule -- so that in many cases it is possible to prove {``}probability-one{''} correctness of programs containing the new operator, which was not possible in {B} before, while remaining almost entirely within the original Boolean logic. Applications include probabilistic algorithms such as the IEEE 1394 Root Contention Protocol ({``}FireWire{''}) in which a probabilistic {``}symmetry-breaking{''} strategy forms a key component of the design.", } @InProceedings{ZB03-Morgan, author = "Hoang, Thai Son and Jin, Zhendong and Robinson, Ken and McIver, Annabelle and Morgan, Carroll", title = "Probabilistic Invariants for Probabilistic Machines", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", crossref = "ZB03", pages = "240--259", year = "2003", keywords = "probability, program correctness, generalised substitutions, weakest preconditions, B-Method, probabilistic algorithms, probabilistic B, pAMN", abstract = "Abrial's Generalised Substitution Language [4] can be modified to operate on arithmetic expressions, rather than Boolean predicates, which allows it to be applied to probabilistic programs [13]. We add a new operator $_p\otimes$ to GSL, for probabilistic choice, and we get the probabilistic Generalised Substitution Language (pGSL): a smooth extension of GSL that includes random algorithms within its scope. In this paper we begin to examine the effect of pGSL on B's larger-scale structures: its machines. In particular, we suggest a notion of probabilistic machine invariant. We show how these invariants interact with pGSL, at a fine-grained level; and at the other extreme we investigate how they affect our general understanding {``}in the large{''} of probabilistic machines and their behaviour. Overall, we aim to initiate the development of probabilistic {B} (pB), complete with a suitable probabilistic AMN. We discuss the practical extension of the B-Toolkit [5] to support pB, and we give examples to show how pAMN can be used to express and reason about probabilistic properties of a system.", } @InProceedings{ZB03-Poerschke, author = "Poerschke, Christine and Lightfoot, David E. and Nealon, John L.", title = "A Formal Specification in {B} of a Medical Decision Support System", keywords = "medical application, formal specification", crossref = "ZB03", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", year = "2003", pages = "497--512", abstract = "We have used the {B} notation to formally specify an existing medical decision support system. The system runs on a palmtop computer and helps patients with insulin-dependent diabetes decide on a dose of insulin to inject. Using extracts we both qualitatively and quantitatively describe the formal specification and compare it with the existing C/C++ implementation of the system. We also report our experience of the specification process, the benefits derived from and the challenges presented by it. We conclude that the use of an abstract machine notation such as {B} for the formal specification and documentation of a knowledge-based medical decision support system is both feasible and viable.", } @InProceedings{ZB03-Pouzancre, author = "Pouzancre, Guilhem", title = "How to Diagnose a Modern Car with a Formal {B} Model?", crossref = "ZB03", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", pages = "98--100", year = "2003", abstract = "We introduce a modern method to diagnose vehicles. The method has been studied for Automobiles Peugeot. The classical methods to diagnose a car are based on technician's experience and failure knowledge (e.g., diagnostic trees). However cars become more and more complex and failures less and less predictable. The modern cars are increasingly complex due to electronic components and services: lights and wipers turn on automatically, engine controller manages efficiently the torque and car radio manages the sound depending on the car speed. Therefore, diagnostic of deficient components is complex, because of the car complexity and distributed functionalities: for example wheel sensors deficiency can induce effects on the car radio. On the other hand, deficiencies are mostly unpredictable, due to a wide variety of suppliers, car options and the short component life-cycle. Furthermore, garage mechanics have to diagnose bugs, which are, by definition, unpredictable. However, all failures have a similar characteristic: a functional component does not respect its nominal specification. In our diagnosis method, event {B} models formalize the nominal functional specification and a {B} model interpreter (BI) checks which component does not match its specification. To diagnose a car with this method we need: Correct and complete description of every vehicle component (vehicle {B} model) A rigourous link between the concrete car and the {B} models (dictionaries) A method to compare the components behaviour with their specification (record analysis)", } @InProceedings{ZB03-Stoddart, author = "Stoddart, Bill and Zeyda, Frank", title = "Expression Transformers in {B-GSL}", crossref = "ZB03", booktitle = "ZB 2003: Formal Specification and Development in Z and B", pages = "197--215", abstract = "The {B} concept of generalised substitutions is applied to expressions as well as predicates to obtain {``}expression transformers{''}, which formalise the idea of speculative computation and form part of the executable subset of our language. We define expression transformers over the syntactic constructs of B-GSL, and show this definition is equivalent to an alternative based on before-after predicates. The use of expression transformers is illustrated by example programs which combine functional and imperative programming styles and exploit backtracking.", keywords = "expression transformers, term transformers, predicate transformers, B-Method, combining functional and imperative programming, backtracking, reversible computation", } @InProceedings{ZB03-Treharne, author = "Treharne, Helen and Schneider, Steve and Bramble, Marchia", title = "Composing Specifications Using Communication", crossref = "ZB03", booktitle = "ZB'2003 -- Formal Specification and Development in {Z} and {B}", pages = "58--78", year = "2003", keywords = "CSP, composing specifications, combining formalisms, concurrency", abstract = "This paper develops a case study using the process algebra {CSP} to enable controlled interaction between {B} machines. This illustrates how {B} machines are essential components within a combined communicating system. The development steps used to build the case study are new: they are applications of theoretical results which allow us to focus on the external interface of a combined communicating system, compositionally verify it, and show that it is a refinement of a more abstract specification described in CSP. This allows safety and liveness properties to be established for combinations of communicating {B} machines.", } @Book{arago20, editor = "OFTA", title = "Application des techniques formelles au logiciel", publisher = "Observatoire Fran{\c{c}}ais des Techniques Avanc{\'e}ees \& Lavoisier TEC \& DOC", year = "1997", } @InProceedings{Bicarregui99, author = "Bicarregui, Juan C. and Dimitrakos, Th. and Lano, Kevin and Maibaum, T. and Matthews, B. M. and Ritchie, B.", title = "The {VDM+B} Project : Objectives and Progress", booktitle = "FM'99 VDM workshop at FM'99 World Congress On Formal Methods In The Development Of Computing Systems", year = "1999", address = "Toulouse, France", month = sep, } @InProceedings{Bieber95, author = "Bieber, Pierre", title = "Sp{\'e}cification et {V}{\'e}rification avec la m{\'e}thode {B} d'un protocole de s{\'e}curit{\'e}", booktitle = "Journ{\'e}es Formalisation des Activit{\'e}s Concurrentes", year = "1995", address = "Toulouse", month = apr, } @Misc{eventb-reference-manual, author = "{C}lear{S}y", title = "Event {B} reference manual", keywords = "event-B", month = jun, year = "2001", URL = "{http://www.atelierb.societe.com/ressources/evt2b/eventb_reference_manual.pdf}", } @InProceedings{Jambon-2001, author = "Jambon, Francis and Girard, Patrick and A{\"\i}t-Ameur Yamine", title = "Engineering for Human-Computer Interaction", booktitle = "8th IFIP International Conference, EHCI'01, Toronto, Canada, May 2001", pages = "39--55", year = "2001", editor = "Little, Reed Murray and Nigay, Laurence", volume = "2254", abstract = "This paper introduces a new technique for the verification of both safety and usability requirements for safety-critical interactive systems. This technique uses the model-oriented formal method {B} and makes use of an hybrid version of the MVC and PAC software architecture models. Our claim is that this technique -that uses proofs obligations- can ensure both usability and safety requirements, from the specification step of the development process, to the implementation. This technique is illustrated by a case study: a simplified user interface for a Full Authority Digital Engine Control (FADEC) of a single turbojet engine aircraft.", keywords = "safety, requirement, B-Method, FADEC", } @Unpublished{matisse-cir, author = "Abrial, Jean-Raymond", title = "Event Driven Circuit Construction", note = "MATISSE project", keywords = "event-B", month = aug, year = "2000", URL = "http://www.matisse.qinetiq.com/cir.pdf", } @Unpublished{matisse-dis, author = "Abrial, Jean-Raymond", title = "Event Driven Distributed Program Construction", note = "MATISSE project", keywords = "event-B", month = aug, year = "2001", URL = "http://www.matisse.qinetiq.com/dis.pdf", } @Unpublished{matisse-fg, author = "Abrial, Jean-Raymond", title = "Guidelines to Formal System Studies", note = "MATISSE project", month = nov, year = "2000", URL = "http://www.matisse.qinetiq.com/formal_guidelines_v2.pdf", } @Unpublished{matisse-pap, author = "Abrial, Jean-Raymond", title = "Event Driven Sequential Program Construction", note = "MATISSE project", keywords = "event-B", month = oct, year = "2000", URL = "http://www.matisse.qinetiq.com/pap.pdf", } @Article{reactive-B, author = "Lano, Kevin", title = "Specifying reactive systems in {B AMN}", journal = LNCS, series = LNCS, year = "1997", volume = "1212", pages = "242--275", } @InProceedings{Sekerinski2001, author = "Sekerinski, E. and Zurob, R.", title = "{iState}: {A} Statechart Translator", booktitle = "{UML} 2001 - The Unified Modeling Language, Toronto, Canada", pages = "376--390", year = "2001", editor = "Gogolla, M. and Kobryn C.", number = "2185", month = oct, publisher = "Lecture Notes in Computer Science, Springer-Verlag", } @InProceedings{Sekerinski2002, author = "Sekerinski, E. and Zurob, R.", title = "Translating Statecharts to {B}", booktitle = "Proceedings of Integrated Formal Methods, Turku, Finland", year = "2002", month = may, organization = "IFM 2002", publisher = "Lecture Notes in Computer Science, Springer-Verlag", abstract = "We present algorithms for the translation of statecharts to the Abstract Machine Notation of the {B} method. These algorithms have been implemented in iState, a tool for translating statecharts to various programming languages. The translation proceeds in several phases. We give a model of statecharts, a model of the code in AMN, as well as the intermediate representations in terms of class diagrams and their textual counterpart. The translation algorithms are expressed in terms of these models. We also discuss optimizations of the generated code. The translation scheme is motivated by making the generated code comprehensible.", } @InProceedings{zum94:Diller, title = "{Z} and {A}bstract {M}achine {N}otation: a comparison", author = "Diller, A. and Docherty, R.", pages = "250--263", year = "1994", ISBN = "3-540-19884-9", booktitle = "{P}roceedings of 8th {Z} {U}ser {M}eeting - {ZUM}'94", abstract = "{C}ompares the formal specification languages {Z} and {A}bstract {M}achine {N}otation ({AMN}); the latter of which is due to {A}brial. {T}he strategy adopted is that of presenting the same specification both in {Z} and {AMN} and of commenting on salient differences as they arise. {T}he specification chosen is a slightly revised version of the specification of an {I}nternal {T}elephone {N}umber {D}atabase found in chapter 4 of {A}.{Z}. {D}iller (1994). {A}t the end of the paper some general conclusions are drawn. (11 {R}efs)", keywords = "Z, formal specification language, AMN, internal telephone number database", } % Additional information: selectivity : {40/120} @InProceedings{BRILLANT05a, author = "Colin, Samuel and Petit, Dorian and Rocheteau, J{\'e}r{\^o}me and Marcano-Kamenoff, Rafa{\"e}l and Mariano, Georges and Poirriez, Vincent", title = "{BRILLANT} : An Open Source and {XML}-based platform for Rigourous Software Development", booktitle = "SEFM (Software Engineering and Formal Methods)", year = "2005", keywords = "formal tools, XML, BRILLANT", month = sep, organization = "AGKI (Artificial Intelligence Research Koblenz)", address = "Koblenz, Germany", publisher = "IEEE Computer Society Press", } @InProceedings{ASM05-Butler, author = "Butler, Michael J. and Leuschel, M. and Snook, C.", title = "Tools for system validation with {B} abstract machines", keywords = "UML, B-Method, tools, AMN, RODIN, ProB", booktitle = "Proceedings of ASM 2005: 12th International Workshop on Abstract State Machines", year = "2005", URL = "http://eprints.ecs.soton.ac.uk/10490/", address = "Paris", abstract = "In this paper we give an overview of some tools that we have developed to support the application of the {B} Method. {ProB} is an animation and model checking tool for the {B} method. {ProB}'s animation facilities allow users to gain confidence in their specifications. {ProB} contains a temporal and a state-based model checker, both of which can be used to detect various errors in {B} specifications. We also overview a recent extension of {ProB} that supports checking of specifications written in a combination of {CSP} and B. Finally we describe the UML-B profile and associated U2B tool that allows {UML} and {B} to be combined and is intended to make modelling with {B} more appealing to software engineers.", } % Additional information: October 23-25 @InProceedings{EDCC4, author = "Boulanger, Jean-Louis and Aljer, Ammar and Mariano, Georges", title = "{B/HDL}, an experiment to formalizing hardware by software formals specifications.", booktitle = "EDCC4, Fourth European Dependable Computing Conference, Parc des Expositions,Toulouse , France", keywords = "hardware, B-Method, formal development, software verification, safety-critical applications, BHDL, hardware, VHDL, codesign", year = "2002", month = oct, ps = "http://www.hds.utc.fr/~boulange/documents/2002/edcc4.ps", pdf = "http://www.hds.utc.fr/~boulange/documents/2002/edcc4.pdf", URL = "http://www.hds.utc.fr/~boulange/biblio-web.html", abstract = "In this paper, we presented a part of our work to create {B} libraries which correspond to some VHDL packages, as the STD\_LOGIC\_1164 package. This project enables us to take advantage of the power of the {B} method to develop a secure circuit. We write the specification of a desired circuit, then little by little we refine our specifications to reach to the implementation of this circuit which depends on the desired libraries. The {B} method due to J.R Abrial is a formal method for the incremental development of specifications and their refinements down to an implementation. It is a model-based approach similar to Z and VDM. The software design in {B} starts from mathematical specifications. Little by little, through many refinement steps , the designer tries to obtain a complete and executable specification. This process must be monotonic, that is any refinement has to be proven coherent according to the previous steps of refinement. The {B} tool can automatically decide which induced proofs are necessary to verify this correctness. Then these proofs are produced either automatically for the simple ones or in cooperation with the designer for the comlex ones. The abstract machine is the basic element of a {B} development. It encapsulates some state data and offers some operations. In the {B} development, the proofs accompany the construction of software. Each time an abstract machine is defined or modified, there are proof obligations related to its mathematical consistency; if the machine is a refinement or an implementation, there are also proofs of its correctness with respect to the previous steps of the development chain. The {B} tool allow to generate automatically the proof obligations for each abstract machine. Generally speaking, the proof obligations will be all the more complex as concrete details are introduced. So, at the last refinement, the implementation, we obtain a secure software which does not need to be tested. On the other hand, VHDL (VHSIC - Very High Speed Integrated Circuits - Hardware Description Language) is an IEEE Standard since 1987. It is {``}a formal notation intended for use in all phases of the creation of electronic systems [ ... ] it supports the development, verification, synthesis, and testing of hardware designs, the communication of hardware design data ...{''} (Preface to the IEEE Standard VHDL Language Reference Manual). This presentation is devoted to showing the cross fertilisation between the circuit design methodology and the {B} method concepts. In fisrt work , the famous standard VHDL package, the STD\_LOGIC\_1164, is transposed in the form of a {B} library as an example to be used as a set of {B} elementary components.In the same way, other VHDL packages can be translated as {B} circuit components in order to give to the designer a high-level view. Using this approach, one can develop a circuit of which each part of the specification is proven to be correct. A {B} circuit may be easily improved and it may be integrated with the other elements in the environment to satisfy safety conditions. We intend to create several libraries in {B} equivalent to the VHDL libraries, in order to facilitate the circuit design in {B}. Also this facilitates the transformation operation from {B} to VHDL. We try to find a common rule which may be used to automise the translation. Also we may solve this problem by creating a physical library in {B} that contains the characteristics of the basic electronic elements or by retranslating the results of a circuit development from {B} to VHDL. Semi-automatic translation of similar VHDL specification to {B} abstract machine is another way of work. In a first step, where we define the properties of the new compoents. The second step, is graphical, it introduce the components synthesis by composition of basic components.", } % Additional information: 12 - 14 June @InProceedings{Mariano2002, author = "Mariano, Georges and Boulanger, Jean-Louis and Aljer, Ammar", title = "Formalization of Digital Circuits Using the {B} Method", booktitle = "CompRail VIII, Eighth International Conference on Computer Aided Design, Manufacture and Operation in the Railway and Other Advanced Mass Transit Systems, Lemnos, Greece", keywords = "B-Method, formal development, software verification, safety-critical applications, VHDL, BHDL, hardware, codesign", year = "2002", month = jun, URL = "http://www.wessex.ac.uk/conferences/2002/cr02/", } % Additional information: May 21st-24th @InProceedings{AFIS02, author = "Boulanger, Jean-Louis and Mariano, Georges", title = "Formalization of Digital Circuits Using the {B} Method", booktitle = "AFIS, EUSEC 3rd European Systems Engineering Conference Systems Engineering: a focus of European expertise, session 10 Modelling \& Tool, Toulouse (France).", pages = "281--290", year = "2002", month = may, URL = "http://www.afis.fr", keywords = "hardware, BHDL, codesign", } @TechReport{INRETS01-717, author = "Boulanger, Jean-Louis and Aljer, Ammar and Mariano, Georges and Tison, Sophie and Devienne, Philippe", title = "Formalization of Digital Circuits Using the {B} Method", institution = "INRETS-ESTAS", year = "2001", number = "01-717", month = jul, keywords = "hardware, BHDL, codesign", } @TechReport{INRETS9925, author = "Boulanger, Jean-Louis and Georges, Mariano", title = "Mod{\'e}lisation Formelle de circuits num{\'e}riques par la m{\'e}thode {B}", institution = "INRETS-ESTAS", year = "1999", number = "TR-99-25", month = oct, ps = "http://www.hds.utc.fr/~boulange/documents/1999/1999-25-RT.ps", pdf = "http://www.hds.utc.fr/~boulange/documents/1999/1999-25-RT.pdf", URL = "http://www.hds.utc.fr/~boulange/biblio-web.html", keywords = "hardware, BHDL, codesign", } % Additional information: 4-6 decembre @InProceedings{ICSSEA01, author = "Boulanger, Jean-Louis and Mariano, Georges and Aljer, Ammar", title = "Conception s{\^u}re de circuit bas{\'e}e sur la notion de propri{\'e}t{\'e}", keywords = "hardware, BHDL, codesign", booktitle = "14{\`e}mes Journ{\'e}es Internationales G{\'e}NIE LOGICIEL \& ING{\'e}NIERIE DE SYST{\`E}MES et leurs APPLICATIONS. SESSION 8 : M{\'e}THODES FORMELLES", year = "2001", month = dec, organization = "ICSSEA'01", publisher = "CNAM Paris", URL = "http://www.hds.utc.fr/~boulange/Presentation/ICSSEA01/", abstract = "The goal of this paper is to show how it is possible to combine the advantages of the {B} method in order to design secure digital circuits that may be easily developed and does not need a design test. The circuit design may be based on the libraries of well-known circuit design language like VHDL. Our goal is to make use of {B} method to produce the electronic or numeric circuits. At the beginning, the circuit specifications are written in the abstract machine. The refinement direction is determined by the basic elements which are used to construct the desired circuit. So the designer can orient the development to the needed level. This level can be found as a basic library in B. We demonstrate how VHDL packages can be tanslated as circuit components for giving to the designer a high-level view. Using this approach, one can develop a circuit of which each part of the specification has proved to be correct. From the {B} model it is possible to generate the VHDL code. In this paper, we describes and models some synchronized basic components which will be then reused. A synchronized circuit is view as a box, within which an (or more) input line is entering, and out of which an output line (or more) is emerging. A synchronized circuit is supposed to be synchronized by a clock. Our aim is to give a general method to model a circuit without knowing the details of the desired circuit. At first the analogy of development between the b method and the numeric circuits design is presented. Using this approach, one can develop a circuit of which each part of the specification is proved to be correct. A circuit may be easily improved and it may be integrated with the other elements in the environment to satisfy safety conditions. The last section of this paper summarises this work and shows its advantages and disadvantages. This paper continue the previous work. We illustrate the method with an example extract from [2] which describes a fail-safe interface able to generate the fail-safe signaIs required in this railways system. Actuators in safety critical systems must be driven by failsafe signais. Under a failure in the system, such a signal must be either on the correct or on the safe state (e.g. red colour in traffic contra! lights).", ps = "http://www.hds.utc.fr/~boulange/documents/2001/resume_icssea01.ps", pdf = "http://www.hds.utc.fr/~boulange/documents/2001/resume_icssea01.pdf", URL = "http://www.hds.utc.fr/~boulange/biblio-web.html", } @Unpublished{RODIN-BEvt, author = "Metayer, Christophe and Abrial, Jean-Raymond and Voisin, Laurent", title = "Event-{B} Language", note = "RODIN Project Deliverable D7", keywords = "RODIN, tools, language, grammar, type-checking", month = may, year = "2005", URL = "http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf", } @Article{Schneider05, author = "Schneider, Steve and Hoang, Thai Son and Robinson, Ken and Treharne, Helen", title = "Tank Monitoring: {A} {pAMN} Case Study", journal = "Electronic Notes in Theoretical Computer Science", year = "2005", abstract = "The introduction of probabilistic behaviour into the B-Method is a recent development. In addition to allowing probabilistic behaviour to be modelled, the relationship between expected values of the machine state can be expressed and verified. This paper explores the application of probabilistic {B} to a simple case study: tracking the volume of liquid held in a tank by measuring the flow of liquid into it. The flow can change as time progresses, and sensors are used to measure the flow with some degree of accuracy and reliability, modelled as non-deterministic and probabilistic behaviour respectively. At the specification level, the analysis is concerned with the expectation clause in the probabilistic {B} machine and its consistency with machine operations. At the refinement level, refinement and equivalence laws on probabilistic GSL are used to establish that a particular design of sensors delivers the required level of reliability.", keywords = "probabilistic B, refinement, formal methods, probabilistic predicate transformers, pAMN", volume = "137", number = "2", pages = "183--204", } @InProceedings{ZB05-Leuschel, author = "Leuschel, Michael and Turner, Edd", title = "Visualising Larger State Spaces in {Pro B}", booktitle = "ZB05", year = "2005", pages = "6--23", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "{ProB} is an animator and model checker for the B method. It also allows to visualise the state space of a {B} machine in graphical way. This is often very useful and allows users to quickly spot whether the machine behaves as expected. However, for larger state spaces the visualisation quickly becomes difficult to grasp by users (and the computation of the graph layout takes considerable time). In this paper we present two relatively simple algorithms to often considerably reduce the complexity of the graphs, while still keeping relevant information. This makes it possible to visualise much larger state spaces and gives the user immediate feedback about the overall behaviour of a machine. The algorithms have been implemented within the {ProB} toolset and we highlight their potential on several examples. We also conduct a thorough experimentation of the algorithm on 47 {B} machines and analyse the results.", keywords = "formal methods, B-Method, tools, model-checking, animation, visualisation, logic programming", } @InProceedings{ZB05-Dunne, author = "Dunne, Steve and Conroy, Stacey", title = "Process Refinement in {B}", booktitle = "ZB2005", year = "2005", pages = "45--64", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", keywords = "CSP, refinement", abstract = "We describe various necessary and sufficient conditions with which to augment {B} existing refinement proof obligations for forward and backward refinement in order to capture within the B Method a variety of {CSP} process refinement relations, including most significantly that of failures-divergences which provides the standard denotational semantics of {CSP} processes.", } @InProceedings{ZB05-Attiogbe, author = "Attiogb{\'e}, Christian", title = "A Stepwise Development of the {Peterson}'s Mutual Exclusion Algorithm Using {B Abstract Systems}.", booktitle = "ZB05", year = "2005", pages = "124--141", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "We present a stepwise formal development of the Petersonrsquos mutual exclusion algorithm using {Event B}. We use a bottom-up approach where we introduce the parallel composition of subsystems which are separately specified. First, we specify subsystems as {B} abstract systems; then we compose the subsystems to get a first abstract solution for the mutual exclusion. This solution is improved to obtain the Peterson's algorithm. This is achieved by refinement and composition of the former abstract subsystems. Therefore the result is formally proved on the basis of correctness (safety) properties added to the invariant. {Atelier B} (a {B} prover) is used to check completely the development.", keywords = "event-B, parallel composition, refinement, mutual exclusion", } @InProceedings{ZB05-Bostrom, author = "Bostr{\"o}m, Pontus and Wald{\'e}n, Marina A.", title = "An Extension of {Event B} for Developing Grid Systems.", booktitle = "ZB05", year = "2005", pages = "142--161", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "Computational grids have become widespread in organizations for handling their need for computational resources and the vast amount of available information. Grid systems, and other distributed systems, are often complex and formal reasoning about them is needed, in order to ensure their correctness and to structure their development. {Event B} is a formal method with tool support that is meant for stepwise development of distributed systems. To facilitate the implementation of grid systems we here propose extensions to {Event B} that take grid specific features into account. We add new constructs to model the client-server architecture of grid systems, as well as important features like communication and synchronisation. We introduce the extensions in such a manner that the necessary proof obligations are automatically generated and the system can be implemented in a straightforward manner.", keywords = "grid computing", } @InProceedings{ZB05-Morgan, author = "Morgan, Carroll and Hoang, Thai Son and Abrial, Jean-Raymond", title = "The Challenge of Probabilistic {Event B} - Extended Abstract.", booktitle = "ZB05", year = "2005", pages = "162--171", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "Among the many opportunities offered by computational semantics for probability, the challenge of probabilistic {Event B} (pEB) is one of the most attractive. The {B} method itself is now almost 20 years old, and has been much improved and adapted over that time by the many projects to which it has been applied, and by its philosophy -- right from the start -- that it must be practical, effective and amenable to tool support.; more recently, {Event B} has extended it and altered its style of use. The probabilistic-program semantics we appeal to is even older (in Kozen's original form), but has only recently been ldquorevivedrdquo in the context of B-style abstraction and refinement. The especial attraction of putting the two together is the likely interplay between the probabilistic theory, on the one hand, and the decades of practical experience that have by now been built-in to the {B} approach, on the other. In particular, there are areas where a full theoretical treatment of probability, concurrency, abstraction and refinement -- all at once -- seems prohibitively complex; and yet in practice either the complexities seldom occur, or the exigencies of Brsquos having been so-often applied to real, non-toy problems has forced it to evolve styles for avoiding such complexities. In short, we want to use (event) {B} to guide us towards the issues that truly are important. Rabin's randomized mutual-exclusion algorithm is used as a motivating case study.", keywords = "event-B, probabilistic B, pAMN", } @InProceedings{ZB05-Zeyda, author = "Zeyda, Frank and Stoddart, Bill and Dunne, Steve", title = "A Prospective-Value Semantics for the {GSL}.", booktitle = "ZB05", year = "2005", pages = "187--202", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "We present a prospective-value (pv) semantics for the Generalised Substitution Language. Whereas wp semantics captures the meaning of a computation in terms of the weakest precondition that must be fulfilled for a generalised substitution S to establish any given postcondition Q, pv semantics expresses the meaning of a computation in terms of the value any expression E would take were the computation to be carried out. To integrate non-termination we formulate improper bunch theory, an extended version of Hehnerrsquos bunch theory where each type is augmented with an improper bunch. Algebraic simplification laws for the pv expression transformer are presented, and proved to be sound. Iteration is treated as a fixed-point in expressions, and a corresponding theorem is presented allowing us to infer the pv effect of the while-loop construct.", keywords = "generalised substitutions, bunch theory, prospective-value semantics, expression transformers, WP calculus, B-Method", } @InProceedings{ZB05-Banach, author = "Banach, Richard and Fraser, Simon", title = "Retrenchment and the {B-Toolkit}.", booktitle = "ZB05", year = "2005", pages = "203--221", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", keywords = "retrenchment", abstract = "An experiment to incorporate retrenchment into the B-Toolkit is described. The syntax of a retrenchment construct is given, as is the proof obligation which gives retrenchment its semantics. The practical aspects of incorporating these into the existing B-Toolkit are then investigated. It transpires that the B-Toolkit's internal architecture is heavily committed to monolithic refinement, because of B-Method philosophy, and this restricts what can be done without a complete rebuild of the toolkit. Experience with case studies is outlined.", } @InProceedings{ZB05-Abrial, author = "Abrial, Jean-Raymond and Cansell, Dominique and M{\'e}ry, Dominique", title = "Refinement and Reachability in {Event B}", booktitle = "ZB05", year = "2005", pages = "222--241", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "Since the early 90's (after the seminal article of R. Back [4]), the refinement of stuttering steps [5] are performed by means of new actions (called here events) refining skip. It is shown in this article that such a refinement method is not always possible in the development of large systems. We shall instead use events refining some kind of non-deterministic actions maintaining the invariant (sometimes called keep). We show that such new refinements are completely safe. In a second part, we explain how such a mechanism can be used to express some reachability conditions that were otherwise expressed using some special temporal logic statements {\`a} la TLA [5] in a previous article [2]. Examples will be used to illustrate our proposals.", keywords = "event-B, stuttering, refinement, reachability", } @InProceedings{ZB05-Zimmermann, author = "Zimmermann, Yann and Toma, Diana", title = "Component Reuse in {B} Using {ACL2}.", booktitle = "ZB05", year = "2005", pages = "279--298", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "We present a new methodology that permits to reuse an existing hardware component that has not been developed within the {B} framework while maintaining a correct design flow. It consists of writing a specification of the component in {B} and proving that the VHDL description of the component implements the specification using the ACL2 system. This paper focuses on the translation of the {B} specification into ACL2.", keywords = "ACL2, BHDL, hardware, VHDL, codesign", } @InProceedings{ZB05-Bert, author = "Bert, Didier and Potet, Marie-Laure and Stouls, Nicolas", title = "{G}ene{S}yst: {A} Tool to Reason About Behavioral Aspects of {B} {E}vent Specifications. Application to Security Properties.", booktitle = "ZB", year = "2005", pages = "299--318", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "In this paper, we present a method and a tool to build symbolic labelled transition systems from B specifications. The tool, called GeneSyst, can take into account refinement levels and can visualize the decomposition of abstract states in concrete hierarchical states. The resulting symbolic transition system represents all the behaviors of the initial {B} event system. So, it can be used to reason about them. We illustrate the use of GeneSyst to check security properties on a model of electronic purse. This work was done in the GECCOO project of program {``}ACI : S{\'e}curit{\'e} Informatique{''} supported by the French Ministry of Research and New Technologies. It is also suported by CNRS and ST-Microelectronics by the way of a doctoral grant.", keywords = "Object-Z, tools, GeneSyst", } @InProceedings{ZB05-Badeau, author = "Badeau, Fr{\'e}d{\'e}ric and Amelot, Arnaud", title = "Using {B} as a High Level Programming Language in an Industrial Project: Roissy {VAL}.", booktitle = "ZB05", year = "2005", pages = "334--354", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "In this article we would like to go back on {B} used to design software, by presenting the industrial process established through years by Siemens Transportation Systems on a real project: the VAL shuttle for Roissy Charles de Gaulle airport. In this project, the logical core of an equipment located along the tracks and driving the shuttles is designed with B. By confronting this {B} software development, with the historical context, we show that {B} can be used as a high-level programming language offering the feature of proving properties. We show how this process is used to build, by construction, a large size software with very few design errors ever since its first release, and for a predefined cost.", } @InProceedings{ZB05-Hoang, author = "Hoang, Thai Son and Jin, Zhendong and Robinson, Ken and McIver, Annabelle and Morgan, Carroll", title = "Development via Refinement in {Probabilistic B} - Foundation and Case Study.", booktitle = "ZB05", year = "2005", pages = "355--373", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "In earlier work, we introduced probability to the B by providing a probabilistic choice substitution and by extending Brsquos semantics to incorporate its meaning [8]. This, a first step, allowed probabilistic programs to be written and reasoned about within B. This paper extends the previous work into refinement within B. To allow probabilistic specification and development within B, we must add a probabilistic specification substitution; and we must determine the rules and techniques for its rigorous refinement into probabilistic code. Implementation in {B} frequently contains loops. We generalise the standard proof obligation rules for loops giving a set of rules for reasoning about the correctness of probabilistic loops. We present a small case-study that uses those rules, the randomised Min-Cut algorithm.", keywords = "probability, program correctness, generalised substitutions, weakest preconditions, B-Method, randomised algorithms, refinement, pAMN", } @InProceedings{ZB05-Bouquet, author = "Bouquet, Fabrice and Dadeau, Fr{\'e}d{\'e}ric and Groslambert, Julien", title = "Checking {JML} Specifications with {B} Machines.", booktitle = "ZB05", year = "2005", pages = "434--453", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "This paper presents a solution to the lack of tool-support for the JML models verification. We propose an approach for expressing JML specifications within the {B} abstract machines notation. The {B} machines generated from the JML can then be checked to ensure their correctness. Thus, we deduce the correctness of the original JML specification, ensured by rewriting rules which give the semantical equivalence of the two models. More generally, this translation can be applied to object-oriented specification languages using before-after predicates.", keywords = "JML, object-oriented, B-Method, specifications, AMN", } @InProceedings{ZB05-Rezazadeh, author = "Rezazadeh, Abdolbaghi and Butler, Michael", title = "Some Guidelines for Formal Development of Web-Based Applications in {B}-Method.", booktitle = "ZB05", year = "2005", pages = "472--492", crossref = "ZB05", bibsource = "DBLP, http://dblp.uni-trier.de", abstract = "Web-based applications are the most common form of distributed systems that have gained a lot of attention in the past ten years. Today many of us are relying on scores of mission-critical Web-based systems in different areas such as banking, finance, e-commerce and government. The development process of these systems needs a sound methodology, which ensures quality, consistency and integrity. Formal Methods provide systematic and quantifiable approaches to create coherent systems. Despite this there has been limited work on the formal modelling of Web-based applications. In this paper our aim is to provide researchers with some guidelines based on results from ongoing work to model a Web-based system using the B-Method. Session and state management, developing formal models for complex data types, abstraction of distributed database systems and formal representation of communication links between different components of a web-based system are the main issues that we have examined.", } @InProceedings{Aljer2003, author = "Aljer, Ammar and Devienne, Philippe and Tison, Sophie and Boulanger, Jean-Louis and Mariano, Georges", title = "{BHDL} : Circuits design in {B}", booktitle = "ACSD'03Proceeeding of the Third International Conference Application of Concurrency to System Design", year = "2003", keywords = "BHDL, hardware, codesign", editor = "IEEE Computer Society Press", month = jun, } @Proceedings{ZB05, editor = "Treharne, Helen and King, Steve and Henson, Martin C. and Schneider, Steve", title = "{ZB}'2005: Formal Specification and Development in {Z} and {B}, 4th International Conference of {B} and {Z} Users, Guildford, {UK}, April 13-15, 2005, Proceedings", booktitle = "ZB05", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "3455", year = "2005", ISBN = "3-540-25559-1", bibsource = "DBLP, http://dblp.uni-trier.de", } @InProceedings{Aljer2003b, author = "Aljer, Ammar and Devienne, Philippe and Tison, Sophie and Boulanger, Jean-Louis and Mariano, Georges", title = "{BHDL} : Circuits design in {B}", booktitle = "ACSD'03Proceeeding of the Third International Conference Application of Concurrency to System Design", year = "2003", abstract = "The main goal of this project is to provide a method of correct design of digital circuit. It combines the advantages of VHDL, the well-known language of circuit design, with the power of {B} method that guarantees the correct design (w.r.t. a formal specification). This allows avoiding the design test since it is {``}correct by proven construction{''}. Furthermore, this project provides a tool, called BHDL, with a graphical interface for creating, editing, viewing and proving modular hardware architectures.", keywords = "hardware, BHDL, codesign", editor = "IEEE Computer Society Press", month = jun, } @Unpublished{AbrialDSM, author = "Abrial, Jean-Raymond", title = "Discrete System Models", note = "Internal Notes / summer school", URL = "http://se.inf.ethz.ch/laser/2004/papers/abrial/discrete_system_models.pdf", month = feb, year = "2002", } @Article{J3ea05-boulanger, author = "Boulanger, Jean-louis", title = "Conception s{\^u}r de circuit num{\'e}rique", journal = "J3ea - Journal sur l'enseignement des sciences et technologies de l'information et des syst{\`e}mes", year = "2005", volume = "4", number = "4", annote = "Hors s{\'e}rie - Diagnostic en EEA", month = nov, abstract = "Initialement cette {\'e}tude constituait un simple exercice de style ayant pour objectif d'{\'e}valuer la mod{\'e}lisation de circuits num{\'e}riques simples {\`a} l'aide de la m{\'e}thode {B}. Cette exp{\'e}rimentation {\'e}tait essentiellement motiv{\'e}e par la perception d'une analogie forte entre le domaine cible et les principes de la m{\'e}thode {B}. Les circuits num{\'e}riques sont de plus en plus complexes tant du point de vue de l'int{\'e}gration que du point de vue des fonctions trait{\'e}es. Actuellement, la principale activit{\'e} de validation des circuits num{\'e}riques consiste {\`a} r{\'e}aliser une campagne de test. Il ne nous semble pas {\'e}vident de faire front {\`a} cette complexit{\'e} uniquement au travers d'activit{\'e}s de test. Le but de cet article est de pr{\'e}senter une approche m{\'e}thodologique bas{\'e}e sur le couplage d'une conception $VHDL$ et sur une v{\'e}rification par preuve formelle bas{\'e}e sur la m{\'e}thode {B}.", editor = "EDP sciences", } @Article{TSI22-Dolle, author = "Doll{\'e}, D. and Essam{\'e}, D. and Falampin, J.", title = "{B} dans le transport ferroviaire. {L}'exp{\'e}rience de Siemens", journal = TSI, year = "2003", volume = "22", number = "1", pages = "11--32", } @Article{TSI22-Burdy, author = "Burdy, Lilian and Casset, Ludovic and Requet, Antoine", title = "{D}{\'e}veloppement formel d'un v{\'e}rifieur embarqu{\'e} de byte-code Java", journal = TSI, keywords = "smartcards, JavaCard", year = "2003", volume = "22", number = "1", pages = "33--60", } @Article{TSI22-Potet, author = "Potet, Marie-Laure", title = "Sp{\'e}cificiation et d{\'e}veloppements structur{\'e}s dans la m{\'e}thode {B} - Principes et validation", journal = TSI, year = "2003", volume = "22", number = "1", pages = "61--88", } @Article{TSI22-Abrial, author = "Abrial, Jean-Raymond", title = "{B} : pass{\'e}, pr{\'e}sent, futur", journal = TSI, year = "2003", volume = "22", number = "1", pages = "89--118", } @PhdThesis{Lanet2004, author = "Lanet, Jean-Louis", title = "Produire des logiciels s{\^u}rs", school = "Universit{\'e} de M{\'e}diterran{\'e}e", year = "2004", URL = "http://www.gemplus.fr/smart/rd/publications/", keywords = "JavaCard, smartcards", type = "Th{\`e}se d'habilitation", month = mar, } @Proceedings{ICFEM2005, title = "Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, {ICFEM} 2005", year = "2005", editor = "Lau, Kung-Kiu and Banach, Richard", number = "3785", series = LNCS, address = "Manchester,UK", month = nov, note = "ISBN: 3-540-29797-9", } @InProceedings{ICFEM2005-Idani, author = "Idani, Akram and Ledru, Yves and Bert, Didier", title = "Derivation of {UML} Class Diagrams as Static Views of Formal {B} Developments", abstract = "Although formal methods provide excellent techniques for the precise description of systems, understanding these descriptions is often restricted to experts. This paper investigates a practical solution to assist the understanding of a formal specification, written in B, by providing a complementary view of the specification as {UML} class diagram. Our technique improves the state of the art by taking into account operations in the construction of the diagram, through the use of concept formation techniques. A documentation tool automates the approach. It has been applied to several specifications built independently of the tool.", keywords = "method integration, B-Method, UML, B2UML, formal concept analysis", crossref = "ICFEM2005", pages = "37--51", } @InProceedings{AFADL06-Bodeveix, author = "Bodeveix, Jean-Paul and Filali, Mamoun and Lawall, Julia and Muller, Gilles", title = "{V}{\'e}rification automatique de propri{\'e}t{\'e}s d'ordonnanceurs {Bossa}", crossref = "AFADL06", month = mar, address = "http://www.infres.enst.fr", pages = "95--109", } @InProceedings{AFADL06-Idani, author = "Idani, Akram and Bert, Didier and Ledru, Yves", title = "Analyse formelle de concepts pour la g{\'e}n{\'e}ration de diagrammes de classes {UML} {\`a} partir de sp{\'e}cifications {B}", crossref = "AFADL06", keywords = "B2UML", } @Proceedings{AFADL06, title = "{AFADL}'06", year = "2006", URL = "http://cedric.cnam.fr/AFADL06/", address = "Paris", month = mar, language = "french", publisher = "ENST", organization = "CEDRIC-CNAM", } @InBook{Laleau2006, author = "Laleau, R{\'e}gine and Mammar, Amel", editor = "Frappier, Marc and Habrias, Henri", book = "Software Specification Methods : an Overview Using a Case Study", title = "From {UML} Diagrams to {B} Specifications", publisher = "ISTE London", keywords = "UML2B", year = "2006", } @InProceedings{IFM05-Bostrom, author = "Bostrom, Pontus and Wald{\'e}n, Marina", title = "Development of Fault Tolerant Grid Applications Using Distributed {B}", booktitle = "IFM'2005", year = "2005", pages = "167--186", keywords = "event-B, grid computing, fault tolerance, domain specific languages, language extensions, stepwise development", abstract = "Computational grids have become popular for constructing large scale distributed systems. Grid applications typically run in a very heterogeneous environment and fault tolerance is therefore very important for their correctness. Since the construction of correct distributed systems is difficult with traditional development methods we propose the use of formal methods. We use Event {B} as our formal framework, which we extend with new constructs such as remote procedures and notifications for reasoning about grid systems. The extended language, called Distributed B, ensures that the application can handle both node and network failures. Furthermore, the new constructs in Distributed {B} enable straightforward implementation of the specifications, as well as automatic generation of the needed proof obligations.", crossref = "IFM05", } @InProceedings{IFM05-Okalas, author = "Okalas-Ossami, Dieu Donn{\'e} and Jacquot, Jean-Pierre and Souqui{\`e}res, Jeanine", title = "Consistency in {UML} and {B} multi-view specifications", booktitle = "IFM'2005", year = "2005", pages = "386--405", abstract = "We present the notion of consistency relation in UML and {B} multi-view specifications. It is defined as a semantic relation between both views. It provides us with a sound basis to define the notion of development operator. An operator models a development step; it separates the design decisions from their expression in the specification formalisms. Operator correctness is defined as a property which guarantees that the application of an operator on a consistent specification state yields a consistent new state. An operator can be proven once and for all to be correct. A classical case-study, the Generalized Railroad Crossing (GRC), demonstrates how the different notions can be put in practice to provide specifiers with a realistic development model.", keywords = "consistency, verification, operators, multi-view, UML, B-Method", crossref = "IFM05", } @InProceedings{IFM05-Bodeveix, author = "Bodeveix, Jean-Paul and Filali, Mamoun and Lawall, Julia and Muller, Gilles", title = "Formal methods meet Domain Specific Languages", booktitle = "IFM'2005", year = "2005", pages = "187--206", crossref = "IFM05", abstract = "In this paper, we relate an experiment whose aim is to study how to combine two existing approaches for ensuring software correctness: Domain Specific Languages (DSLs) and formal methods. As examples, we consider the Bossa DSL and the {B} formal method. Bossa is dedicated to the development of process schedulers and has been used in the context of Linux and Chorus. {B} is a refinement based formal method which has especially been used in the domain of railway systems. In this paper, we use {B} to express the correctness of a Bossa specification. Furthermore, we show how {B} can be used as an alternative to the existing Bossa tools for the production of certified schedulers.", keywords = "DSL, scheduling, formal methods, refinement, decision procedure", } @InProceedings{IFM05-Gervais, author = "Gervais, Fr{\'e}d{\'e}ric and Frappier, Marc and Laleau, R{\'e}gine", title = "Synthesizing {B} Specifications from {EB3} Attribute Definitions", booktitle = "IFM'2005", year = "2005", pages = "207--226", crossref = "IFM05", keywords = "information systems, data integrity constraints, attributes, B-Method, EB3, recursive functions, pattern matching", abstract = "$EB^3$ is a trace-based formal language created for the specification of information systems (IS). Attributes, linked to entities and associations of an IS, are computed in $EB^3$ by recursive functions on the valid traces of the system. On the other hand, {B} is a state-based formal language also well adapted for the specification of IS. In this paper, we deal with the synthesis of B specifications that correspond to $EB^3$ attribute definitions, in order to specify and verify safety properties like data integrity constraints. Each action in the $EB^3$ specification is translated into a {B} operation. The substitutions are obtained by an analysis of the CAML-like patterns used in the recursive functions that define the attributes in $EB^3$. Our technique is illustrated by an example of a simple library management system.", } @InProceedings{IFM05-Schneider, author = "Schneider, Steve and Treharne, Helen and Evans, Neil", title = "Chunks: Component Verification in {CSP||B}", booktitle = "IFM'2005", year = "2005", pages = "89--108", keywords = "component based verification, B-Method, CSP, decomposition", abstract = "{CSP||B} is an approach to combining the process algebra {CSP} with the formal development method B, enabling the formal description of systems involving both event-oriented and state-oriented aspects of behaviour. The approach provides architectures which enable the application of {CSP} verification tools and {B} verification tools to the appropriate parts of the overall description. Previous work has considered how large descriptions can be verified using coarse grained component parts. This paper presents a generalisation of that work so that {CSP||B} descriptions can be decomposed into finer grained components, chunks, which focus on demonstrating the absence of particular divergent behaviour separately. The theory underpinning chunks is applicable not only to {CSP||B} specification but to {CSP} specifications. This makes it an attractive technique to decomposing large systems for analysing with {FDR}.", } @Proceedings{IFM05, title = "Fifth International Conference on Integrated Formal Methods", year = "2005", number = "3771", series = LNCS, address = "Eindhoven, The Netherlands", month = nov, ISBN = "978-3-540-30492-0", publisher = "Springer Berlin / Heidelberg", } @InProceedings{IFM04-Lano, author = "Lano, K. and Clark, D. and Androutsopoulos, K.", title = "{UML} to {B}: Formal Verification of Object-Oriented Models", crossref = "IFM04", booktitle = "IFM'2004", pages = "187--206", keywords = "UML, B-Method, UML-RSDS, graphical specifications, UML2B", abstract = "The integration of {UML} and formal methods such as {B} and SMV provides a bridge between graphical specification techniques usable by mainstream software engineers, and precise analysis and verification techniques, essential for the development of high integrity and critical systems. In this paper we define a translation from {UML} class diagrams into B, which is used to verify the consistency of {UML} models and to verify that expected properties of these models hold.", } @Proceedings{IFM04, title = "Fourth International Conference on Integrated Formal Methods", year = "2004", number = "2999", series = LNCS, address = "Canterbury, Kent, England", month = apr, ISBN = "978-3-540-21377-2", publisher = "Springer Berlin / Heidelberg", } @InProceedings{SAC06-Fekih, author = "Fekih, Houda and Jemni Ben Ayed, Leila and Merz, Stephan", title = "Transformation of {B} Specifications into {UML} Class Diagrams and State Machines", keywords = "B2UML, UML, refinement, class diagram, state machine", booktitle = "21st Annual ACM Symposium on Applied Computing - SAC 2006", pages = "1840--1844", year = "2006", volume = "2", address = "Dijon, France", month = apr, } @InProceedings{VoisinetTJ05, author = "Voisinet, Jean-Christophe and Tatibou{\"e}t, Bruno and Jacques, Isabelle", title = "Generation of {OCL} Constraints from {B} Abstract Machines.", booktitle = "Software Engineering Research and Practice", year = "2005", pages = "260--266", bibsource = "DBLP, http://dblp.uni-trier.de", keywords = "OCL, UML, B2UML", } @InProceedings{ENTCS-Idani, author = "Idani, Akram and Ledru, Yves", title = "Object Oriented Concepts Identification from Formal {B} Specifications", keywords = "B-Method, UML, B2UML", booktitle = ENTCS, pages = "159--174", year = "2005", volume = "133", publisher = "Elsevier", note = "sciencedirect.com", } @PhdThesis{HDR-Potet, author = "Potet, Marie-Laure", title = "Sp{\'e}cifications et d{\'e}veloppements formels : Etude des aspects compositionnels dans la m{\'e}thode {B}", school = "LSR-IMAG", year = "2002", keywords = "software formal development, modularity, B-Method, compositional verification", URL = "http://tel.ccsd.cnrs.fr/tel-00004580/en/", abstract = "{\`A} ce jour, les m{\'e}thodes formelles ont montr{\'e} qu'elles {\'e}taient applicables avec succ{\`e}s au d{\'e}veloppement de logiciels industriels. Pour ma\^{\i}triser la complexit{\'e} croissante de ces applications, la mise en {\oe}uvre des paradigmes d'abstraction et de composition est incontournable. La m{\'e}thode {B} permet d'assister le processus de d{\'e}veloppement des sp{\'e}cifications au code et offre une notion de modularit{\'e} qui permet de composer {\`a} la fois les sp{\'e}cifications et les d{\'e}veloppements. La compositionnalit{\'e} des preuves est assur{\'e}e par des restrictions impos{\'e}es par le langage, qui limitent les formes d'architectures autoris{\'e}es. A la suite de nos pr{\'e}c{\'e}dents travaux, le manuscrit pr{\'e}sent{\'e} ici explicite les principes de composition des sp{\'e}cifications et des d{\'e}veloppements, {\'e}nonce les th{\'e}or{\`e}mes sous-jacents {\`a} la composition des preuves et compl{\`e}te et valide les restrictions impos{\'e}es par la m{\'e}thode B. Bien que d{\'e}di{\'e}s {\`a} la m{\'e}thode B, les r{\'e}sultats pr{\'e}sent{\'e}s sont plus g{\'e}n{\'e}raux : ils peuvent s'appliquer {\`a} d'autres approches formelles bas{\'e}es sur la notion d'{\'e}tat, comme les approches objet.", type = "Th{\`e}se d'habilitation", } @Proceedings{B07, editor = "Julliand, Jacques and Kouchnarenko, Olga", title = "{B} 2007: Formal Specification and Development in {B}, 7th International Conference of {B} Users, Besan{\c{c}}on, France, January 17-19, 2007, Proceedings", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "4355", year = "2006", ISSN = "0302-9743", ISBN = "978-3-540-68760-3", bibsource = "DBLP, http://dblp.uni-trier.de", } @InProceedings{B07-Jaffuel, author = "Jaffuel, Eddie", title = "Using {B} Machines for Model-Based Testing of Smartcard Software.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "2", doi = "http://dx.doi.org/10.1007/11955757_2", crossref = "B07", keywords = "testing, tool, test generation, smartcards", abstract = "Automated test generation from {B} abstract machines is commonly used in the smart card industry since 2003. Several domains are concerned such as mobile communication applications (e.g. SIM cards) [1], identity applications (e.g. health cards or identity cards) and banking applications. The model-based testing tool LTG (LEIRIOS Test Generator) [2] makes it possible to generate executable test scripts from a {B} formal model of the functional requirements. Therefore, the design of the test cases and the development of the test scripts are based on a modeling and automated test generation approach. The model-based testing process is structured in 3 main steps: Model. The first step consists in developing a behavior model using the B abstract machine notation. The model represents the expected behavior of the smart card application under test. Configure test generation. The configuration of the test generation with LTG is based on model coverage criteria. Three families of criteria give a precise control over the test generation: decision coverage, operation effect coverage and data coverage. Adapt. The generated test cases are then translated in executable test scripts using an adaptor customized for the test execution environment and the project. This talk show how {B} abstract machines are developed in the context of model-based testing of smart card applications, how model coverage criteria makes it possible to generate accurate test cases and how those test cases are adapted into executable test scripts for a targeted test execution environment.", } @InProceedings{B07-Chemouil, author = "Chemouil, David", title = "The Design of Spacecraft On-Board Software.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "3", doi = "http://dx.doi.org/10.1007/11955757_3", abstract = "This presentation deals with the way Space Systems and particularly Spacecraft On-Board Software are designed. I will try to show how the design of Space Systems is undergoing a shift from a seasoned-expert craft to a methodology based upon modelling. First, I will introduce Space Systems by presenting their applications and architecture. Then I will detail the design of such systems, insisting on systems and software aspects. Finally, I will describe some directions currently followed by CNES regarding modelling technologies. Among them, I will bring the notion of pre-proven business-specific refinement patterns to the forefront, as a possible (partial) solution to the reluctance to proof-based development methods in industry. David Chemouil works in the On-Board Software Office at the French Space Agency (CNES) in Toulouse. His activities include monitoring the development of On-Board Software contracted by CNES and carrying out R\&D on Embedded Software Engineering. David Chemouil holds a PhD in Computer Science from Universit{\'e} Paul Sabatier, Toulouse (2004).", crossref = "B07", } @InProceedings{B07-Boulme, author = "Boulm{\'e}, Sylvain and Potet, Marie-Laure", title = "Interpreting Invariant Composition in the {B} Method Using the Spec\# Ownership Relation: {A} Way to Explain and Relax {B} Restrictions.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "4--18", doi = "http://dx.doi.org/10.1007/11955757_4", crossref = "B07", abstract = "In the B method, the invariant of a component cannot be violated outside its own operations. This approach has a great advantage: the users of a component can assume its invariant without having to prove it. But, B users must deal with important architecture restrictions that ensure the soundness of reasonings involving invariants. Moreover, understanding how these restrictions ensure soundness is not trivial. This paper studies a meta-model of invariant composition, inspired from the Spec{\#} approach. Basically, in this model, invariant violations are monitored using ghost variables. The consistency of assumptions about invariants is controlled by very simple proof obligations. Hence, this model provides a simple framework to understand B composition rules and to study some conservative extensions of B authorizing more architectures and providing more control on components initialization.", } @InProceedings{B07-Dunne, author = "Dunne, Steve", title = "Chorus Angelorum.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "19--33", doi = "http://dx.doi.org/10.1007/11955757_5", crossref = "B07", } @InProceedings{B07-Ifill, author = "Ifill, Wilson and Schneider, Steve A. and Treharne, Helen", title = "Augmenting {B} with Control Annotations.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "34--48", doi = "http://dx.doi.org/10.1007/11955757_6", crossref = "B07", abstract = "CSP||B is an integration of the process algebra Communicating Sequential Processes (CSP), and the B-Method, which enables consistent controllers to be written for B machines in a verifiable way. Controllers are consistent if they call operations only when they are enabled. Previous work has established a way of verifying consistency between controllers and machines by translating control flow to AMN and showing that a control loop invariant is preserved. This paper offers an alternative approach, which allows fragments of control flow expressed as annotations to be associated with machine operations. This enables designers' understanding about local relationships between successive operations to be captured at the point the operations are written, and used later when the controller is developed. Annotations provide a bridge between controllers and machines, expressing the relevant aspects of control flow so that controllers can be verified simply by reference to the annotations without the need to consider the details of the machine operations. This paper presents the approach through two instances of annotations with their associated control languages, covering recursion, prefixing, choice, and interrupt.", } @InProceedings{B07-Hallerstede, author = "Hallerstede, Stefan", title = "Justifications for the Event-{B} Modelling Notation.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "49--63", keywords = "event-B", doi = "http://dx.doi.org/10.1007/11955757_7", crossref = "B07", abstract = "Event-B is a notation and method for discrete systems modelling by refinement. The notation has been carefully designed to be simple and easily teachable. The simplicity of the notation takes also into account the support by a modelling tool. This is important because Event-B is intended to be used to create complex models. Without appropriate tool support this would not be possible. This article presents justifications and explanations for the choices that have been made when designing the Event-B notation.", } @InProceedings{B07-Yang, author = "Yang, Letu and Poppleton, Michael", title = "Automatic Translation from Combined {B} and {CSP} Specification to Java Programs.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "64--78", doi = "http://dx.doi.org/10.1007/11955757_8", crossref = "B07", abstract = "A recent contribution to the formal specification and verification of concurrent systems is the integration of the state- and event-based approaches B and CSP, specifically in the ProB model checking tool. At the implementation end of the development, concurrent programming in Java remains a demanding and error-prone activity, because of the need to verify critical properties of safety and liveness as well as functional correctness. This work contributes to the automated development of concurrent Java programs from such integrated specifications. The JCSP package was originally designed as a proven clean Java concurrency vehicle for the implementation of certain CSP specifications. In the context of best current Java concurrent programming practice, we extend the original JCSP package to support the integrated B and CSP specification by implementing new channel classes. We propose rules for the automated translation of the integrated specification to multi-threaded Java using the extended JCSP channel classes. We briefly present a prototype translation tool which extends ProB, with a worked example, and conclude with a strategy for formally verifying the translation.", } @InProceedings{B07-Leuschel, author = "Leuschel, Michael and Butler, Michael and Spermann, Corinna and Turner, Edd", title = "Symmetry Reduction for {B} by Permutation Flooding.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "79--93", doi = "http://dx.doi.org/10.1007/11955757_9", crossref = "B07", keywords = "tool support, model-checking, symmetry reduction", abstract = "Symmetry reduction is an established method for limiting the amount of states that have to be checked during exhaustive model checking. The idea is to only verify a single representative of every class of symmetric states. However, computing this representative can be non-trivial, especially for a language such as B with its involved data structures and operations. In this paper, we propose an alternate approach, called permutation flooding. It works by computing permutations of newly encountered states, and adding them to the state space. This turns out to be relatively unproblematic for B's data structures and we have implemented the algorithm inside the ProB model checker. Empirical results confirm that this approach is effective in practice; speedups exceed an order of magnitude in some cases. The paper also contains correctness results of permutation flooding, which should also be applicable for classical symmetry reduction in B.", } @InProceedings{B07-Bouquet, author = "Bouquet, Fabrice and Couchot, Jean-Francois and Dadeau, Fr{\'e}d{\'e}ric and Giorgetti, Alain", title = "Instantiation of Parameterized Data Structures for Model-Based Testing.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "94--108", doi = "http://dx.doi.org/10.1007/11955757_10", crossref = "B07", abstract = "", } @InProceedings{B07-Groslambert, author = "Groslambert, Julien", title = "Verification of {LTL} on {B} Event Systems.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "109--124", doi = "http://dx.doi.org/10.1007/11955757_11", crossref = "B07", abstract = "This paper proposes a way to verify temporal properties expressed in LTL (Linear Temporal Logic) on B Event Systems. The method consists in generating a B representation of the B{\"u}chi automaton associated with the LTL property to verify. We establish the consistency of the generated event system implies the satisfaction of the LTL property on the executions of the original event system. We also characterize the subset of LTL preserved by the B refinement and we propose another refinement relation, with necessary and sufficient condition for preserving any given LTL property.", keywords = "LTL, Buchi automata, verification, refinement", } @InProceedings{B07-Chan, author = "Chan, Edward and Robinson, Ken and Welch, Brett", title = "Patterns for {B}: Bridging Formal and Informal Development.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "125--139", doi = "http://dx.doi.org/10.1007/11955757_12", crossref = "B07", abstract = "Patterns capture the shape of particular specifications, providing starting points for developers. The most well known design patterns in software are those of the Gang of Four (GoF), Gamma, Helm, Johnson {\&} Vlissides[4], who have provided a set of patterns for Object-Oriented development. Starting with these patterns as a motivation, this paper discusses various issues concerning the concept of patterns for the B Method (B) and explores a number of patterns that could be used with B. The paper presents a number of case studies to illustrate use of the patterns, and discusses future exploration of design patterns for B. A motivation for the development of patterns for B is to enable reuse and also to make B more accessible to developers from the more informal side of software development.", keywords = "design patterns, formal development, classes, objects", } @InProceedings{B07-Cansell, author = "Cansell, Dominique and M{\'e}ry, Dominique and Rehm, Joris", title = "Time Constraint Patterns for Event {B} Development.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "140--154", doi = "http://dx.doi.org/10.1007/11955757_13", crossref = "B07", } @InProceedings{B07-Stoddart, author = "Stoddart, Bill and Cansell, Dominique and Zeyda, Frank", title = "Modelling and Proof Analysis of Interrupt Driven Scheduling.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "155--170", doi = "http://dx.doi.org/10.1007/11955757_14", crossref = "B07", } @InProceedings{B07-Snook, author = "Snook, Colin and Wald{\'e}n, Marina", title = "Refinement of Statemachines Using Event {B} Semantics.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "171--185", doi = "http://dx.doi.org/10.1007/11955757_15", crossref = "B07", } @InProceedings{B07-Bostrom, author = "Bostr{\"o}m, Pontus and Neovius, Mats and Oliver, Ian and Wald{\'e}n, Marina", title = "Formal Transformation of Platform Independent Models into Platform Specific Models.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "186--200", doi = "http://dx.doi.org/10.1007/11955757_16", crossref = "B07", } @InProceedings{B07-Gervais, author = "Gervais, Fr{\'e}d{\'e}ric and Frappier, Marc and Laleau, R{\'e}gine", title = "Refinement of {EB3} Process Patterns into {B} Specifications.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "201--215", doi = "http://dx.doi.org/10.1007/11955757_17", crossref = "B07", } @InProceedings{B07-Stouls, author = "Stouls, Nicolas and Potet, Marie-Laure", title = "Security Policy Enforcement Through Refinement Process.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "216--231", doi = "http://dx.doi.org/10.1007/11955757_18", crossref = "B07", } @InProceedings{B07-Benaissa, author = "Bena{\"\i}ssa, Nazim and Cansell, Dominique and M{\'e}ry, Dominique", title = "Integration of Security Policy into System Modeling.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "232--247", doi = "http://dx.doi.org/10.1007/11955757_19", crossref = "B07", } @InProceedings{B07-Oliver, author = "Oliver, Ian", title = "Experiences in Using {B} and {UML} in Industrial Development.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "248--251", doi = "http://dx.doi.org/10.1007/11955757_20", crossref = "B07", } @InProceedings{B07-Essame, author = "Essam{\'e}, Didier and Doll{\'e}, Daniel", title = "{B} in Large-Scale Projects: The Canarsie Line {CBTC} Experience.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "252--254", doi = "http://dx.doi.org/10.1007/11955757_21", crossref = "B07", } @InProceedings{B07-Clabaut, author = "Clabaut, Mathieu", title = "A Tool for Firewall Administration.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "255--256", doi = "http://dx.doi.org/10.1007/11955757_22", crossref = "B07", } @InProceedings{B07-Hoffmann, author = "Hoffmann, Sarah and Haugou, Germain and Gabriele, Sophie and Burdy, Lilian", title = "The {B}-Method for the Construction of Microkernel-Based Systems.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "257--259", doi = "http://dx.doi.org/10.1007/11955757_23", crossref = "B07", } @InProceedings{B07-Evans, author = "Evans, Neil and Ifill, Wilson", title = "Hardware Verification and Beyond: Using {B} at {AWE}.", booktitle = "The 7th International {B} Conference", year = "2007", pages = "260--261", doi = "http://dx.doi.org/10.1007/11955757_24", crossref = "B07", } @InProceedings{B07-Bendisposto-b, author = "Bendisposto, Jens and Leuschel, Michael", title = "A Generic Flash-Based Animation Engine for {ProB}.", booktitle = "The 7th International {B} Conference", year = "2007", keywords = "tools", pages = "266--269", doi = "http://dx.doi.org/10.1007/11955757_26", crossref = "B07", } @InProceedings{B07-Bendisposto, author = "Bendisposto, Jens and Leuschel, Michael", title = "{BE4}: The {B} Extensible Eclipse Editing Environment.", booktitle = "The 7th International {B} Conference", keywords = "tools, ProB, BE4", abstract = "The open-source {Eclipse} platform has become hugely popular as an integrated development environment for Java, and a considerable number of plug-ins have been developed for other programming languages (e.g., C++,PHP, Eiffel, Python, Fortran, etc.). In this paper we present a new plug-in for Eclipse, supporting the {B-method} and {B}'s abstract machine notation ({AMN}). In addition to providing editing and syntax highlighting, the plug-in displays syntax and structural errors in the {B} source code, as well as suggesting fixes for those errors.", URL = "http://www.stups.uni-duesseldorf.de/publications/be4.pdf", year = "2007", pages = "270--273", doi = "http://dx.doi.org/10.1007/11955757_27", crossref = "B07", } @InProceedings{B07-Servat, author = "Servat, Thierry", title = "{BRAMA}: {A} New Graphic Animation Tool for {B} Models.", booktitle = "The 7th International {B} Conference", keywords = "tools", year = "2007", pages = "274--276", doi = "http://dx.doi.org/10.1007/11955757_28", crossref = "B07", } @InProceedings{B07-Jaffuell, author = "Jaffuel, Eddie and Legeard, Bruno", title = "{LEIRIOS} Test Generator: Automated Test Generation from {B} Models.", booktitle = "The 7th International {B} Conference", keywords = "tools", year = "2007", pages = "277--280", doi = "http://dx.doi.org/10.1007/11955757_29", crossref = "B07", } @InProceedings{B07-Haddad, author = "Haddad, Amal", title = "Meca: {A} Tool for Access Control Models.", booktitle = "The 7th International {B} Conference", keywords = "tools", year = "2007", pages = "281--284", doi = "http://dx.doi.org/10.1007/11955757_30", crossref = "B07", } @InProceedings{B07-Bouquet-b, author = "Bouquet, Fabrice and Dadeau, Fr{\'e}d{\'e}ric and Groslambert, Julien", title = "{JML2B}: Checking {JML} Specifications with {B} Machines.", booktitle = "The 7th International {B} Conference", keywords = "tools, JML2B", year = "2007", pages = "285--288", doi = "http://dx.doi.org/10.1007/11955757_31", crossref = "B07", abstract = "This paper introduces a tool, named JML2B, destined to check the consistency of JML specifications. JML2B is a solution to the lack of tool-support for the JML models verification. Our tool translates JML specifications into the B abstract machines notation. The generated B machines can then be checked to ensure their correctness. When the proof fails, it is possible to retrieve the mistakes in the original JML specification.", } @PhdThesis{Okalas-PhD, author = "Okalas-Ossami, Dieudonn{\'e}", title = "{Construction Simultan{\'e}e de Sp{\'e}cifications Multi-Vues {UML} et B}", school = "LORIA-Universit{\'e} Nancy2", keywords = "UML2B, B2UML", month = oct, year = "2006", } @PhdThesis{Thuan-PhD, author = "Thuan, N.", title = "{Utilisation de {B} pour la v{\'e}rification de sp{\'e}cifications {UML} et le d{\'e}veloppement formel orient{\'e} objet}", school = "LORIA -Universit\'e Nancy2", URL = "http://tel.archives-ouvertes.fr/tel-00080852/en/", keywords = "UML2B", abstract = "The coupling of object-oriented approaches with the {B} method makes improvement the activities of software specification and development. The {B} method provides notations for the specification and powerful tools, allowing to specify and verify models. The object-oriented approaches provide interesting mechanisms for the structuring and the development of large systems. The contribution of this thesis deals with the activities of coupling between these two formalisms by using the {B} provers to validate and verify {UML} specifications. By extending the derivation of {UML} to {B} of preceding works realised in the Dedale research group, we propose an approach of the derivation to {B} of the {UML} meta-models, the static diagrams and the dynamic diagrams. The aim of this proposition is to check semantics and coherence between different diagrams of {UML} specification. Our thesis brings also a contribution to the development of objects oriented specifications using B. The first proposition concerns the taking into account some types of association between classes during the derivation to {B}. The second relates the validation of object-oriented specifications described by {UML2.0} sequence diagrams.", year = "2006", } @Article{Sorensen2001, author = "Sorensen, Ib and Neilson, David", title = "{B}: towards zero defect software", book = "High integrity software", year = "2001", ISBN = "0-7923-7949-7", pages = "23--42", publisher = "Kluwer Academic Publishers", address = "Norwell, MA, USA", } @PhdThesis{Gervais-PhD, author = "Gervais, Fr{\'e}d{\'e}ric", title = "Combinaison de sp{\'e}cifications formelles pour la mod{\'e}lisation des syst{\`e}mes d'information", school = "Conservatoire national des arts et metiers - CNAM Universit{\'e} de Sherbrooke", year = "2006", URL = "http://tel.archives-ouvertes.fr/tel-00121006", month = dec, abstract = "Our aim is to use only formal notations and techniques to specify information systems (IS), contrary to current methodologies that are based on semi-formal notations. On one hand, {EB3} is a trace-based formal language specially created for the specification of such systems. On the other hand, {B} is a state-based formal language well adapted for the specification of IS static properties. A new approach called {EB4} has been defined to integrate both {EB3} and B. Process expressions described in {EB3} are first used to represent the behaviour of the system. Then, the specification is translated into {B} in order to specify the main static properties. For the implementation, a set of translation rules has been defined to automatically synthesize relational database transactions from the data model described in {EB3}.", } @InProceedings{JFLA04-Rocheteau, author = "Rocheteau, J{\'e}r{\^o}me and Colin, Samuel and Mariano, Georges and Poirriez, Vincent", title = "\'Evaluation de l'extensibilit{\'e} de Pho{X}: {B/PhoX} un assistant de preuves pour {B}", booktitle = "Journ\'ees Francophones des Langages Applicatifs (JFLA 2004)", pages = "37--54", year = "2004", editor = "M{\'e}nissier-Morain, Val{\'e}rie", URL = "http://jfla.inria.fr/2004/actes/PS/10-rocheteau.ps", keywords = "B-Method, interactive prover, PhoX, BPhoX, BRILLANT", publisher = "INRIA", } @InProceedings{FDL06-Oliver, author = "Oliver, Ian", title = "A Demonstration of Specifying and Synthesising Hardware using {B} and Bluespec", booktitle = "Forum on Specification and Design Languages", year = "2006", keywords = "BHDL, bluespec, hardware, codesign", URL = "http://rodin.cs.ncl.ac.uk/Publications/", address = "Darmstadt", month = sep, organization = "European Electronic Chips \& Systems design Initiative", } @InProceedings{MOSIM06-Mosbahi, author = "Mosbahi, O. and Jemni Ben Ayed, L.", title = "Utilisation conjointe de {B} {\'e}v{\'e}nementiel et la logique temporelle {TLA+} pour la mod{\'e}lisation et la v{\'e}rification de syst{\`e}mes r{\'e}actifs", booktitle = "6{\`e}me Conf{\'e}rence Francophone de Mod{\'e}lisation et Simulation Mod{\'e}lisation, Optimisation et Simulation des Syst{\`e}mes", year = "2006", address = "Rabat, Maroc", keywords = "TLA+, event-B", URL = "http://www.isima.fr/mosim06/actes/articles/12-modelisation%20et%20verification%20des%20systemes%20reactifs/255.pdf", month = apr, } @InProceedings{MOSIM06-Fadil, author = "Fadil, H. and Koning, Jean-Luc", title = "Vers une sp{\'e}cification formelle des protocoles d'interaction des syst{\`e}mes multi-agents en {B}", booktitle = "6{\`e}me Conf{\'e}rence Francophone de Mod{\'e}lisation et Simulation Mod{\'e}lisation, Optimisation et Simulation des Syst{\`e}mes", year = "2006", address = "Rabat, Maroc", keywords = "multi-agents, protocol", URL = "http://www.isima.fr/mosim06/actes/articles/7-systemes%20multiagents/125.pdf", month = apr, } @InProceedings{CPA07-Ifill, author = "Ifill, Wilson and Schneider, Steve", title = "A Step Towards Refining and Translating {B} Control Annotations to {Handel-C}", crossref = "CPA07", booktitle = "Communication Process Architecture 2007", keywords = "Handel-C, codesign, CSP, ProB", abstract = "Research augmenting {B} machines presented at B2007 has demonstrated how fragments of control flow expressed as annotations can be added to associated machine operations, and shown to be consistent. This enables designers understanding about local relationships between successive operations to be captured at the point the operations are written, and used later when the controller is developed. This paper introduces several new annotations and I/O into the framework to take advantage of hardware s parallelism and to facilitate refinement and translation. To support the new annotations additional {CSP} control operations are added to the control language that now includes: recursion, prefixing, external choice, if-then-else, and sequencing. We informally sketch out a translation to {Handel-C} for prototyping.", } @InProceedings{CPA07-McEwan, author = "McEwan, Alistair A. and Schneider, Steve", title = "Modeling and Analysis of the {AMBA} Bus Using {CSP} and {B}", crossref = "CPA07", booktitle = "Communication Process Architecture 2007", keywords = "CSP, codesign, AMBA, ProB", abstract = "In this paper, we present a formal model and analysis of the AMBA Advanced High-performance Bus (AHB) on-chip bus. The model is given in CSPkB an integration of the process algebra {CSP} and the state-based formalism B. We describe the theory behind the integration of {CSP} and B. We demonstrate how the model is developed from the informal ARM specification of the bus. Analysis is performed using the model-checker ProB. The contribution of this paper may be summarised as follows: presentation of work in progress towards a formal model of the AMBA AHB protocol such that it may be used for inclusion in, and analysis of, co-design systems incorporating the bus, an evaluation of the integration of {CSP} and {B} in the production of such a model, and a demonstration and evaluation of the ProB tool in performing this analysis. The work in this paper was carried out under the Future Technologies for Systems Design Project at the University of Surrey, sponsored by AWE.", } @InProceedings{CPA07-Grant, author = "Grant, Neil and Evans, Neil", title = "Towards the Formal Verification of a Java Processor in Event-{B}", crossref = "CPA07", booktitle = "Communication Process Architecture 2007", keywords = "Java, codesign, event-B, hardware", abstract = "Formal verification is becoming more and more important in the production of high integrity microprocessors. The general purpose formal method called {Event-B} is the latest incarnation of the {B} Method: it is a proof-based approach with a formal notation and refinement technique for modelling and verifying systems. Refinement enables implementation-level features to be proven correct with respect to an abstract specification of the system. In this paper we demonstrate an initial attempt to model and verify Sandia National Laboratories Score processor using {Event-B}. The processor is an (almost complete) implementation of a {Java Virtual Machine} in hardware. Thus, refinement-based verification of the Score processor begins with a formal speci- fication of Java bytecode. Traditionally, {B} has been directed at the formal development of software systems. The use of {B} in hardware verification could provide a means of developing combined software/hardware systems, i.e. codesign", } @InProceedings{CPA07-Yang, author = "Yang, Letu and Poppleton, Michael R.", title = "{JCSProB}: Implementing Integrated Formal Specifications in Concurrent Java", crossref = "CPA07", URL = "http://eprints.ecs.soton.ac.uk/14300/", booktitle = "Communication Process Architecture 2007", keywords = "Java, ProB, tools, model-checking, CSP", abstract = "The {ProB} model checker provides tool support for an integrated formal specification approach, combining the classical state-based B language with the eventbased process algebra CSP. In this paper, we present a developing strategy for implementing such a combined {Prob} specification as a concurrent Java program. A Java implementation of the combined B and CSP model has been developed using a similar approach to {JCSP}. A set of translation rules relates the formal model to its Java implementation, and we also provide a translation tool {JCSProB} to automatically generate a Java program from a {Prob} specification. To demonstrate and exercise the tool, several {B/CSP} models, varying both in syntactic structure and behavioural/concurrency properties, are translated by the tool. The models manifest the presence and absence of various safety, deadlock, and bounded fairness properties; the generated Java code is shown to faithfully reproduce them. Run-time safety and bounded fairness checking is also demonstrated. The Java programs are discussed to demonstrate our implementation of the abstract {B/CSP} concurrencymodel in Java. In conclusion we consider the effectiveness and generality of the implementation strategy.", } @Proceedings{CPA07, title = "Communication Process Architecture 2007", year = "2007", address = "Guildford, Surrey, U.K", month = jul, organization = "Department of Computing at University of Surrey", } @Book{UMLB, editor = "Mermet, Jean P.", title = "{UML-B} Specification for Proven Embedded Systems Design", publisher = "Kluwer Academic Publishers", year = "2004", series = "ChDL", } @InBook{UMLB-Kronlof, author = "Kronlof, Klaus and Oliver, Ian", editor = "Mermet, Jean P.", book = "{UML-B} Specification for Proven Embedded Systems Design", title = "{Formally Unified System Specification Environment with UML, B and SystemC.}", chapter = "2", publisher = "Kluwer Academic Publishers", year = "2004", keywords = "B-Method, UML2B, SystemC, model-checking, hardware, BHDL, PUSSEE", pages = "21--36", } @InBook{UMLB-Voros, author = "Voros, Nikolaos S. and Snook, Colin and Hallerstede, Stefan and Lecomte, Thierry", editor = "Mermet, Jean P.", book = "{UML-B} Specification for Proven Embedded Systems Design", title = "{Embedded System Design Using the PUSSEE Method}", chapter = "3", publisher = "Kluwer Academic Publishers", year = "2004", keywords = "B-Method, UML2B, SystemC, model-checking, hardware, BHDL, PUSSEE", pages = "37--51", } @Article{Gomes2007, author = "Gomes, Bruno Emerson Gurgel and Moreira, Anamaria Martins and D{\'e}harbe, David", title = "Developing Java Card Applications with {B}", journal = ENTCS, volume = "184", year = "2007", ISSN = "1571-0661", pages = "81--96", doi = "http://dx.doi.org/10.1016/j.entcs.2007.03.016", publisher = "Elsevier Science Publishers B. V.", address = "Amsterdam, The Netherlands", keywords = "JavaCard, smartcards", } @InProceedings{LPAR07-Jaeger, author = "Jaeger, {\'E}ric and Dubois, Catherine", title = "Why Would You Trust {B} ?", booktitle = "LPAR, 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning", year = "2007", pages = "288--302", doi = "http://dx.doi.org/10.1007/978-3-540-75560-9_22", bibsource = "DBLP, http://dblp.uni-trier.de", URL = "http://www-spi.lip6.fr/~jaume/ssurf.html", keywords = "proof assistant, Coq, deep embedding, tools, BiCOQ", abstract = "The use of formal methods provides confidence in the correctness of developments. Yet one may argue about the actual level of confidence obtained when the method itself -- or its implementation -- is not formally checked. We address this question for the {B}, a widely used formal method that allows for the derivation of correct programs from specifications. Through a deep embedding of the {B} logic in Coq, we check the {B} theory but also implement {B} tools. Both aspects are illustrated by the description of a proved prover for the {B} logic.", } @PhdThesis{Stouls-Phd, author = "Stouls, Nicolas", title = "Syst{\`e}mes de transitions symboliques et hi{\'e}rarchiques pour la conception et la validation de mod{\`e}les {B} raffin{\'e}s", school = "Institut Polytechnique de Grenoble", year = "2007", abstract = "Cette th{\`e}se propose une approche d'aide {\`a} la conception et au d{\'e}veloppement de mod{\`e}les formels B. Cette approche se base sur la construction d'un syst{\`e}me de transitions symboliques d{\'e}crivant les comportements du mod{\`e}le. Cette seconde vue est compl{\'e}mentaire avec la description orient{\'e}e donn{\'e}es du mod{\`e}le B et peut {\^e}tre utilis{\'e}e pour le d{\'e}crire, le documenter ou le valider. Le syst{\`e}me de transitions est {\'e}labor{\'e} {\`a} partir d'un espace d'{\'e}tats fourni par l'utilisateur et les transitions sont construites par r{\'e}solution d'obligations de preuve. Nous proposons {\'e}galement de prendre en compte le processus de raffinement B en introduisant la notion de hi{\'e}rarchie dans les syst{\`e}mes de transitions. Cette repr{\'e}sentation permet de mettre en {\'e}vidence le lien entre les donn{\'e}es des diff{\'e}rents niveaux de raffinement. De plus, la m{\'e}thode que nous proposons se base sur la d{\'e}composition des {\'e}tats d'une repr{\'e}sentation du mod{\`e}le abstrait, permettant ainsi de conserver la structure g{\'e}n{\'e}rale du syst{\`e}me. Enfin, nous terminons ce manuscrit en d{\'e}crivant l'outil G{\'e}n{\'e}Syst qui implante cette m{\'e}thode, ainsi que son utilisation dans le cadre du projet GECCOO, pour la v{\'e}rification de propri{\'e}t{\'e}s de s{\'e}curit{\'e}.", keywords = "B-Method, transition systems, refinement, vues, development aid, validation", pdf = "http://www.lri.fr/~stoulsn/Productions/These/These.pdf", ps = "http://www.lri.fr/~stoulsn/Productions/These/These.ps.gz", month = dec, } @InProceedings{ICFEM97-Habrias, title = "Formal Specification of Dynamic Constraints with the {B} Method", author = "Henri Habrias and B. Griech", year = "1997", bibdate = "Mon Jan 7 10:00:00 CET 2002", bibsource = "DBLP, http://dblp.uni-trier.de/db/conf/icfem/icfem1997.html#HabriasG97", booktitle = "ICFEM'97", pages = "304--314", } @Article{FMSD98-Walden, author = "M. Wald{\'e}n and K. Sere", title = "Reasoning about Action Systems using the {B}-Method", journal = "Formal Methods in System Design: An International Journal", publisher = "Kluwer Academic Publishers", publaddr = "", ISSN = "0925-9856", year = "1998", volume = "13", number = "1", month = may, pages = "5--35", keywords = "Action systems", } @PhdThesis{Peureux2002-Phd, author = "Fabiena Peureux", title = "{G}{\'e}n{\'e}ration de tests aux limites {\`a} partir de sp{\'e}cifications {B} en Programmation Logique avec Contraintes Ensemblistes", school = "UFR Sciences et techniques de l'Universit{\'e} de Franche-Comt{\'e}", year = "2002", URL = "http://www-lsr.imag.fr/b/Documents/Theses/thesePeureux.ps.gz", } @InProceedings{Chouali2006, author = "Samir Chouali and Maritta Heiselb and Jeanine Souqui{\`e}res", title = "Proving Component Interoperability with {B} Refinement", booktitle = "Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005)", keywords = "Component interoperability; B method", abstract = "We use the formal method {B} for specifying interfaces of software components. Each component interface is equipped with a suitable data model defining all types occurring in the signature of interface operations. Moreover, pre- and postconditions have to be given for all interface operations. The interoperability between two components is proved by using a refinement relation between an adaptation of the interface specifications.", pages = "157--172", year = "2006", number = "160", series = "Electronic Notes in Theoretical Computer Science", month = aug, } @PhdThesis{Peureux2002-Phd, author = "Fabiena Peureux", title = "{G}{\'e}n{\'e}ration de tests aux limites {\`a} partir de sp{\'e}cifications {B} en Programmation Logique avec Contraintes Ensemblistes", school = "UFR Sciences et techniques de l'Universit{\'e} de Franche-Comt{\'e}", year = "2002", URL = "http://www-lsr.imag.fr/b/Documents/Theses/thesePeureux.ps.gz", }