Scienca Esplora Grupo pri Formalaj Metodoj
Kiam ĝi aperis?
- “Neformale” fondita ĉirkaŭ 2020
- Membroj de la grupo: Haroldas Giedra, Saulius Gražulis, Irus Grinis, Linas Laibinis, Karolis Petrauskas, Viačeslav Pozdniakov, Tomas Ustinavičius
- Fondanta gvidanto de la grupo – Linas Laibinis
- Formalaj metodoj – matematike striktaj (bazitaj) metodoj por la specifado/modelado, konstruado kaj verifikado de programoj kaj komputilaj sistemoj
- Ponto inter teoriaj fundamentoj (Teoria Komputado) kaj iliaj praktikaj aplikoj
Motivado
- Modernaj programaj sistemoj fariĝas ĉiam pli kompleksaj
- Malfacilas kompreni kaj verifiki ilin (t.e., kontroli ilian ĝustecon)
- Tiaj sistemoj estas ĉiam pli ofte uzataj en kritikaj kampoj, kie la kosto de eraro povas esti tre granda
- Ĉu ni povas fidi je tiaj sistemoj kaj ilia programaro?
Temoj
- Modelado kaj verifikado de komputilaj aŭ programaj sistemoj
- Pruvado de algoritmoj ĝusteco (kadre de formalaj semantikoj)
- Uzado de aŭtomatigitaj teoremapruviloj aŭ modelkontroliloj (TLA+, Isabelle/HOL, Coq, Uppaal, Ada Sparc, …)
- Modalaj, tempaj kaj pli altordaj logikoj kaj iliaj aplikoj
- Verifikado de algoritmoj/protokoloj por disaj sistemoj, komputilaj retoj aŭ telekomunikaj sistemoj
- Verifikado de fervojaj signalaj sistemoj
- Nombra taksado de disaj programoj aŭ komputilaj sistemoj
Formalaj modeloj
- Bazas sin sur formala (matematika) reprezentado de objektaj stato kaj iliaj ŝanĝoj. Alivorte – difinita formala semantiko
- Ebligas verifikadon de formaligitaj sistemaj trajtoj (postuloj), kio fariĝas postulo por atestado en multaj kritikaj aplikaj kampoj
- Multaj formalaj modeligaj lingvoj: Z, VDM, TLA, B Metodo, Event-B, Alloy, Promela, Uppaal, ktp.
- Matematika bazo: teorio de aroj, predikata, modala kaj altordaj logikoj, probabla teorio, aŭtomata teorio, sistemoj de ŝtato-transiro, ktp.
Formala verifikado
- Bazas sin sur (aŭtomatigita) teoremapruvado kaj modelkontrolo
- Modelkontrolo: aŭtomata esplorado de generitaj statoj de la sistemo; pli rapidaj rezultoj, sed eblas “eksplodo” de la nombro de statoj
- Teoremapruvado: matematika/logika pruvo ke propraĵoj de la modelo validas en ĉiuj statoj de la sistemo; postulas pli da peno, donas pli fortan garantion
- Aŭtomatigitaj medioj kaj iloj por helpi la verifikadon: TLA+, Isabelle, Coq, SparcAda, Atelier-B, Rodin platform, Spin, Uppaal, PRISM, nuSMV, Perfect Developer, AADL, Mobius, ktp.
Finitaj esploroj kaj studentaj projektoj
- Algoritmo por kunordigo de seancoj (TLA+, nombra taksado)
- Analizo de dependecoj en telekomunikaj servoj (TLA+)
- Modifado de Paxos-algoritmo por nefidindaj retoj (TLA+)
- Verifikado de logiko de Buridano (teoremapruvado)
- Verifikado de fervoja signalada sistemo (teoremapruvado, kun partneroj el Britio)
- Formala analizo de Redis Cluster-kaŝmemora sistemo (TLA+)
- Formaligo de teorio pri programkorekteco (Refinement Calculus) en teoremapruva sistemo Coq (kun bak. M. Saulius)
- Verifikado de Interreto-de-aĵoj-sistemo per statistikaj modelkontrolaj metodoj (kun mag. N. Jarmolenka)
Aktualaj esploroj kaj studentaj projektoj
- Pruvado de algoritmoj ĝusteco en kristalografio (Isabelle/HOL)
- Analizo de dependecoj en telekomunikaj servoj (Isabelle/HOL)
- Diagnostiko de fervoja signalada sistemo surbaze de formala verifikado (kun partneroj el Britio)
- Modelkontrolo por randomigita konsensa algoritmo (TLA+)
- Verifikado de la etendita UTXO-modelo de IOTA (Isabelle/HOL, kun mag. E. Dlugauskas)
- Optimumigo de specifoj por modelkontrolo (TLA+, kun mag. M. Jasinskas)
- Kunligo de specifoj kun programkodo en Elixir (TLA+, kun mag. D. Bražėnas kaj A. Maliuginas)
Artikoloj de grupanoj kaj iliaj partneroj
- K. Petrauskas, A. Merkys, A. Vaitkus, L. Laibinis, S. Gražulis, Proving the Correctness of the Algorithm for Building a Crystallographic Space Group, Journal of Applied Crystallography, paĝoj 515–525, IUCr, 2022
- L. Laibinis, A. Iliasov, A. Romanovsky. Mutation Testing for Rule-Based Verification of Railway Signalling Data, IEEE Transactions on Reliability, Vol. 70(2), paĝoj 676–691, IEEE, 2021
- A. Iliasov, D. Taylor, L. Laibinis, 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, L. Laibinis, Quantitative Validation of Formal Domain Models, 19-a IEEE Internacia Simpozio pri Altfidindaj Sistemaj Inĝenieradoj, HASE 2019, Hangzhou, Ĉinio, paĝoj 17–24. IEEE, 2019
Verifikado de kristalografia algoritmo
- K. Petrauskas, A. Merkys, A. Vaitkus, L. Laibinis, S. Gražulis, Proving the correctness of the algorithm for building a crystallographic space group, Journal of Applied Crystallography, 2022
- Formala verifikado de la korekteco de algoritmo por prilaborado de kristalografiaj datumoj (uzante teoremapruvan sistemon Isabelle/HOL)
- Algoritmo vaste uzata en kristalografiaj kalkuloj por generi aŭ rekonstrui liston de operacioj de spaca grupo
Estontaj planoj
- Pli da artikoloj 🙂
- Pli granda engaĝiĝo de studentoj en la agado de la grupo
- Pli aktiva partopreno en konferencoj / projektoj (nuntempe ni estas membroj de COST Action CA20111 “European Research Network on Formal Proofs”)
(laste redaktita: la 15-a de majo 2025)