B is a tool-supported formal method based around AMN, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the Paris Métro Line 14), and is attracting increasing interest in industry.

PropertyValue
dbpprop:abstract
  • B is a tool-supported formal method based around AMN, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the Paris Métro Line 14), and is attracting increasing interest in industry. It has robust, commercially available tool support for specification, design, proof and code generation. The method of software development based on B is known as the B-Method. Compared to Z, B is slightly more low-level and more focused on refinement to code rather than just formal specification — hence it is easier to correctly implement a specification written in B than one in Z. In particular, there is good tool support for this. Recently, another formal method called Event-B has been developed. Event-B is considered an evolution of B (also known as classical B). It is a simpler notation, which is easier to learn and use. It comes with tool support in the form of the Rodin Platform
  • La méthode B est une méthode formelle de développement logiciel qui permet de modéliser de façon abstraite dans le langage de B le comportement d'un programme, puis par raffinements successifs, d'aboutir à un modèle concret, sous-ensemble du langage transcodable en Ada ou en C. Une activité de preuve formelle permet de vérifier la cohérence du modèle abstrait et la conformité de chaque raffinement avec le modèle supérieur (prouvant ainsi la conformité de l'ensemble des implantations concrètes avec le modèle abstrait). On distingue le : B classique tel qu'il est définit dans le B Book de 1996 . L'outil logiciel de support est l'atelierB, ou le B-Toolkit . B événementiel qui est une évolution utilisant uniquement la notion d'événements pour décrire les actions et non plus les opérations (qui sont proches des routines informatiques). Du coup la méthode peut s'appliquer sur des systèmes variés comme de l'électronique et non plus seulement des programmes. On réalise alors des développements incrémentaux de systèmes prouvés. Pour cela on utilise toujours l'atelierB mais conjointement avec Click'n'Prove B# (B sharp) qui est une reprise du B événementiel avec des éléments de la notation Z. L'atelier logiciel change et s'appelle Rodin.
  • B-Methodとは、AMN（Abstract Machine Notation）という仕様記述言語（兼プログラミング言語）を中心とした形式手法に基づいたソフトウェア開発手法である。B-Method で使用する形式手法やそのツール群は単に B と呼ぶ。
  • B är en mjukvaruutvecklingsmetod framtagen av Jean-Raymond Abrial, tillika ett språk och CASE-verktyg från B-Core (UK) Ltd.. B-metoden är nästan unik bland formella mjukvaruutvecklingsmetoder i det avseendet att den använder samma notation för specifikation, design och programmeringen. Språket B byggs upp med hjälp av matematiska formler med vars hjälp det går att validera programmet. På detta sättet går det att ta fram matematiska bevis att programmet fungera innan det riktiga programmet skrivs.
dbpprop:hasPhotoCollection
dbpprop:reference
rdf:type
rdfs:comment
  • B is a tool-supported formal method based around AMN, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the Paris Métro Line 14), and is attracting increasing interest in industry.
  • La méthode B est une méthode formelle de développement logiciel qui permet de modéliser de façon abstraite dans le langage de B le comportement d'un programme, puis par raffinements successifs, d'aboutir à un modèle concret, sous-ensemble du langage transcodable en Ada ou en C.
  • B-Methodとは、AMN（Abstract Machine Notation）という仕様記述言語（兼プログラミング言語）を中心とした形式手法に基づいたソフトウェア開発手法である。B-Method で使用する形式手法やそのツール群は単に B と呼ぶ。
  • B är en mjukvaruutvecklingsmetod framtagen av Jean-Raymond Abrial, tillika ett språk och CASE-verktyg från B-Core (UK) Ltd.. B-metoden är nästan unik bland formella mjukvaruutvecklingsmetoder i det avseendet att den använder samma notation för specifikation, design och programmeringen. Språket B byggs upp med hjälp av matematiska formler med vars hjälp det går att validera programmet.
rdfs:label
  • B-Method
  • Méthode B
  • B-Method
  • B (mjukvaruutveckling)
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of
is owl:sameAs of