Konuşmacı: Ferhat Erata, UNIT Information Technologies R&D Ltd.

Başlık: 
Yazılım Tasarımlarının Biçimsel Modellemesi, Analizi ve Gerçekleştiriminin Doğrulanması
 
Özet:
Bu oturuma, kritik sistemlerin yüksek kesinlikle doğrulanmasında biçimsel yöntemlerin kullanımına dair otomotiv ve havacılık endüstrisinden örnekler sunularak bir başlangıç yapılacaktır. Daha sonra, gereksinimlerden başlayarak seçilen bir özyinelemeli veri yapsının temel operasyonları ve yapısal özellikleri birinci derece ilişkisel mantık (first-order relational logic) kullanılarak biçimsel modellenecek ve doğruluğu analiz edilecektir. Sonrasında, bu tasarım ve yapılan analiz temel alınarak veri yapsının nesne yönelimli bir gerçekleştirimini model sınama (model checking) ve sembolik işletim (symbolic execution) ile doğruluğunun sınanması gösterilecektir. 
 
Bu oturumda kullanılacak araçlar aşağıda listelenmiştir:
 
* Gereksinimlerin analizi için Z3 (https://github.com/Z3Prover/z3) SMT çözümleyicisi,
* Seçilen veri yapısının biçimsel modellenmesi ve analiz için Alloy (https://github.com/AlloyTools/org.alloytools.alloy) ve AlloyInEcore (https://modelwriter.github.io/AlloyInEcore/) araçları,
* Gerçekleştirimin sınanması için Java PathFinder (https://github.com/javapathfinder/jpf-core) ve Symbolic PathFinder (https://github.com/SymbolicPathFinder/jpf-symbc) araçları kullanılacaktır.