B-Method (original) (raw)
The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.
| Property | Value |
|---|---|
| dbo:abstract | The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software. (en) La méthode B est une méthode formelle qui permet le raisonnement sur des systèmes complexes ainsi que le développement logiciel. La méthode B permet de modéliser de façon abstraite le comportement et les spécifications d'un logiciel dans le langage de B, puis par raffinements successifs d'aboutir à un modèle concret dans un sous-ensemble du langage B transcodable en Ada ou en C, exécutables par une machine concrète. Elle permet de formaliser le système et son environnement de manière abstraite, puis par raffinements successifs, de rajouter les détails au modèle du système. 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 implémentations concrètes avec le modèle abstrait). On distingue : * le B classique tel qu'il est défini dans le B Book de 1996. L'outil logiciel de support est l'atelier B ou le B-Toolkit . * le 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). Par conséquent, la méthode peut s'appliquer pour l'étude des systèmes de domaines variés, plus seulement à des programmes. On réalise alors des développements incrémentaux de systèmes prouvés. Pour cela on utilise toujours l'atelier B. * le 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. (fr) B-Methodとは、AMN（Abstract Machine Notation）という仕様記述言語（兼プログラミング言語）を中心とした形式手法に基づいたソフトウェア開発手法である。B-Method で使用する形式手法やそのツール群は単に B と呼ぶ。 (ja) B är en mjukvaruutvecklingsmetod framtagen av , tillika ett språk och CASE-verktyg från . 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 programmet. På detta sätt går det att ta fram matematiska bevis att programmet fungera innan det riktiga programmet skrivs. (sv) B — загальний термін, яким називають B-Method (формальний метод розробки програмного забезпечення), процес такої розробки, мову запису специфікації, і інструменти що їх підтримують (B-Toolkit) (uk) |
| dbo:wikiPageExternalLink | http://www.atelierb.eu/index_en.html https://www.methode-b.com/en/ https://web.archive.org/web/20051012233257/http:/www-lsr.imag.fr/B/ https://web.archive.org/web/20080221232310/http:/www.atelierb.eu/index_en.html |
| dbo:wikiPageID | 2443683 (xsd:integer) |
| dbo:wikiPageLength | 13125 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1113555107 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Cambridge_University_Press dbr:Canada dbr:Besançon dbc:Formal_methods_tools dbr:Ulm dbr:United_Kingdom dbr:VHDL dbr:X_Window dbr:STMicroelectronics dbr:Open_source dbr:Ib_Holm_Sørensen dbr:Germany dbr:Montpellier dbr:Motif_(software) dbr:Linux dbr:Linz dbr:London dbr:Siemens dbr:Z_User_Group dbr:Palgrave_Macmillan dbr:Plug-in_(computing) dbr:Austria dbr:BP dbr:British_Computer_Society dbr:COVID-19_pandemic dbc:Formal_specification_languages dbr:Toulouse dbr:Turku dbr:Alstom dbr:Eclipse_(software) dbr:Europe dbr:European_Union dbr:Finland dbr:France dbr:Abstract_State_Machines dbr:Paris_Métro_Line_1 dbr:Paris_Métro_Line_14 dbr:Formal_methods dbr:Formal_specification dbr:Digital_circuit dbr:Mathematical_proof dbr:Refinement_(computing) dbr:ATMEL dbr:Grenoble dbr:Guildford dbr:Italy dbr:Ariane_5 dbc:Formal_methods dbr:Abstract_machine_notation dbr:Kevin_Lano dbr:Jean-Raymond_Abrial dbr:Z_notation dbr:Software_design dbr:Automatic_programming dbr:Pisa dbr:Software_development dbr:Solaris_(operating_system) dbr:Southampton dbr:Springer_Science+Business_Media dbr:Encapsulation_(object-oriented_programming) dbr:Integrated_development_environment dbr:Nantes dbr:OS_X dbr:Orford,_Quebec dbr:Québec dbr:Set_theory dbr:York dbr:Software dbr:Imperial_College_Press dbr:Programming_language dbr:Safety-critical_system dbr:World_Scientific_Publishing_Company dbr:First_order_logic dbr:Formal_method dbr:Addison_Wesley_Longman dbr:Program_refinement dbr:Program_specification dbr:Logical_argument |
| dbp:date | 2008-02-21 (xsd:date) |
| dbp:url | https://web.archive.org/web/20080221232310/http:/www.atelierb.eu/index_en.html |
| dbp:wikiPageUsesTemplate | dbt:ISBN dbt:Main dbt:Reflist dbt:Webarchive |
| dcterms:subject | dbc:Formal_methods_tools dbc:Formal_specification_languages dbc:Formal_methods |
| gold:hypernym | dbr:Method |
| rdf:type | dbo:Software yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Communication100033020 yago:Know-how105616786 yago:Language106282651 yago:Method105660268 yago:PsychologicalFeature100023100 yago:WikicatFormalMethods yago:WikicatFormalSpecificationLanguages |
| rdfs:comment | The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software. (en) B-Methodとは、AMN（Abstract Machine Notation）という仕様記述言語（兼プログラミング言語）を中心とした形式手法に基づいたソフトウェア開発手法である。B-Method で使用する形式手法やそのツール群は単に B と呼ぶ。 (ja) B är en mjukvaruutvecklingsmetod framtagen av , tillika ett språk och CASE-verktyg från . 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 programmet. På detta sätt går det att ta fram matematiska bevis att programmet fungera innan det riktiga programmet skrivs. (sv) B — загальний термін, яким називають B-Method (формальний метод розробки програмного забезпечення), процес такої розробки, мову запису специфікації, і інструменти що їх підтримують (B-Toolkit) (uk) La méthode B est une méthode formelle qui permet le raisonnement sur des systèmes complexes ainsi que le développement logiciel. La méthode B permet de modéliser de façon abstraite le comportement et les spécifications d'un logiciel dans le langage de B, puis par raffinements successifs d'aboutir à un modèle concret dans un sous-ensemble du langage B transcodable en Ada ou en C, exécutables par une machine concrète. Elle permet de formaliser le système et son environnement de manière abstraite, puis par raffinements successifs, de rajouter les détails au modèle du système. 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 implémentations concrètes (fr) |
| rdfs:label | B-Method (en) Méthode B (fr) B-Method (ja) B (mjukvaruutveckling) (sv) B-метод (uk) |
| owl:sameAs | freebase:B-Method yago-res:B-Method wikidata:B-Method dbpedia-fr:B-Method dbpedia-ja:B-Method dbpedia-sv:B-Method dbpedia-uk:B-Method https://global.dbpedia.org/id/2reK8 |
| prov:wasDerivedFrom | wikipedia-en:B-Method?oldid=1113555107&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:B-Method |
| is dbo:knownFor of | dbr:Ken_Robinson_(computer_scientist) dbr:Kevin_Lano dbr:Michael_Butler_(computer_scientist) |
| is dbo:wikiPageDisambiguates of | dbr:B_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:B-Tool dbr:B_notation_(specification_language) dbr:Ib_Sørensen dbr:B-Toolkit dbr:Atelier_B dbr:Abstract_machine_notation dbr:Association_de_Pilotage_des_Conférences_B dbr:Event-B dbr:International_B_Conference_Steering_Committee dbr:B4free dbr:B_method dbr:B-Tookit dbr:Clearsy |
| is dbo:wikiPageWikiLink of | dbr:Carroll_Morgan_(computer_scientist) dbr:B-Tool dbr:B_(disambiguation) dbr:B_notation_(specification_language) dbr:Rodin_tool dbr:Predicate_transformer_semantics dbr:Egon_Börger dbr:Contrôle_de_vitesse_par_balises dbr:Steve_Schneider_(computer_scientist) dbr:Z_User_Group dbr:Ib_Sørensen dbr:Specification_language dbr:B-Toolkit dbr:Alt-Ergo dbr:Abrial dbr:Paris_Métro_Line_14 dbr:Formal_methods dbr:Formal_specification dbr:Refinement_(computing) dbr:Atelier_B dbr:Abstract_machine_notation dbr:Ken_Robinson_(computer_scientist) dbr:Kevin_Lano dbr:TLA+ dbr:Jean-Raymond_Abrial dbr:Z_notation dbr:Association_de_Pilotage_des_Conférences_B dbr:Guarded_Command_Language dbr:Michael_Butler_(computer_scientist) dbr:Model-based_testing dbr:Satisfiability_modulo_theories dbr:Event-B dbr:International_B_Conference_Steering_Committee dbr:B4free dbr:B_method dbr:B-Tookit dbr:Clearsy |
| is dbp:knownFor of | dbr:Ken_Robinson_(computer_scientist) dbr:Kevin_Lano dbr:Michael_Butler_(computer_scientist) |
| is foaf:primaryTopic of | wikipedia-en:B-Method |