Kada atsirado?
• ”Neformaliai” įkurta apie 2020 metus
• Grupės nariai: Haroldas Giedra, Saulius Gražulis, Irus Grinis, Linas Laibinis, Karolis Petrauskas, Viačeslav Pozdniakov, Tomas Ustinavičius
• Steigiamos grupės vadovas – Linas Laibinis
• Formalieji metodai – matematiškai griežti (pagrįsti) programų ir
kompiuterinių sistemų specifikavimo/modeliavimo, kūrimo ir verifikavimo metodai
• Tiltas tarp teorinių pagrindų (Theoretical Computer Science) ir jų praktinių taikymų
Motyvacija
• Modernios programų sistemos tampa vis sudėtingesnės
• Sunku suprasti ir verifikuoti (t.y,patikrinti jų korektiškumą)
• Sistemos yra vis daugiau naudojamos kritinėse srityse, kur
klaidos kaina gali būti labai didelė
• Ar mes galime pasitikėti tokiomis sistemos ir jų programine įranga?
Tematika
• Kompiuterinių ar programų sistemų modeliavimas ir verifikavimas
• Algoritmų korektiškumo įrodymai (formalios semantikos rėmuose)
• Automatizuoto teoremų įrodymo ar modelių patikrinimo įrankių
(TLA+, Isabelle/HOL, Coq, Uppaal, Ada Sparc, …) panaudojimas
• Modalinės, laiko ir aukštesnės eilės logikos ir jų taikymai
• Išskirstytų sistemų, kompiuterinių tinklų ar telekomunikacinių sistemų
algoritmų/protokolų verifikavimas
• Geležinkelio signalizavimo sistemų verifikavimas
• Išskirstytų programų ar kompiuterinių sistemų skaitinis įvertinimas
Formalieji modeliai
• Remiasi sistemos objektų, būsenų ir jų pasikeitimų formaliu (matematiniu)
atvaizdavimu. Kitais žodžiais – apibrėžta formalia semantika
• Leidžia formalizuotų sistemos savybių (reikalavimų) verifikavimą (kas yra ar
tampa sertifikavimo reikalavimu daugelyje kritinių pritaikymo sričių)
• Daug formalaus modeliavimo kalbų: Z, VDM, TLA, B Method, Event-B, Alloy, Promela, Uppaal, ir t.t.
• Matematinė bazė: aibių teorija, predikatų, modalinės ir aukštesnės eilės logikos, tikimybių teorija, automatų teorija, būsenų perėjimo sistemos, ir t.t.
Formalusis verifikavimas
• Remiasi (automatizuotu) teoremų įrodymu ir modelių patikrinimu
• Modelių patikrinimas: automatinis perėjimas per sugeneruotas sistemos būsenas; Greitesni rezultatai, bet galimas būsenų skaičiaus „sprogimas“
• Teoremų įrodymas: matematinis/loginis įrodymas, kad modelio savybės galioja visose sistemos būsenose; Reikalauja daugiau pastangų, duoda stipresnę garantiją
• Automatizuotos aplinkos ar įrankiai palengvinantys verifikavimą: TLA+,
Isabelle, Coq, SparcAda, Atelier-B, Rodin platform, Spin, Uppaal, PRISM, nuSMV, Perfect Developer, AADL, Mobius, t.t.
Pasibaigę tyrimai ir studentų projektai
- Sesijų koordinavimo algoritmas (TLA+, skaitinis įvertinimas)
- Telekomukacijos paslaugų priklausomybių analizė (TLA+)
- Paxos algoritmo modifikacija nepatikimiems tinklams (TLA+)
- Buridano logikos verifikavimas (teoremų įrodymas)
- Geležinkelio signalizavimo sistemos verifikavimas (teoremų įrodymas, su partneriais iš Didžiosios Britanijos)
- Redis Cluster podėlio sistemos formali analizė (TLA+)
- Programų korektiškumo teorijos (Refinement Calculus) formalizavimas Coq teoremų įrodymo sistemoje (su bak. M. Sauliumi)
- Daiktų internet sistemos verifikavimas statistinio modelių tikrinimo metodais (su mag. N. Jarmolenka)
Vykstantys tyrimai ir studentų projektai
- Algoritmų korektiškumo įrodymai kristalografijos srityje (Isabelle/HOL teoremų įrodymas su Isabelle/HOL)
- Telekomukacijos paslaugų priklausomybių analizė (Isabelle/HOL teoremų įrodymo sistema)
- Geležinkelio signalizavimo sistemos diagnostika formalaus verifikavimo pagrindu (su partneriais iš DB)
- Modelių tikrinimas randomizuotam konsensuso algoritmui (TLA+);
- IOTA išplėsto UTXO modelio verifikavimas (Isabelle/HOL, su mag. E. Dlugausku);
- Specifikacijų optimizavimas modelių tikrinimui (TLA+, su mag. M. Jasinsku);
- Specifikacijų susiejimas su Elixir programiniu kodu (TLA+, su mag. D. Bražėnu ir A. Maliuginu).
Grupės narių ir jų partnerių straipsniai
- K.Petrauskas, A.Merkys, A.Vaitkus, L.Laibinis and S.Gražulis, Proving the Correctness of the Algorithm for Building a Crystallographic Space Group, Journal of Applied Crystallography, pages 515 – 525, IUCr,
2022. - L.Laibinis, A.Iliasov, A.Romanovsky. Mutation Testing for Rule-Based Verification of Railway Signalling
Data. IEEE Transactions on Reliability, Volume 70(2), pages 676-691, IEEE, 2021. - A. Iliasov, D. Taylor, L. Laibinis and A. Romanovsky, Practical Verification of Railway Signalling Programs, IEEE Transactions on Dependable and Secure Computing, 2022, doi:10.1109/TDSC.2022.3141555.
- J.Dagys, A.Pabijutaite, H.Giedra, Representing Buridan’s Divided Modal Propositions in First-Order Logic, History and Philosophy of Logic, 2022.
- A.Iliasov, A.Romanovsky, and L.Laibinis. Quantitative Validation of Formal Domain Models. In 19th IEEE Int. Symposium on High Assurance Systems Engineering, HASE 2019, Hangzhou, China, pages 17–24. IEEE, 2019.
Kristalografinio algoritmo verifikavimas
- K.Petrauskas, A.Merkys, A.Vaitkus, L.Laibinis and S.Gražulis, “Proving the correctness of the algorithm for building a crystallographic space group”, Journal of Applied Crystallography, 2022
- Kristalografinių duomenų apdorojimo alogoritmo korektiškumo formalus verifikavimas (naudojant teoremų įrodymų sistemą Isabelle/HOL)
- Plačiai naudojamas kristalografiniuose skaičiavimuose algoritmas generuojantis ar rekonstruojantis erdvinės grupės operatorių sąrašą.
Tolimesni planai
• Daugiau straipsnių 🙂
• Didesnis studentų įtraukimas į grupės veiklą
• Aktyvesnis dalyvavimas konferencijose / projektuose (šiuo metu esame COST Action CA20111 “European Research Network on Formal Proofs” nariai)
(paskutinį kartą redaguotas 2023 m. sausio 13)