Testing Implementations of Formally Verified Algorithms

• Algorithms described in literature can often be used to solvepractical, industrial problems. In safety-critical industrialsettings, algorithms that have been formally verified should be evenmore attractive candidates for implementations. Nevertheless, weobserve little transfer of algorithms from research papers intoproducts. In this paper we describe a case study on the implementationof algorithms for the widely known and broadly studied problem ofleader election. Despite thousands of articles on that topic, itstill requires a lot of engineering to select the relevant articles,and get a correct algorithm implemented in an industrial setting.Modifications are necessary to meet all requirements. We proposeadaptation and testing of formal properties as a realistic and cheap way tocheck the correctness of the modifications, since performing a formalproof seems unrealistic for industrial systems. We show how we use theproperties stated in the articles to guide our tests.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Software Engineering (hsv//eng)

Publikations- och innehållstyp

kon (ämneskategori)

ref (ämneskategori)