Formal Methods for Industrial Critical Systems 2020

The 25th International Conference on Formal Methods (FMICS) 2020 took place virtually in Vienna on the 2-3 September. Today Formal Methods - techniques more than 50 years old - is recognized by the FMICS community as the cutting-edge technologies for specification, development, and verification of software and hardware systems. FMICS 2020 was an unprecedented effort [...]

By |2020-10-14T13:55:54+01:00October 14th, 2020|Formal Methods|

Why Formal Verification – Verifying Safety Requirements on Railway Systems

The subject I am going to write about this time is not an easy one. I will try to explain why formal verification is good. In particular, why it is a good practice to use formal verification when verifying safety requirements on railway systems. The Verification Problem In order to make a convincing argument, I [...]

By |2021-11-20T12:00:42+01:00February 10th, 2020|Formal Methods, Formal Verification|

Using HLL to solve Sudoku puzzles

In a recent post we celebrated the 10th anniversary of the declarative, formal language HLL. The language is used extensively in the railway signaling domain for the formal verification of interlocking logic and CBTC subsystems (such as zone controllers). In this more technical post we will familiarize the reader further with HLL, by formalizing the famous [...]

By |2019-07-11T09:08:21+01:00July 10th, 2019|Formal Methods, HLL – High Level Language|

HLL formal language celebrates 10 years

The formal language HLL (High Level Language) has emerged in recent years as a quite popular language for formal verification of safety-critical systems, especially in the railway signaling domain. This year marks the 10th anniversary of its conception. The history of HLL The language has its roots in the proof engine technologies developed by Prover in the 1980s (Stålmarck's [...]

By |2019-07-03T09:25:55+01:00June 30th, 2018|Formal Methods, HLL – High Level Language|

Performance issues with formal verification

We've all been there, waiting for the theorem prover to answer. Getting up for a cup of coffee, bugging a colleague... still no answer. This can be standard behaviour when doing formal verification. The requirements are difficult to prove, the system manages to escape into some dark corner not easily approached by the theorem prover. [...]

By |2018-06-05T13:51:24+01:00April 17th, 2018|Formal Methods|

Shift2Rail – The Work Package on Formal Methods and Standard Interfaces has Started

Back in March this year I wrote about a work package on formal methods and standard interfaces, led by the Swedish Transport Administration (Trafikverket, and part of the European Shift2Rail (S2R) Joint Undertaking. Since that time, the proposal for the overall project that includes this work package has been submitted and become approved, and the project started [...]

By |2021-11-20T11:58:15+01:00October 25th, 2017|Formal Methods, Standards|

Formal Methods for Railway Interlocking

In the early days of railway history there were no interlocking systems. It was considered enough to have personnel at the train stations manually observing trains and operating signals. The need for automatic signalling eventually became evident: human beings tend to make mistakes, which can lead to serious accidents, and the capacity of railroads was [...]

By |2017-10-13T12:16:04+01:00October 13th, 2017|Formal Methods, Signaling Solutions|

How to handle Complexity and Safety for Modern Railroads

The digitalized railway signaling systems of today are becoming increasingly complex with more and more functionality added to make better use of the existing infrastructure, while maintaining the highest level of safety. This also means that the task of assessing the safety and function of these system becomes more and more complex and often constitutes [...]

By |2017-10-11T09:18:12+01:00October 4th, 2017|Formal Methods, Signaling Solutions|
Go to Top