# Formaliųjų metodų mokslinė grupė

## 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 – [u]linas.laibinis[/u]
- 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ų

## 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)



## Kontaktai
Vadovas: [u]{psn}linas.laibinis[/u] (linas.laibinis@mif.vu.lt)