Links - Revision history

Michael Leuschel: /* Tools using ProB */

2024-10-01T10:41:53Z

Tools using ProB

← Older revision		Revision as of 10:41, 1 October 2024
Line 30:		Line 30:
	* [https://github.com/Joshua27/BSynthesis BSynthesis] tool for repair and generation of formal models		* [https://github.com/Joshua27/BSynthesis BSynthesis] tool for repair and generation of formal models
	* [https://safecap.co.uk SafeCap]		* [https://safecap.co.uk SafeCap]
			* [https://pkoerner.github.io/lisb-doc/ LisB], a Clojure/DSL API built-on top of the ProB-JAVA API
	* [http://wiki.event-b.org/index.php/IUML-B iUML Statemachines]		* [http://wiki.event-b.org/index.php/IUML-B iUML Statemachines]
	* [http://users.ecs.soton.ac.uk/vs2/ac.soton.multisim.updatesite/ MultiSimulation Plug-In for Rodin]		* [http://users.ecs.soton.ac.uk/vs2/ac.soton.multisim.updatesite/ MultiSimulation Plug-In for Rodin]

Michael Leuschel: /* Testimonials */

2024-09-05T07:43:13Z

Testimonials

← Older revision		Revision as of 07:43, 5 September 2024
Line 66:		Line 66:

	== Testimonials ==		== Testimonials ==
	* [https://prologyear.logicprogramming.org/ColmerauerPrize.html ~~Winner of the first~~ Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i> "The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022: ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i>		* [https://prologyear.logicprogramming.org/ColmerauerPrize.html Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i> "The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022: ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i>
	* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>		* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>
	*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>		*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>

Michael Leuschel: /* Testimonials */

2024-09-05T07:42:49Z

Testimonials

← Older revision		Revision as of 07:42, 5 September 2024
Line 66:		Line 66:

	== Testimonials ==		== Testimonials ==
	* [https://prologyear.logicprogramming.org/ColmerauerPrize.html Winner of the first Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i>"The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022: ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i>		* [https://prologyear.logicprogramming.org/ColmerauerPrize.html Winner of the first Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i> "The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022: ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i>
	* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>		* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>
	*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>		*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>

Michael Leuschel: /* Testimonials */

2024-09-05T07:42:30Z

Testimonials

← Older revision		Revision as of 07:42, 5 September 2024
Line 66:		Line 66:

	== Testimonials ==		== Testimonials ==
	* [https://prologyear.logicprogramming.org/ColmerauerPrize.html Winner of the first Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i>"The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022:		* [https://prologyear.logicprogramming.org/ColmerauerPrize.html Winner of the first Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i>"The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022: ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i>
	ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i>
	* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>		* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>
	*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>		*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>

Michael Leuschel: /* Testimonials */

2024-09-05T07:42:15Z

Testimonials

← Older revision		Revision as of 07:42, 5 September 2024
Line 66:		Line 66:

	== Testimonials ==		== Testimonials ==
			* [https://prologyear.logicprogramming.org/ColmerauerPrize.html Winner of the first Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i>"The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022:
			ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i>
	* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>		* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>
	*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>		*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>

Michael Leuschel: /* Testimonials */

2024-09-05T07:37:53Z

Testimonials

← Older revision		Revision as of 07:37, 5 September 2024
Line 66:		Line 66:

	== Testimonials ==		== Testimonials ==
			* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i>
	*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>		*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>
	*[https://openportal.isti.cnr.it/doc?id=people______::8e1a740ac10b66042af4f30812531d2d The 4SECURail approach to formalizing standard interfaces between signalling systems components, Belli et al.] <i>"ProB has been selected as the second target of the formal encoding because of its recognized role (Ferrari et al. 2020) in the field of formal railway-related modelling. It provides user-friendly interfaces, and allows LTL/CTL model checking, state-space exploration, state-space projections, and trace descriptions in the form of sequence diagrams"</i>		*[https://openportal.isti.cnr.it/doc?id=people______::8e1a740ac10b66042af4f30812531d2d The 4SECURail approach to formalizing standard interfaces between signalling systems components, Belli et al.] <i>"ProB has been selected as the second target of the formal encoding because of its recognized role (Ferrari et al. 2020) in the field of formal railway-related modelling. It provides user-friendly interfaces, and allows LTL/CTL model checking, state-space exploration, state-space projections, and trace descriptions in the form of sequence diagrams"</i>

Michael Leuschel: /* Testimonials */

2023-08-08T08:03:18Z

Testimonials

← Older revision		Revision as of 08:03, 8 August 2023
Line 67:		Line 67:
	== Testimonials ==		== Testimonials ==
	*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>		*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>
	*[https://openportal.isti.cnr.it/doc?id=people______::8e1a740ac10b66042af4f30812531d2d The 4SECURail approach to formalizing standard interfaces between signalling systems components, Belli et al.] <t>"ProB has been selected as the second target of the formal encoding because of its recognized role (Ferrari et al. 2020) in the field of formal railway-related modelling. It provides user-friendly interfaces, and allows LTL/CTL model checking, state-space exploration, state-space projections, and trace descriptions in the form of sequence diagrams"</i>		*[https://openportal.isti.cnr.it/doc?id=people______::8e1a740ac10b66042af4f30812531d2d The 4SECURail approach to formalizing standard interfaces between signalling systems components, Belli et al.] <i>"ProB has been selected as the second target of the formal encoding because of its recognized role (Ferrari et al. 2020) in the field of formal railway-related modelling. It provides user-friendly interfaces, and allows LTL/CTL model checking, state-space exploration, state-space projections, and trace descriptions in the form of sequence diagrams"</i>
	* [http://www.deploy-project.eu/pdf/D41-Siemens-final-full.pdf Data validation at Siemens, Jérôme Falampin]: <i>""The work done with ProB is a great success. Thanks to the automatization and ProB, the wayside data validation is quicker, easier and complete."</i> More details and academic papers can be found on our page [[Siemens Data Validation with ProB]].		* [http://www.deploy-project.eu/pdf/D41-Siemens-final-full.pdf Data validation at Siemens, Jérôme Falampin]: <i>""The work done with ProB is a great success. Thanks to the automatization and ProB, the wayside data validation is quicker, easier and complete."</i> More details and academic papers can be found on our page [[Siemens Data Validation with ProB]].
	* [http://dl.acm.org/citation.cfm?doid=2406336.2406351 Pacemaker model by Mery and Singh]: <i>"ProB was very useful in the development of the pacemaker specification, and was able to animate all of our models and able to prove the absence of error (no counterexample exist). The ProB model checker also discovered several invariant violations, e.g., related to incorrect responses or unordered pacing and sensing activities. It was also able to discover a deadlock in two of the models, which was due to the fact that “clock counter” were not properly recycled, meaning that after a while no pacing or sensing activities occur into the system. Such kind of errors would have been more difficult to uncover with the prover of RODIN tool."</i>		* [http://dl.acm.org/citation.cfm?doid=2406336.2406351 Pacemaker model by Mery and Singh]: <i>"ProB was very useful in the development of the pacemaker specification, and was able to animate all of our models and able to prove the absence of error (no counterexample exist). The ProB model checker also discovered several invariant violations, e.g., related to incorrect responses or unordered pacing and sensing activities. It was also able to discover a deadlock in two of the models, which was due to the fact that “clock counter” were not properly recycled, meaning that after a while no pacing or sensing activities occur into the system. Such kind of errors would have been more difficult to uncover with the prover of RODIN tool."</i>

Michael Leuschel: /* Testimonials */

2023-08-08T08:03:00Z

Testimonials

← Older revision		Revision as of 08:03, 8 August 2023
Line 67:		Line 67:
	== Testimonials ==		== Testimonials ==
	*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>		*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i>
			*[https://openportal.isti.cnr.it/doc?id=people______::8e1a740ac10b66042af4f30812531d2d The 4SECURail approach to formalizing standard interfaces between signalling systems components, Belli et al.] <t>"ProB has been selected as the second target of the formal encoding because of its recognized role (Ferrari et al. 2020) in the field of formal railway-related modelling. It provides user-friendly interfaces, and allows LTL/CTL model checking, state-space exploration, state-space projections, and trace descriptions in the form of sequence diagrams"</i>
	* [http://www.deploy-project.eu/pdf/D41-Siemens-final-full.pdf Data validation at Siemens, Jérôme Falampin]: <i>""The work done with ProB is a great success. Thanks to the automatization and ProB, the wayside data validation is quicker, easier and complete."</i> More details and academic papers can be found on our page [[Siemens Data Validation with ProB]].		* [http://www.deploy-project.eu/pdf/D41-Siemens-final-full.pdf Data validation at Siemens, Jérôme Falampin]: <i>""The work done with ProB is a great success. Thanks to the automatization and ProB, the wayside data validation is quicker, easier and complete."</i> More details and academic papers can be found on our page [[Siemens Data Validation with ProB]].
	* [http://dl.acm.org/citation.cfm?doid=2406336.2406351 Pacemaker model by Mery and Singh]: <i>"ProB was very useful in the development of the pacemaker specification, and was able to animate all of our models and able to prove the absence of error (no counterexample exist). The ProB model checker also discovered several invariant violations, e.g., related to incorrect responses or unordered pacing and sensing activities. It was also able to discover a deadlock in two of the models, which was due to the fact that “clock counter” were not properly recycled, meaning that after a while no pacing or sensing activities occur into the system. Such kind of errors would have been more difficult to uncover with the prover of RODIN tool."</i>		* [http://dl.acm.org/citation.cfm?doid=2406336.2406351 Pacemaker model by Mery and Singh]: <i>"ProB was very useful in the development of the pacemaker specification, and was able to animate all of our models and able to prove the absence of error (no counterexample exist). The ProB model checker also discovered several invariant violations, e.g., related to incorrect responses or unordered pacing and sensing activities. It was also able to discover a deadlock in two of the models, which was due to the fact that “clock counter” were not properly recycled, meaning that after a while no pacing or sensing activities occur into the system. Such kind of errors would have been more difficult to uncover with the prover of RODIN tool."</i>

Michael Leuschel: /* Books and Resources on B */

2023-02-15T16:31:41Z

Books and Resources on B

← Older revision		Revision as of 16:31, 15 February 2023
Line 1:		Line 1:
	== Books and Resources on B ==		== Books and Resources on B ==
	* [https://doi.org/10.1017/CBO9780511624162 The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial]		* [https://doi.org/10.1017/CBO9780511624162 The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial]
	* [~~http~~://www.~~palgrave~~.~~com~~/~~science~~/~~computing~~/~~schneider~~/ The B-Method: An Introduction, by Steve Schneider] ((Cornerstones of Computing) )		* [https://www.amazon.de/-/en/Steve-Schneider/dp/033379284X/ The B-Method: An Introduction, by Steve Schneider] ((Cornerstones of Computing) )
	* [http://www.event-b.org/abook.html Modeling in Event-B: System and Software Engineering, by Jean-Raymond Abrial] (the Bee book)		* [http://www.event-b.org/abook.html Modeling in Event-B: System and Software Engineering, by Jean-Raymond Abrial] (the Bee book)
	* [https://www3.hhu.de/stups/handbook/rodin/current/html/ Rodin Users' Handbook]		* [https://www3.hhu.de/stups/handbook/rodin/current/html/ Rodin Users' Handbook]

Michael Leuschel: /* Books */

2023-02-15T16:29:56Z

Books

← Older revision		Revision as of 16:29, 15 February 2023
Line 1:		Line 1:
	== Books ==		== Books and Resources on B ==
	* [https://doi.org/10.1017/CBO9780511624162 The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial]		* [https://doi.org/10.1017/CBO9780511624162 The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial]
	* [http://www.palgrave.com/science/computing/schneider/ The B-Method: An Introduction, by Steve Schneider] ((Cornerstones of Computing) )		* [http://www.palgrave.com/science/computing/schneider/ The B-Method: An Introduction, by Steve Schneider] ((Cornerstones of Computing) )
Line 5:		Line 5:
	* [https://www3.hhu.de/stups/handbook/rodin/current/html/ Rodin Users' Handbook]		* [https://www3.hhu.de/stups/handbook/rodin/current/html/ Rodin Users' Handbook]
	* Atelier-B Reference Manual (available as part of the [[https://www.atelierb.eu/en/atelier-b-support-maintenance/download-atelier-b/ Atelier-B download])		* Atelier-B Reference Manual (available as part of the [[https://www.atelierb.eu/en/atelier-b-support-maintenance/download-atelier-b/ Atelier-B download])
			* [https://mooc.imd.ufrn.br/course/the-b-method MOOC: The B-Method: from specification to code]

	== Papers ==		== Papers ==