Jérôme Falampin

dblp:39/2996 · DBLP profile ↗
← Back
2ranked-venue papers
0as first author
0since 2021 · last 2011
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 2Software engineering, systems software and programming languages · 1

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
1 paper
Program verification · 100%

Topics — the 1 heaviest of 2, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Program verification
formal modeling
0.012009
Automated Property Verification for Large Scale B Models · FM 2009

Methods — techniques the papers use, named apart from their topics

property verification · 0.1b method · 0.1
YearPublicationVenuePosition
2011 Automated property verification for large scale B models with ProB
abstract
Abstract In this paper we describe the successful application of the ProB tool for data validation in several industrial applications. The initial case study centred on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for Atelier B. Atelier B, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense, and they need to be revalidated whenever the rail network infrastructure changes. In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in a few minutes that were manually uncovered in about one man-month. We have repeated this task for three ongoing projects at Siemens, notably the ongoing automatisation of the line 1 of the Paris Métro. Here again, about a man month of effort has been replaced by a few minutes of computation. This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation algorithm. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. We also describe the issue of validating ProB , so that it can be integrated into the SIL4 development chain at Siemens.
Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
Formal Aspects Comput.2
2009 Automated Property Verification for Large Scale B Models
Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
FM2