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

Implementing an LTL-to-Büchi translator in Erlang: a ProTest experience report

Hans Svensson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Proceedings of the 8th ACM SIGPLAN workshop on ERLANG p. 63-70. (2009)
[Konferensbidrag, refereegranskat]

In order to provide a nice user experience in McErlang, a model checker for Erlang programs, we needed an LTL-to-Büchi translator. This paper reports on our experiences implementing a translator in Erlang using well known algorithms described in literature. We followed a property driven development schema, where QuickCheck properties were formulated before writing the implementation. We successfully implement an LTL-to-Büchi translator, where the end result performs on par (or better) than two well known reference implementations.

Nyckelord: Testing and model checking



Denna post skapades 2010-01-20. Senast ändrad 2016-07-21.
CPL Pubid: 109167

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)

Ämnesområden

Programvaruteknik

Chalmers infrastruktur