Współbieżne solvery adaptacyjne dla problemów inżynieryjnych sterowane sieciami Petriego
Teza rozprawy:
Możliwe jest zbudowanie modelu bazującego na sieciach Petriego z gramatyką grafową, opisującego szeroką klasę algorytmów adaptacyjnych bazujących na dwu- i trójwymiarowych siatkach obliczeniowych, umożliwiającego formalną analizę własności współbieżnej wersji algorytmów.
Niniejsza rozprawa przedstawia modele sieci Petriego dla konkretnych implementacji algorytmów adaptacyjnych, mianowicie hp2d- dwuwymiarowej adaptacyjnej metody elementów skończonych, oraz hp3d - trójwymiarowej adaptacyjnej metody elementów skończonych. Opracowane modele pozwoliły dowieść możliwości zablokowania się algorytmu adaptacji w obu przypadkach. Wspomniana blokada faktycznie wystąpiła podczas dwuwymiarowej symulacji pomiarów magnetotellurycznych oraz trójwymiarowej symulacji pomiarów rozkładu potencjału elektrycznego w odwiertach kierunkowych. Model sieci Petriego ułatwił znalezienie modyfikacji algorytmu adaptacji, w wyniku której blokada adaptacji jest niemożliwa, oraz umożliwił dowiedzenie tej ostatniej własności. Wyniki naukowe przedstawione w niniejszej pracy mogą być łatwo rozszerzone poza konkretne implementacje algorytmów adaptacyjnych - hp2d i hp3d. Zaprezentowana metodologia dowodowa może być zastosowana do dowolnego algorytmu adaptacji dwu- i trójwymiarowych siatek obliczeniowych.
Petri nets controlled concurrent adaptive solvers for engineering problems
Main thesis:
It is possible to develop a formal model, based on Petri nets and graph grammar, for a class of adaptive algorithms based on two-dimensional and three- dimensional computational meshes, that allows for formal analysis of the correctness of these algorithms, in particular for detection of the deadlock problem.
This thesis focuses on construction of Petri net models for particular implementation of adaptive algorithms, namely the two-dimensional self-adaptive hp finite element method hp2d and three-dimensional self-self-adaptive hp finite element method hp3d. The Petri net models allowed to prove deadlock-proneness of the original implementations of both algorithms. A deadlock evidence was seen during 2D simulations of magnetolluric measurements process as well as during 3D simulations of resistivity logging while drilling measurements. The constructed Petri nets models made it easier to modify the 2D and 3D mesh adaptation algorithms to make them deadlock-free, and also allowed to prove that the new modified algorithms actually held that property. Scientific results presented in this thesis can be easily generalized beyond the two specific implementations of self-adaptive algorithms - hp2d and hp3d. The same kind of formal proof can be applied to any 2D and 3D computational mesh refinement algorithm.
