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 to collect knowledge of Formal Methods, based on an extensive survey of 130 international renowned experts. Based on their answers and comments were proposed a rigorous analysis on the past, present and future of formal methods in research, education and industry was presented.
According to a vast majority of the experts (almost 100%), Formal Methods are very important for building safety critical software. They contribute to the construction of trustworthy systems and are crucial for high-quality assessments. Moreover, 73,9 % respondents estimated that Formal Methods lead to better performance, 60% – lower cost and 56,9 % faster development.
Formal Methods are very important for safety critical software in the railway domain. The CENELEC EN 50128 standard recommends Formal Methods for the highest safety integrity level (SIL).
Stefan Resch (Thales Austria GmbH) – one of the invited speakers – highlighted successful applications of Formal Methods in the railway industry:
1) ERTMS Hybrid Level 3 (successful use of FMs for increasing track capacity in the railway network);
2) Checking European Train Control System (ETCS) Level 1 Lineside configuration data (many data errors can be caught in the early stages by using the Emerald approach);
3) TAS Control Platform (analyzing core safety and liveness properties of a fault-tolerant protocol by using model-checker).
A huge majority of the experts in the survey also agreed about the unique qualities of Formal Methods in providing correctness, which makes it incomparable to other methods such as artificial intelligence, quantum or molecular computing.
Regardless of the technical benefits of Formal methods, there are still several obstacles in making them more spread in the industry. The most important of them originates in financial and human factors.
Around 60% experts thought that the application of Formal methods is profitable only in medium and long terms. Immediate return is prevented by the high initial investment cost: “The real cost savings appear only later, with less and cheaper maintenance due to fewer failures”.
The human factor is another potential barrier for wider usage of Formal Methods in the industry. Formal Methods are depending on sufficiently high skill-levels and can be difficult to learn and deploy. According to the experts´ opinions, both managers and developers show a lack of knowledge in Formal Methods: “developers are reluctant to change their way of working”. Many experts also emphasized the lack of appropriate scientific/technical education. Expert Joost-Pieter Katoen underlined in his statement the need for “lightweight” Formal Methods.
The application of formal methods is foresee by many experts to spread in the future, not only to be applied in software engineering and computer science (69,2 %), but also in other science (biology, chemistry, epidemiology, etc. – 58,5 %), finance (digital currencies, smart contracts, etc. – 61,5%), in politics (e-voting, e-government, etc. – 43,8 %) and other parts of society – 31,5%.
Einar Broch Johnson claimed in his statement that formal methods can be applied “anywhere in science or society, where correct models matter”.
How safe and efficient are your rail control systems? Let’s find out!
Share this article
Learn more about how to develop specifications with Digital Twins
Fill out your information here.
More News & Articles
Prover PSL, the leading model checker used for formal verification in the rail and metro signaling domain, is now even faster.
Prover and RATP Strengthen Collaboration: Advancing Passenger Safety with Formal Methods.
Prover Certifier has now been certified by TÜV NORD as a CENELEC EN 50716-compliant T2 tool for SIL 4 applications.