Operációkutatási módszerek műszaki informatikai rendszerek analízisében és verifikációjában = Operation Research Methods for the Analysis and Verification of Information Technology Systems

摘要

Kidolgoztuk a Petri-hálók és produkciós hálók (PNS) egységes szemléletű leírását. Megfogalmaztuk az "optimális trajektória generálásának" problémáját Petri-hálós modellekre. A megoldásként kidolgozott és implementált algoritmus egyúttal temporális logikai követelményeket is vizsgál a modellen. Az algoritmust gyorsítottuk a PNS logikai bázisa fölötti kereséssel. A SPIN modellellenőrzőt magát használva egy másik megoldást is adtunk a problémára, valamint gráftranszformációs rendszerek optimalizálására. Megadtuk a lineáris korlátozási feltételekkel adott szeparábilis konkáv minimalizálási feladat egy elégséges optimalitási kritériumát, mely a Branch-and-Bound típusú algoritmusban használható fel megállási kritériumként. A magasszintű leírásokból a Petri-hálós modellbe történő transzformációkat matematikai alapokon definiáltuk, megvalósításukra automatikus modelltranszformációs megoldást dolgoztunk ki: egy algoritmust, amely GRM profillal adott modellből generálja a Petri-hálót, és egy általános algoritmust, amely UML modellekből származtat a diagnosztika alapjául szolgáló modelleket. Megvizsgáltuk ezen modellek illeszthetőségét a szabványokhoz. Multiprocesszoros rendszerek diagnosztizálására egy PNS technikákat használó algoritmust adtunk, melynek várható hatékonyságát igazoltuk. Munkálatok folytak a diagnosztika tesztalapú megközelítésére, és diagnosztikai modellek kísérletes paraméterezésére. Kísérleteket végeztünk az IBM Holosofx ipari workflow modellező eszköz illesztésére. | A unified treatment for Petri nets and process network (PNS) problems was defined. The 'optimal trajectory generation problem' for Petri nets was defined. Elaboration and implementation of an algorithm that is able not only to give the optimal trajectory but to verify temporal logic requirements for Petri nets. This algorithm was accelerated using Branch-and-Bound method over the logical basis of the feasible process networks. Another algorithm to solve the problem using only the SPIN model checker was elaborated. The optimization of graph transformation systems with time was solved based on the same technique. A sufficient optimality criteria was given for constrained, concave minimization problems. The precise mathematics of the model transformation from high-level models to Petri nets was defined, and automatic model transformations were carried out to realize these transformations: a transformation from UML models given by the GRM profile to Petri nets and a general algorithm that delivers models to diagnose from UML models. The conformancy of these models to standards was investigated. The probabilistic diagnosis problem in multiprocessor systems was solved using PNS techniques. The efficiency of the method was shown. There were efforts to elaborate a test-based approach of diagnostics, and to parameterize diagnostics models based on dependability experiments. Experiments were carried out to transform IBM Holosofx models to Petri nets.