CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Testing Implementations of Formally Verified Algorithms

Thomas Arts (Institutionen för tillämpad informationsteknologi (Chalmers)) ; Koen Claessen (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)) ; John Hughes (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)) ; Hans Svensson (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Proceedings of the 5th Conference on Software Engineering Research and Practice in Sweden (2005)
[Konferensbidrag, refereegranskat]

Algorithms described in literature can often be used to solve practical, industrial problems. In safety-critical industrial settings, algorithms that have been formally verified should be even more attractive candidates for implementations. Nevertheless, we observe little transfer of algorithms from research papers into products. In this paper we describe a case study on the implementation of algorithms for the widely known and broadly studied problem of leader election. Despite thousands of articles on that topic, it still 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 propose adaptation and testing of formal properties as a realistic and cheap way to check the correctness of the modifications, since performing a formal proof seems unrealistic for industrial systems. We show how we use the properties stated in the articles to guide our tests.



Denna post skapades 2006-08-25. Senast ändrad 2013-08-12.
CPL Pubid: 11248