Технологија за конструкцију поузданих и коректних рачунарских система је од велике важности за развој индустрије. Ово је дугорочан проблем који захтева развој у многим областима. Употреба формалних метода за спецификацију и испитивање рачунарских система и програмских језика чини део решења овог проблема. Наше истраживачке активности усмерене су на примену теорије типова и теорије доказа у рачунарству, на развој модела, језика и процеса у глобалном рачунарству и на дигиталну обраду слике. У склопу овог пројекта бавићемо се конструктивним интерпретацијама класичне логике које су у основи прогамских језика. Развијаћемо технике за формално резоновање засноване на теорији типова и теорији доказа. Испитиваћемо технике програмских језика за глобално рачунарство и развијаћемо моделе дистрибутивних мобилних система. Такође ћемо развијати ефикасне методе за кодирање дигиталних објеката.
Учесници овог Пројекта су укључени у рад два текућа европска пројекта од којих је један 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 пројектима. Настојаћемо да своја истраживања у глобалном рачунарству укључимо у неки међународни програм.