Team

This page lists all known team members and their expertise in alphabetical order (by first name):

Alexander Stante

Company	gitHub
Frauenhofer Gesellschaft (FhG)	astante

Cecile Braunstein

Company	gitHub
University of Bremen (UBremen)	cecilebraun

Chokri Mraidha

Company	gitHub
CEA	cmraidha

Christophe Gaston

Company	gitHub
CEA	ChristopheGaston

Daniel Plagge

Company	gitHub
Formal Mind GmbH (FM)	dplagge

I have experience with model based specification formalisms like (Event-)B, Z and TLA+. The main focus of my work is validation of specifications by animation and model checking (some key words: constraint solving, LTL (linear temporal logic), SAT solving). I'm one of the developers of the ProB animator and model checker.

David Mentre

Company	gitHub
MITSUBISHI ELECTRIC R&D Centre Europe (MERCE)	MERCEmentre

Jan Peleska

Company	gitHub
University of Bremen (UBremen)	peleska

Jens Gerlach

Company	gitHub
Frauenhofer Gesellschaft (FhG)	mottainai

Jochen Krause (EclipseSource)

Jonas Helming (EclipseSource)

Klaus-Rüdiger Hase (Deutsche Bahn)

• Project Leader of openETCS

Marielle Petit Doche

Company	gitHub
Systerel	MariellePetitDoche

• I'm looking who si going to participate to the project for Systerel asap, thus new persons will be added.
• We will produce a white paper on Rodin and pluggins for the end of September.

Matthias Kummer

Company	gitHub
Swiss Railway Engineering (SRE)	mkummer

Merlin Pokam

Company	gitHub
Angewandte Eisenbahntechnik GmbH (AEbt)	MerlinPokam

Expertise in the railway sector

• Homologation of railway vehicles in Germany and Austria
• Creation of test specification for the detection of customer and safety requirements
• Planning and execution of tests of control software in laboratory and on railway vehicles
• Creation of hazard- and safety analysis
• Support for the evaluation of software according to EN 50128
• Consulting and implementation of standards compliant development processes according to
• EN 50126, EN 50128 and EN 50129
• Evaluation of the safety integrity of soft-and hardware
• I took part in the Development of the International Requirement List (European list of requirements for railway vehicles with the countries Germany, Italy, Netherlands, Austria and Switzerland) Expertise in the railway sector
• Assessor of the German Federal Railway Authority (EBA) for functional tests of railway vehicles and safety of computer-aided systems ID-No.: 05 E 33 B 002
• Assessor of the German Federal Railway Authority (EBA) for safety of computer-aided systems - vehicle control systems ID-No.: 31/02/019
• Assessor of the BMVIT (Federal Ministry of Traffic, Innovation and Technology, Austria) for expertises according § 31 EisbG (all extensive expertises) and §32 EisbG functional safety of railway vehicles
• Active member of the working group Task Force Interoperability (TFI) of the countries Germany, Austria, Switzerland, Italy and the Netherlands
• Active member of the working group Software, which is initiated and led of the German Federal Railway Authorities (EBA)
• Active member of the internal working group of the EBA for the definition of functional safety goals of railway vehicles

Michael Ditze

Company	gitHub
TWT GmbH (TWT)	mditze

Michael Jastram

Company	gitHub
Formal Mind GmbH (FM)	jastram

• Project lead of the toolchain workpackage (WP3a).
• Project lead of the Eclipse RMF project and extensive experience with the B and Event-B formalisms, as well as the Rodin platform for Event-B (Eclipse-based open source) and ProB (open source model checker for various formalisms.

Nico Laum

Company	gitHub
Universität Rostock (Uni Rostock)	nclmde

Norbert Schäfer (AEbt)

Expertise in the railway sector

• Assessor of the German Federal Railway Authority (EBA) for functional tests of railway vehicles and safety of computer-aided systems ID-No.: 05 E 33 B 002
• Assessor of the German Federal Railway Authority (EBA) for safety of computer-aided systems - vehicle control systems ID-No.: 31/02/019
• Assessor of the BMVIT (Federal Ministry of Traffic, Innovation and Technology, Austria) for expertises according § 31 EisbG (all extensive expertises) and §32 EisbG functional safety of railway vehicles
• Active member of the working group Task Force Interoperability (TFI) of the countries Germany, Austria, Switzerland, Italy and the Netherlands
• Active member of the working group Software, which is initiated and led of the German Federal Railway Authorities (EBA)
• Active member of the internal working group of the EBA for the definition of functional safety goals of railway vehicles

Silvano Dal Zilio

Company	gitHub
Vertics Group (Vertics)	dalzilio

Stanislas Pinte

Company	gitHub
ERTMS Solutions (ERTMS)	stanpinte

I took part in designing http://www.ertmssolutions.com/ertms-formalspecs/ I am in contact with WP2 leaders (SNCF), and already suggested to include in their study our tool ERTMSFormalSpecs (http://www.ertmssolutions.com/ertms-formalspecs/). I suggest to include ERTMSFormalSpecs.

Uwe Steinke

Company	gitHub
Siemens	UweSteinkeFromSiemens

We are implementing safety related software for rail systems and want to bring in the tool chain user's point of view: Requirements to the tool chain, but not develop the tool chain ourselves.

Virgile Prevosto

Company	gitHub
CEA LIST	(vprevosto)

• Frama-C: A framework for analysis of C programs

  • Frama-C is a set of tools for analyzing C programs. It is based on a kernel responsible for parsing the code under analysis and maintaining the internal state of the whole verification tasks. Various plug-ins can then be used, either interactively or through their programmatic interface, in order to verify the properties of interest on the code. In addition, Frama-C can take into account specifications for the program in the form of ACSL (ANSI/ISO C Specification Language) annotations.
  • The main plug-ins available within Frama-C distribution are the following:
    • Value analysis, which computes an over-approximation of the value of each variable at each program point, and will warn for each potential runtime error of the program
    • WP and Jessie, that are dedicated to prove functional properties expressed as function contracts in ACSL langage and are base on Hoare logic
    • From, which uses results of Value to retrieve the dependencies between inputs and outputs of a function.
    • Slicing, which transforms a program into a simpler one, equivalent to the original one according to some criteria set by the user

• Frama-C is distributed under the LGPL 2 license. An Eclipse plug-in allowing to interact with Frama-C from Eclipse has been released by Atos under the EPL license (see below).

  • Innovation Benefits
    • Frama-C is meant to handle real-world programs and has already been used in industrial case studies.
    • The framework is very flexible and allows to easily tailor generic analyzers to specific usages, as well as combining results from different analysis techniques to attain a given verification objective.
  • Inputs
    • C program
    • Potentially ACSL specifications
    • Specific plug-ins can be used to take other models (e.g. an automaton for the Aoraï plugin) as input.
  • Contacts
    • within OpenETCS: Virgile Prevosto [[mailto:[email protected]][[email protected]]]
    • http://frama-c.com
    • http://gforge.enseeiht.fr/projects/fcdt/ for the Eclipse plugin