Prover’s expertise in formal methods, particularly through the use of the HLL (High Level Language) and its dedicated tools, combined with the constant commitment of the teams, has led to significant advancements. Our team has thus contributed to the thorough assessment of the tracking function of this CBTC, together with experts from Sig4 Engineering. As a tool provider, expertise provider, and long-time partner of RATP, Prover stands out for its leading position in the field of critical systems analysis, thus ensuring reliable and efficient solutions for transport infrastructures. 

Inlägget Prover and RATP strengthen collaboration dök först upp på Prover - Engineering a Safer World.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Prover’s advanced solutions powering Orléans Tramway signaling project dök först upp på Prover - Engineering a Safer World.

• Ha erfarenhet av och intresse för projektledning.

• Samarbeta bra både med kunder och Provers experter.

• Vara kvalitetsmedveten och resultatinriktad och hela tiden vara uppmärksam på att de som arbetar i projekten gör det som faktiskt beställts.

• Ha förmåga att arbeta systematiskt.

• Vara bra på att organisera och följa upp.

• Ha tillräcklig teknisk kunskap om signalsystem för tunnelbana och järnväg för att kunna delta i och förstå vad som sägs på möten både med kund och internt.

• Prata bra svenska med svenskspråkiga kunder. 

• Prata bra engelska med utländska kunder och med de Prover-anställda som inte pratar svenska.

Arbetsbeskrivning

Tåg är snabbare, mer ekonomiska, säkrare och miljövänligare än bilar och lastbilar. På Prover är vi fast beslutna att göra vår del för en bättre värld. Vi levererar lösningar för konstruktion av de säkerhetskritiska system som styr tågsignaler och växlar. Bland våra kunder finns infrastrukturförvaltare som SL, Trafikverket, Paris tunnelbana RATP och New Yorks tunnelbana MTA, samt leverantörer av signalsystem såsom Alstom, Hitachi och Siemens. 

På Prover arbetar skickliga människor från hela världen tillsammans för att skapa och leverera moderna lösningar för signalsystem. Förutom i Stockholm har vi också kontor i Frankrike, samt verksamhet i USA och Kina. Dina kollegor kommer att vara några av de bästa på formella metoder och signalering. Vi är angelägna om att ständigt förbättra våra arbetssätt, så det finns många möjligheter att bidra med nya innovativa idéer. 

Vi ser gärna att du har erfarenhet av branschen för signalsystem för järnväg och tunnelbana i Sverige. 

Anställningen är tills vidare och innebär projektledning av såväl dagens projekt som framtida projekt. Vi växer och har ett ständigt inflöde av nya projekt, både större som sträcker sig över flera år och mindre som varar någon månad. 

Som projektledare rapporterar du till vår Solutions Manager Benjamin Blanc. 

Du kan komma att säkerhetsprövas för känsliga projekt och behöver vara beredd att godkänna det. 

Skicka din ansökan med personligt brev och CV till jobs@prover.com. Vi ser fram emot att höra av dig! 

Contact

Benjamin Blanc
Solutions Manager, Prover

Inlägget Project manager – Rail and Metro dök först upp på Prover - Engineering a Safer World.

Introduction

Guarantee the safety of your rail control system.

When developing safety critical rail control software, achieving compliance with safety standards such as CENELEC EN50128 is a significant part of the project. Traditionally, this involves a number of manual steps such as reviewing verification documents, making test plans and reports and, of course, testing itself.

These activities are typically carried out at a later stage of the project, where delays can significantly impact the overall schedule and any issues discovered are costly to address. Furthermore, the highly experienced staff who have the qualifications needed to perform these tasks are often a bottleneck resource.

The solution is to consider safety, and how it is demonstrated, from the start of the project, and to use more automation throughout the verification process. Much of the work of achieving compliance with safety standards can be replaced with Formal Verification. A technique based on mathematical proofs that gives 100% coverage. Since Formal Verification gives full coverage and is fully automated, not only will it increase safety confidence but it will also help reduce the overall cost for safety assessment.

What you will learn in this guide

In this guide, you will learn how to use Formal Verification to meet prevailing safety requirements with full confidence. All while reducing effort, increasing quality, and reducing the risk for project delays in the process.

On the following pages, we will summarize the safety requirements for rail control software set out by the prevailing CENELEC EN 50128 standard, discuss the advantages of using Formal Verification versus traditional system testing methods, and take a closer look at how Formal Verification impacts the verification and validation process and safety approval in rail control projects. Finally, we will explore how Formal Verification is used in practice and offer some recommendations for the implementation process.

Fill out the form to read the full guide.

Inlägget How to build a solid safety case for your rail control system using formal verification dök först upp på Prover - Engineering a Safer World.

With this new version of PSL, it is now possible to directly load sHLL models without an external translation phase. Potential error messages are displayed with direct reference to the sHLL file. This sHLL model can be mixed with any HLL sections such as constraints, proof obligations or lemmas.

sHLL is Prover’s imperative extension over HLL. It can be used as an intermediate step when translating designs from imperative languages (such as C or Ada) but can also be used as an input language for the formalization of imperative-style specifications. sHLL simply encapsulates HLL expressions as assignments in a setting that also defines:

– a set of global variables that could be assigned at various levels.

– procedures, that may modify some global variables, and that provides a finite while loop construction.

– statements that define a call order of these procedures.

This structure is then embedded in the natural temporal loop beneath the HLL execution model.

Consider the following HLL loop, where an array state variable state is defined recursively by a global variable global:

Inputs:
int in1;
Declarations:
int^(3) state;
Definitions:
I(state[a]) := 0;
X(state[a]) := global[a];

The following sHLL model defines how global is successively modified at each step by calls to procedure1 (which iterates over the array and adds the current input value in1 to each cell of the array), and procedure2 (which multiplies the resulting cell with the value of its index):

Globals:
int^(3) global;
Procedures:
procedure1(int in1; int^(3) global) {
    int idx;
    idx:= 0;
    while (idx <= 2)[3] {
    global[idx] := global[idx] + in1;
    idx := idx + 1;
    }
}
procedure2(; int^(3) global) {
    int idx;
    idx:= 0;
    while (idx <= 2)[3] {
    global[idx] := global[idx] * idx;
    idx := idx + 1;
    }
}
Statements:
global:=state;
procedure1(in1; global);
procedure2(;global);

At every cycle, in1 is randomly assigned to an integer value; global is evaluated by first applying the expression in procedure1, then procedure2; global is eventually passed to state to store the value at the end of an HLL cycle.  

This clear separation between the pure dataflow style of HLL and the imperative style of sHLL allows to lower the distance when dealing with high-level pieces of code. For instance, when an algorithm has been specified in C, Ada, or even in a state-based specification language like B, using sHLL is a more natural candidate both for modeling this algorithm and for checking properties. You might, for example, want to check that the following property holds:

Proof Obligations:
ALL i:[0,2] (global[i] >=i);

This proof obligation is obviously false, and when loading this model files in PSL, a counterexample can be explored using the tool Why for sHLL structures:

psl -shll model.shll -hll model.hll -intSize 16 -ind -why

[depth 0]>
$0: ALL i:[0,2] (global[i] >= i) is [f]
because:
$1: global[0] >= 0 is [t]
$2*: global[1] >= 1 is [f]
$3: global[2] >= 2 is [f]

[depth 0]>
$4: global[1] is [-32767]
because:
procedure2(; global);
and:
$6*: global[1] is [-32767]

[model.shll:26][depth 0]>
$6: global[1] is [-32767]
because:
global[idx] := global[idx] * idx;
and:
$7: idx is [1]
$8*: global[idx] * idx is [-32767]

Debugging is available at the sHLL level, allowing for backward search into root causes of this falsifiable proof obligation using the identifiers at the sHLL level, and pointing to part of the code relevant for the current state of the debugger. It is hence much easier to understand what is wrong and corrections made in the source code can be directly fed to PSL for another run until the proof obligation becomes valid.

This step forward in the direction of handling imperative programs with PSL will be followed by many other steps to keep improving the debugger, and the support for error localization in Prover Studio. See our previous blog post about that here. We are eagerly waiting for your feedback to contribute to this new feature and its integration with other Prover tools.  

Inlägget PSL now supports sHLL dök först upp på Prover - Engineering a Safer World.

• You are talented, ambitious and enthusiastic. You want to contribute to a sustainable and safe world.

• You have a degree (at least three years of university studies) in computer science, automation or mathematics.

• You are a good programmer in at least one programming language, and you are familiar with mathematical logic.

• You need to be fluent in English, and located in Sweden or France.

Job Description

At Prover an experienced team with talents from around the world works together creating and delivering state-of-the-art solutions for train control systems. Your colleagues will be some of the best people in the world in formal methods. The Prover team is highly educated (~50% PhD’s) with a desire to apply theoretical knowledge to real-life problems that matter. We are eager to constantly improve our methods. There are many opportunities to contribute with new innovative techniques and bright ideas.

You will work in the Solutions team located in France and Sweden. Your main task will be to develop and maintain formal specifications for customers in rail or metro, and to perform formal verification work. We use Python for automation of various tasks and for conversion between data formats.

Please note that this position is based in either Stockholm or Toulouse, and relocation is required.

Send your application with your resume and cover letter to jobs@prover.com.

About Prover

Engineering a safer world

Trains are faster, more economical, safer and greener than cars and trucks. At Prover Technology, we are committed to doing our part for a better world. We supply solutions for engineering the safety-critical systems that control train signals and switches.

Prover has subsidiaries in the US, France and China. It is privately owned by investors and staff, and has customers in Europe, North America and Asia.

At Prover you will find a highly intelligent team, a respectful atmosphere and cultural diversity.

Contact

Benjamin Blanc
Solutions Manager, Prover

Inlägget Formal methods developer – rail and metro dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

benjamin.blanc

An easier path to CENELEC EN50128 SIL4 compliance

In almost every rail control project the effort for achieving compliance with safety standards such as CENLEC EN50128 is a significant part of the project. Traditionally, this involves many manual steps such as reviewing verification documents, test plans, and test reports.

Much of this work can be replaced with automated formal verification, reducing effort, increasing quality, and reducing risk for project delays.

Formal verification is a technique based on mathematical proofs that gives 100 % coverage and can be fully automated. In this recorded webinar, we focus on how formal verification, implemented with a pre-qualified T2 SIL4 tool, Prover Certifier, can be used in a CENELEC EN50128 compliant process.

We also present a case study on how CASCO, a leading rail control supplier, benefits from formal verification in its safety process.

Agenda:

• What is formal verification and why do we need it
• Formal verification in a CENELEC EN50128 SIL4 process
• Introduction to Prover Certifier, a T2 SIL-4 qualified formal verification tool

• A case study: Formal safety verification at CASCO

• Recommendations and considerations for the implementation process

Yes please, send me the recording!

Hosts

Benjamin Blanc
Solutions Manager, Prover

Olav Bandmann
Chief Technology Officer, Prover

Daniel Fredholm
Senior Consultant, Prover

Inlägget Building a safety case for rail control software with formal verification dök först upp på Prover - Engineering a Safer World.

This course provided a practical introduction to formal verification activities that are encountered in real-world projects. We talked about formalizing requirements, environment modeling through constraints, choosing an appropriate proof strategy and, of course, some debugging. This may sound like it would require a strong background in software engineering to be at ease with the software tools. However, the attendees revealed unexpected skills when digging into PSL – our proof engine – and its associated tools.

As per usual in formal verification, a large amount of time was spent on the corner cases of requirement specification. Indeed, even though safety engineers are used to providing such requirements, they were sometimes surprised when formalization exposed some missing behaviors or lack of precision. Manipulating HLL formulas, especially when quantification enters, is a powerful way to reveal corner cases of even the most simple designs.

Prover would like to congratulate all of the attendees for their patience and enthusiasm during this course, helping to share lessons learned with others. We are happy that more people are now Prover Certified formal verification engineers.

Inlägget HLL crash course for safety engineers dök först upp på Prover - Engineering a Safer World.