Visible to the public Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware

TitleUsing TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware
Publication TypeConference Paper
Year of Publication2017
AuthorsResch, S., Paulitsch, M.
Conference Name2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)
KeywordsAlgorithm design and analysis, C code, C language, code generation, complex algorithms, composability, distributed algorithms, Fault tolerant systems, fault-tolerant distributed algorithms, formal methods, formal specification, formal verification, middleware, model checking, property-driven design, pubcrawl, rail traffic control, railway control applications, railway safety, railways, Redundancy, Resiliency, safety integrity level 4, safety-critical fault-tolerant middleware, safety-critical industries, safety-critical modules, safety-critical software, software architecture, software fault tolerance, software quality, software quality metrics, TAS Control Platform, TLA+, trusted platform modules

Creating and implementing fault-tolerant distributed algorithms is a challenging task in highly safety-critical industries. Using formal methods supports design and development of complex algorithms. However, formal methods are often perceived as an unjustifiable overhead. This paper presents the experience and insights when using TLA+ and PlusCal to model and develop fault-tolerant and safety-critical modules for TAS Control Platform, a platform for railway control applications up to safety integrity level (SIL) 4. We show how formal methods helped us improve the correctness of the algorithms, improved development efficiency and how part of the gap between model and implementation has been closed by translation to C code. Additionally, we describe how we gained trust in the formal model and tools by following a specific design process called property-driven design, which also implicitly addresses software quality metrics such as code coverage metrics.

Citation Keyresch_using_2017