Page 13 - GP_02_2010
P. 13
MAGRODY
Crystall, zaprojektowano rygory- klaratywnej synchronizacji oraz dy- chunku zadań atomowych, w tym
styczne specyfikacje protokołów namicznej aktualizacji protokołów w dowód dynamicznej poprawności
dynamicznej konstrukcji grupowej systemach komunikacyjnych. Mogą przykładowego algorytmu sterowa-
oraz przeprowadzono dowody po- one służyć do budowy systemów nia współbieżnością.
prawności wybranych protokołów. komunikacyjnych z modularnych
Zaprojektowano i wdrożono nowy, protokołów, które można zastę- Dorobek naukowy dra hab. inż.
w pełni modularny system komuni- pować dynamicznie. Komunikacja P.T. Wojciechowskiego stanowi 38
kacji grupowej Fortika, przeznaczo- umożliwia użyteczne aplikacje, ale publikacji: 2 rozprawy, 2 rozdziały
ny do budowy odpornych na awarie jednocześnie sprawia, że imple- w książkach, 18 artykułów opubli-
serwerów aplikacji rozproszonych. mentacja atomowości, synchroni- kowanych w materiałach recenzo-
W Fortika zastosowano nowe mo- zacji i dynamicznej aktualizacji nie wanych konferencji międzynaro-
dularne protokoły komunikacji gru- jest łatwa. Aby ułatwić programo- dowych, artykuł w czasopiśmie,
powej. Pozwala ona na budowę wanie oraz móc zagwarantować 9 raportów naukowych oraz 3 inne.
aplikacji ze wsparciem zarówno niezawodność, nowe abstrakcje Spośród tych publikacji 10 zostało
modeli awarii typu crash – stop programistyczne są potrzebne. opublikowanych w materiałach na-
(stosowanych dotychczas w innych W rozprawie zaprojektowano rachu- ukowych z listy filadelfijskiego In-
systemach komunikacji grupowej) nek (ang. calculus) zadań atomo- stytutu Informacji Naukowej.
jaki i crash – recovery, tj. z odtwa- wych, tj. transakcji atomowych bez
rzaniem stanu serwera, który uległ odtwarzania stanu, mogących mieć Dr hab. inż. Teofil Jesionowski,
awarii. W projekcie Crystall dr hab. efekty wejścia/wyjścia oraz opisano Wydział Technologii Chemicznej,
inż. Wojciechowski zaproponował nowe algorytmy przeznaczone do otrzymał nagrodę w kategorii Tech-
zbudowanie frameworku protoko- sterowania współbieżnością w za- nologia Chemiczna za cykl prac
łowego, który pozwalałby na bu- daniach atomowych. Rachunek ten ,,Tlenkowe układy hybrydowe –
dowę systemów rozproszonych, wyposażony jest w system typów technologie otrzymywania, wła-
w których protokoły mogą byś do statycznej weryfikacji danych ściwości i zastosowania”. Badania
zmieniane dynamicznie, tj. w trak- wymaganych przez te algorytmy. nad nową generacją tlenkowych
cie działania systemu. Wynikiem System typów gwarantuje, że pro- układów hybrydowych mają olbrzy-
prac w tym kierunku jest frame- ponowane w rachunku konstruk- mie znaczenie dla rozwoju nauki,
work SAMOA, który oferuje abs- cje programistyczne są używane w szczególności technologii che-
trakcję programistyczne i biblioteki, w sposób prawidłowy. Następnie micznej, inżynierii materiałowej
które pozwalają na budowę proto- opisano dwa różne podejścia do i szeroko rozumianej ochrony śro-
kołów sieciowych w sposób mo- synchronizacji deklaratywnej: (1) dowiska. W ten niezwykle istotny
dularny, z możliwością dynamicz- rachunek kombinatorów współ- obszar badań naukowych i technicz-
nej zamiany protokołów w sposób bieżności z opartą na typach wery- nych wpisują się zagadnienia zwią-
całkowicie transparentny dla usług fikacją spełnialności kombinatorów zane z syntezą funkcjonalizowanych
korzystających z tych protokołów. (co daje gwarancję ich poprawnego substancji krzemionkowych, krze-
SAMOA została użyta do imple- zastosowania) oraz (2) język ograni- mianowych i międzytlenkowych,
mentacji AGC – adoptowalnego czeń (ang. constraint language) dla ich charakterystyką fizykochemicz-
systemu komunikacji grupowej, modelu synchronizacji opartego na ną oraz zastosowaniem. Opubliko-
opartego na protokołach z Forti- rolach. Opisano także model dyna- wany cykl prac (m.in. w Dyes and
ka, przystosowanych do modelu micznej aktualizacji protokołów oraz Pigments, Journal of Power Sour-
kompozycji i interakcji istniejącego podano dwa przykładowe algoryt- ces, Journal of Materials Science,
w SAMOA. my przełączania protokołów, mają- Environmental Science and Tech-
ce określone pożądane własności. nology, Journal of Materials Pro-
W nagrodzonej rozprawie habi- Wreszcie zaprojektowano, oparty cessing Technology, Advanced
litacyjnej „Language Design for na klasach, obiektowy rachunek Powder Technology czy Colloid and
Atomicaly, Declarative Synchro- wiązań dynamicznych. Rachunek Polymer Science) dotyczy otrzymy-
anization, and Dynamic Update posłużył do pokazania zastosowań wania sferycznych, monodysper-
in Communicating Systems” zajął mechanizmów synchronizacji opi- syjnych krzemionek i kompozytów
się problemami takimi jak: atomo- sanych w tej książce (tj. zadań ato- tlenkowych w skali laboratoryjnej
we przetwarzanie współbieżnych mowych i kombinatorów współbież- i wielkolaboratoryjnej metodą pre-
operacji protokołów, deklaratyw- ności) przy dynamicznym wiązaniu cypitacji, oceny ich właściwości
na synchronizacja oraz dynamicz- obiektów. W dodatku zamieszczo- fizykochemicznych i użytkowych.
na aktualizacja oprogramowania. no formalne dowody poprawności Ponadto przeprowadzono liczne
W tej rozprawie zaprojektowano szeregu twierdzeń wykazujących badania eksperymentalne nad ukła-
nowe konstrukcje językowe i algo- trafność (poprawność) systemu ty- dami hybrydowymi (np. między-
rytmy uzyskiwania atomowości, de- pów (ang. type soundness) dla ra- tlenkowymi), które stanowią naj-
GŁOS POLITECHNIKI | 13
Crystall, zaprojektowano rygory- klaratywnej synchronizacji oraz dy- chunku zadań atomowych, w tym
styczne specyfikacje protokołów namicznej aktualizacji protokołów w dowód dynamicznej poprawności
dynamicznej konstrukcji grupowej systemach komunikacyjnych. Mogą przykładowego algorytmu sterowa-
oraz przeprowadzono dowody po- one służyć do budowy systemów nia współbieżnością.
prawności wybranych protokołów. komunikacyjnych z modularnych
Zaprojektowano i wdrożono nowy, protokołów, które można zastę- Dorobek naukowy dra hab. inż.
w pełni modularny system komuni- pować dynamicznie. Komunikacja P.T. Wojciechowskiego stanowi 38
kacji grupowej Fortika, przeznaczo- umożliwia użyteczne aplikacje, ale publikacji: 2 rozprawy, 2 rozdziały
ny do budowy odpornych na awarie jednocześnie sprawia, że imple- w książkach, 18 artykułów opubli-
serwerów aplikacji rozproszonych. mentacja atomowości, synchroni- kowanych w materiałach recenzo-
W Fortika zastosowano nowe mo- zacji i dynamicznej aktualizacji nie wanych konferencji międzynaro-
dularne protokoły komunikacji gru- jest łatwa. Aby ułatwić programo- dowych, artykuł w czasopiśmie,
powej. Pozwala ona na budowę wanie oraz móc zagwarantować 9 raportów naukowych oraz 3 inne.
aplikacji ze wsparciem zarówno niezawodność, nowe abstrakcje Spośród tych publikacji 10 zostało
modeli awarii typu crash – stop programistyczne są potrzebne. opublikowanych w materiałach na-
(stosowanych dotychczas w innych W rozprawie zaprojektowano rachu- ukowych z listy filadelfijskiego In-
systemach komunikacji grupowej) nek (ang. calculus) zadań atomo- stytutu Informacji Naukowej.
jaki i crash – recovery, tj. z odtwa- wych, tj. transakcji atomowych bez
rzaniem stanu serwera, który uległ odtwarzania stanu, mogących mieć Dr hab. inż. Teofil Jesionowski,
awarii. W projekcie Crystall dr hab. efekty wejścia/wyjścia oraz opisano Wydział Technologii Chemicznej,
inż. Wojciechowski zaproponował nowe algorytmy przeznaczone do otrzymał nagrodę w kategorii Tech-
zbudowanie frameworku protoko- sterowania współbieżnością w za- nologia Chemiczna za cykl prac
łowego, który pozwalałby na bu- daniach atomowych. Rachunek ten ,,Tlenkowe układy hybrydowe –
dowę systemów rozproszonych, wyposażony jest w system typów technologie otrzymywania, wła-
w których protokoły mogą byś do statycznej weryfikacji danych ściwości i zastosowania”. Badania
zmieniane dynamicznie, tj. w trak- wymaganych przez te algorytmy. nad nową generacją tlenkowych
cie działania systemu. Wynikiem System typów gwarantuje, że pro- układów hybrydowych mają olbrzy-
prac w tym kierunku jest frame- ponowane w rachunku konstruk- mie znaczenie dla rozwoju nauki,
work SAMOA, który oferuje abs- cje programistyczne są używane w szczególności technologii che-
trakcję programistyczne i biblioteki, w sposób prawidłowy. Następnie micznej, inżynierii materiałowej
które pozwalają na budowę proto- opisano dwa różne podejścia do i szeroko rozumianej ochrony śro-
kołów sieciowych w sposób mo- synchronizacji deklaratywnej: (1) dowiska. W ten niezwykle istotny
dularny, z możliwością dynamicz- rachunek kombinatorów współ- obszar badań naukowych i technicz-
nej zamiany protokołów w sposób bieżności z opartą na typach wery- nych wpisują się zagadnienia zwią-
całkowicie transparentny dla usług fikacją spełnialności kombinatorów zane z syntezą funkcjonalizowanych
korzystających z tych protokołów. (co daje gwarancję ich poprawnego substancji krzemionkowych, krze-
SAMOA została użyta do imple- zastosowania) oraz (2) język ograni- mianowych i międzytlenkowych,
mentacji AGC – adoptowalnego czeń (ang. constraint language) dla ich charakterystyką fizykochemicz-
systemu komunikacji grupowej, modelu synchronizacji opartego na ną oraz zastosowaniem. Opubliko-
opartego na protokołach z Forti- rolach. Opisano także model dyna- wany cykl prac (m.in. w Dyes and
ka, przystosowanych do modelu micznej aktualizacji protokołów oraz Pigments, Journal of Power Sour-
kompozycji i interakcji istniejącego podano dwa przykładowe algoryt- ces, Journal of Materials Science,
w SAMOA. my przełączania protokołów, mają- Environmental Science and Tech-
ce określone pożądane własności. nology, Journal of Materials Pro-
W nagrodzonej rozprawie habi- Wreszcie zaprojektowano, oparty cessing Technology, Advanced
litacyjnej „Language Design for na klasach, obiektowy rachunek Powder Technology czy Colloid and
Atomicaly, Declarative Synchro- wiązań dynamicznych. Rachunek Polymer Science) dotyczy otrzymy-
anization, and Dynamic Update posłużył do pokazania zastosowań wania sferycznych, monodysper-
in Communicating Systems” zajął mechanizmów synchronizacji opi- syjnych krzemionek i kompozytów
się problemami takimi jak: atomo- sanych w tej książce (tj. zadań ato- tlenkowych w skali laboratoryjnej
we przetwarzanie współbieżnych mowych i kombinatorów współbież- i wielkolaboratoryjnej metodą pre-
operacji protokołów, deklaratyw- ności) przy dynamicznym wiązaniu cypitacji, oceny ich właściwości
na synchronizacja oraz dynamicz- obiektów. W dodatku zamieszczo- fizykochemicznych i użytkowych.
na aktualizacja oprogramowania. no formalne dowody poprawności Ponadto przeprowadzono liczne
W tej rozprawie zaprojektowano szeregu twierdzeń wykazujących badania eksperymentalne nad ukła-
nowe konstrukcje językowe i algo- trafność (poprawność) systemu ty- dami hybrydowymi (np. między-
rytmy uzyskiwania atomowości, de- pów (ang. type soundness) dla ra- tlenkowymi), które stanowią naj-
GŁOS POLITECHNIKI | 13
