Пројекат 144029

Модели, језици, типови и процеси у рачунарству

Руководилац: Проф. Силвиа Гилезан

 

Резиме

Технологија за конструкцију поузданих и коректних рачунарских система је од велике важности за развој индустрије. Ово је дугорочан проблем који захтева развој у многим областима. Употреба формалних метода за спецификацију и испитивање рачунарских  система и програмских језика чини део решења овог проблема. Наше истраживачке активности  усмерене су на примену теорије типова и теорије доказа у рачунарству, на развој модела, језика и процеса у глобалном рачунарству и на дигиталну обраду слике.  У склопу овог пројекта бавићемо се конструктивним интерпретацијама класичне логике које су у основи прогамских језика.  Развијаћемо технике за формално резоновање засноване на теорији типова и теорији доказа. Испитиваћемо технике програмских језика за глобално рачунарство и  развијаћемо моделе дистрибутивних мобилних система. Такође ћемо развијати  ефикасне методе за кодирање дигиталних објеката.

Учесници овог Пројекта су укључени у рад два текућа европска пројекта од којих је један FP6 IST-FET пројекат TYPES-Types for Proofs and Programs, FP6-510996, (2004.-2007.год)  а други пројекат је из CEEPUS II програма "Medical imaging & Medical information processing", CII-AT-0042-01-0506, (2005.-2007.год). На тај начин ће рад на овам Пројекту бити директно укључен у актуелна међународна истраживања у овом домену.

 

Предмет истраживања

Пројекат је усмерен на истраживања у следећим областима:

Теорија типова је основа програмских језика са типовима, као што су Java, OCAML, Haskell, ML. Теорија типова је уједно и алтернатива теорији скупова у заснивању математике. Базирана је на структуирању типова да би се избегла некохерентност. Истраживања у конструктивној математичкој логици, која је у основи теорије типова, су у последње две деценије поново у жижи интересовања због њихове примене у рачунарству. У оквиру овог Пројекта предлажемо испитивање  конструктивних интерпретација класичне логике, којe су до сада недовољно истражене, а у основи су програмског језика SCHEME. Посебну пажњу ћемо посветити операторима контроле и сепарације и карактеризацији јаке нормализације у том рачуну, што у програмском језику базираном на тим рачунима одговара завршетку коректно написаног програма. Уз то, бавићемо се и моделима заснованим на теорији типова. Концепти подтипа, изоморфизма међу типовима, као и ретракција типова ће такође бити предмет нашег истраживања. Ови концепти су  од великог значаја у истрaживањима основа рачунарства, јер дају ефикасна решења  како у домену безбедности, тако и у домену поузданости. У домену примене теорије типова у доказивачу теорема COQ бавићемо се рачуном конструкција чију основну карактеристику чине типови који зависе од других типова и других вредности. Наша истраживања ће бити у формализацији математике помоћу COQ-а. Такође бавићемо се репрезентацијама доказа у структурама теорије категорија блиским геометрији и применама резултата добијених у нормализацији и одлучивању доказа. Истраживања у овом домену ће бити повезана са истраживањима у оквиру европског FP6 IST-FET пројекта TYPES-Types for Proofs and Programs, FP6-510996, (2004.-2007.год) у коме учествују чланови овог пројекта.

Под појмом глобални рачунарски системи се подразумевају инфраструктуре глобалне светске рачунарске мреже (Internet, World Wide Web). Глобални рачунарски системи постају све сложенији с обзиром на своју распрострањеност и неминовност у данашњем свету. Нова концепцијска димензија рачунарства, у којој ентитети распрострањени широм света размењују податке, крећу се са једне на другу локацију и међусобно комуницирају, је добила важну улогу и захтева одговарајућу теоретску основу засновану на математичком моделирању. Глобално рачунарство се бави моделирањем и дизајнирањем глобалних рачунарских система. Истраживања су усмерена на системе који имају следеће карактеристике:     - Системи који су сачињени од аутономних целина у којима активност није централно контролисана, зато што је глобална контрола немогућа или зато што различити корисници стварају те целине.  
   
- Целине које су мобилне и то двојако,   унутар једне платформе или између различизих плаформи. 
    - Конфигурације које се мењaју током времена тако што је систем отворен за стварање нових целина, али и за њихово уклањање.
     - Системи који раде са непотпуном информацијом о околини,  јер информације брзо застаревају, а мобилност захтева откривање информација о околини.

Рачунарска обрада слике је савремена област у оквиру математике и рачунарства, која налази широку примену у многим другим областима, пре свега у медицини. Савремена средства за добијање дигиталне слике (CT, MRA, PET) захтевају и нове методе за њену обраду. Приступ заснован на моделирању дигиталних слика фази-скуповима у том смислу нуди моћно средство, посебно захваљујући подршци развијене рачунарске технологије. Избегавањем класичног бинарног приступа, дозвољавајући делимично припадање елемента (фази-)скупу, очувава се драгоцена информација која се даље може користити у процесу обраде слике. На тај начин значајно се повећава поузданост и прецизност добијених резултата. Примена фази-скупова у анализи облика захтева истраживања у области математичког моделирања дискретних фази облика и њихових релевантних особина. Док је теорија фази-скупова над непрекидним доменом добро развијена, дискретни фази-скупови, који су неизбежни у примени у рачунарској обради слика, су далеко мање изучавани. Такође је потребно развијати алгоритме за ефикасан рад са великом количином података, присутном у фази-репрезентацијама. Истраживања у овом домену ће бити повезана са истраживањима у оквиру европског CEEPUS II програма, на  Пројекту "Medical imaging & Medical information processing", CII-AT-0042-01-0506, (2005.-2007.год) у коме учествују чланови овог Пројекта.

 

Значај планираних истраживања

Предложене истраживачке теме спадају у три области које су од великог значаја у савременом информатичком друштву. Овим је јасно истакнут и значај истраживања у оквиру Пројекта.  Теорија типова је уграђна у основе рачунарства, глобално рачунарство је незаобилазан и све присутнији концепт у нашем модерном свету, а рачунарска обрада слика је постала једна од важнијих области примене рачунарства у свекодневном животу. Активан рад међународних научно-истраживачких тимова у оквиру свих ових области илуструје актуелност предложеног Пројекта.  Намера је да се обједињавањем ових тема у оквиру једног пројекта обезбеде услови за међусобну сарадњу истраживача,  интеракцију њиховог истраживања и међусобну стимулацију.  Значајна заједничка тачка истраживачких тема је њихова заснованост на математици и математичким моделима.  Планирано истраживање  ће ићи у правцу развијања математичких модела, као и у правцу различитих примена развијених модела.  Међусобна зависност теоријских резултата и захтева праксе биће и покретачка снага, и значајан резултат планираних истраживања.

Значајан аспект је и наставак и продубљивање међународне научно-истраживачке сарадње  са водећим стручњацима са Универзитета у Торину,  ENS у Лиону, Универзитета у Упсали, и другим академским институцијама са којима је истраживачки тим већ успоставио успешне контакте.

 

Циљеви истраживања и планирани резултати

Циљеви истраживања за сваку од предложених тема су:

1. Примена теорије типова у рачунарству:

  2. Глобално рачунарство:

 3. Обрада дигиталних слика:

 Очекивани резултати пројекта су значајан број публикација у међународним часописима, као и друге публикације. Уз то, очекује се и наставак постојеће успешне међународне сарадње. Нека истраживања у склопу овог пројекта подржана су FP6 и CEEPUS пројектима. Настојаћемо да своја истраживања у глобалном рачунарству укључимо у неки међународни програм.