TLA+ specifikacijų išskyrimas iš Elixir programos

Abstract

Šiame tyrime yra nagrinėjamas metodas, padedantis užtikrinti Elixir programos atitikimą programinės įrangos inžinieriaus kurtai TLA+ specifikacijai. Kuriant metodą apibrėžtas vertimo taisyklių rinkinys, skirtas TLA+ specifikacijų išskyrimui iš nuosekliosios išskirstyto Elixir algoritmo dalies. Naudojant sudarytas taisykles, buvo įgyvendintas vertimo įrankis, Elixir kodą paverčiantis į TLA+ specifikaciją. Sugeneruotos specifikacijos teisingumas tikrinamas modelio tikrinimu ir tikslinimu, o teisingas vertimo įrankio veikimas užtikrinamas konvertuojant sugeneruotą specifikaciją atgal į Elixir kodą ir vykdant pirminės programos vienetų testus.