Testing Implementations of Formally Verified Algorithms

Arts, Thomas,1969Chalmers tekniska högskola,Chalmers University of Technology (författare)

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.

Lindström Claessen, Koen,1975Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)koen (författare)
Hughes, John,1958Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)rjmh (författare)
Svensson, Hans,1979Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)hanssv (författare)
Chalmers tekniska högskola (creator_code:org_t)

Ingår i:Proceedings of the 5th Conference on Software Engineering Research and Practice in Sweden

Av författaren/redakt...: Arts, Thomas, 19 ...; Lindström Claess ...; Hughes, John, 19 ...; Svensson, Hans, ...

Om ämnet

NATURVETENSKAP: NATURVETENSKAP; och Data och informa ...; och Programvarutekni ...

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.