Invited Speakers
Joint FMICS / FM-RAIL-BOK Keynote
Twenty-Five Years of Formal Methods and Railways: What Next?
Alessandro Fantechi, Università di Firenze
Railway signaling is now since more than 25 years the subject of successful industrial application of formal methods in the development and verification of its computerized equipment.
However the evolution of the technology of railways signaling systems in this long term has had a strong influence on the way formal methods can be applied in their design and implementation. At the same time important advances had been also achieved in the formal methods area.
The evolution of railways signaling systems has seen railways moving from a protected market based on national railway companies and national manufacturers to an open market based on international standards for interoperability, in which systems of systems are providing more and more complex automated operation, but maintaining, and even improving, demanding safety standards.
The scope of the formal methods discipline has enlarged from the methodological provably correct software construction of the beginnings to the analysis and modelling of increasingly complex systems, always on the edge of the ever improving capacity of the analysis tools, thanks to the technological advances in formal verification of both qualitative and quantitative properties of such complex systems.
In spite of these advances, the verification of complex railway signalling systems is still a main challenge and an important percentage of the cost in the development of these systems. We will discuss a few examples of such systems that witness these difficulties.
The thesis we will put forward in this talk is that the complexity of future railway systems of systems can be addressed with advantage only by a higher degree of distribution of functions on local interoperable computers - communicating by means of standard protocols - and by adopting a multi-level formal modelling suitable to support the verification at design time and at different abstraction levels of the safe interaction among the distributed functions.
FMICS Keynote
TrustInSoft: Industrial Formal Methods to Protect Security-Sensitive Systems
Benjamin Monate, TrustInSoft
TrustInSoft is a start-up founded in 2013. It provides formal method-based solutions to help software publishers and integrators develop secure systems. In this talk I will explain the challenges we are facing as the software publisher of the Open Source platform Frama-C. I will discuss a few questions:
- Can theoretically well-founded formal methods be applied without compromises in non-regulated industrial domains?
- Who in the industry is ready to pay for formal security?
- Can a start-up afford an ambitious research roadmap in formal methods?
