Atkarpomis tiesinių agregatų transformacija į PROMELA kalbą
Myžetis, Kęstutis |
Atkarpomis tiesinių agregatų (PLA) metodas paremtas semantine matematinio modelio taikymu specifikuoti sistemas. Norint jas verifikuoti - vienas iš įrankių yra Spin. Pastarasis supranta PROMELA kalba parašytą specifikaciją. Tai siekiamas uždavinys - transformuoti PLA specifikaciją į PROMELA kalbą. Transformacijos vyksmui išanalizavę PLA specifikaciją, pasiūlėme modifikacijas, kurias įtakoja programavimo kalba Python ir siekiami identifikuoti atributai. Atliekama programos transformavimo metodu – interpretuojame PLA specifikacija kaip programos kodą ir verčiame į PROMELA kalbą. Transformacijos metu siekiama išlaikyti semantinę uždavinio prasmę ir vykdant sudėtingesnės abstrakcijos vertimą į žemesnę atliekame: detalizavimą, architektūros ištraukimą, duomenų srauto analizę, sudalinimą, normalizaciją ir optimizaciją. Transformacijai atlikti sukurta programa, kuri automatiškai, pagal modifikuota PLA specifikaciją, verčia į PROMELA kabą. Vartojo patogumui suteikta grafinė sąsaja, kurioje galima atlikti pagrindinius veiksmus:įkelti, rašyti, saugoti modifikuot PLA specifikaciją,o taip pat matyti tarpinius veiksmus ir duomenų saugojimo srukturą.
Piece-Linear Aggregates (PLA) method based on semantic mathematical model to specify the application systems. In order to verify them - one of the tools are Spin. It understands specification written in PROMELA language. The main purpose is to transform the PLA specification to PROMELA language. In transformation process have analyzed the PLA specification and suggested modifications, which affects by Python programming language and attributes seeking to identify. We use program transformation method - interpretation of the PLA specification as program code and convert to PROMELA language. In this process we trying to keep task semantic meaning and to transform from complex abstractions into a lower we use: specification, architecture extraction, data flow analysis, division, normalization and optimization. Created program, witch automatically transforms modified PLA specification to PROMELA language. User friendly graphical interface is provided, witch can perform the basic steps: upload, post, store the modified PLA specification, but also shows the intermediate steps, and data storage sructure.