Modeling and verification of fuzzy control systems using piece linear aggregate formalism

Darbe pristatomas neraiškių valdymo sistemų modeliavimas ir verifikavimas atkarpomis tiesiniu agregatiniu formalizavimo metodu. Ši metodika leidžia pagal vieną formalaus modelio aprašą kurti realiojo laiko neraiškių valdymo sistemų modelius, skirtus sistemos funkcionavimo ir elgsenos analizei. Sistemų modeliavimui buvo sukurti agregatai, kurie realizuoja neraiškios sprendimo priėmimo sistemos pagrindinius komponentus. Pagal analizuojamos neraiškios valdymo sistemos struktūrą sujungus šiuos agregatus, gaunamas neraiškios sprendimo priėmimo sistemos agregatinis modelis, kuris gali būti taikomas sistemos funkcionavimo ir elgsenos analizei. Darbe taip pat pristatoma sukurta realiojo laiko agregatinių modelių verifikavimo metodika, kurią sudaro agregatinio modelio transformavimas į laiko automatus, verifikuojamų savybių užrašymas laiko logikoje bei modelių tikrinimo įrankio UPPAAL panaudojimas sistemos savybėms patikrinti. Sukurta neraiškių valdymo sistemų modeliavimo ir verifikavimo metodika agregatiniam formalizavimo metodui buvo pritaikyta transporto srautų valdymo ir vaistų leidimo pompų sistemų analizei. Panaudojant sukurtus transporto srautų valdymo ir vaistų leidimo pompų agregatinius modelius, buvo sudaryti imitaciniai modeliai, kurie leido įvertinti modelių funkcionavimo charakteristikas ir juos tarpusavyje palyginti. Realiojo laiko agregatinių sistemų verifikavimo metodika panaudota tikrinant analizuojamų sistemų gyvybingumo, saugumo ir pasiekiamumo savybes.In this research a Piece Linear Aggregate method for modelling and verification of fuzzy control systems is presented. This method allows to create an aggregate model of a real time fuzzy control system for performance and behaviour analysis in a single mathematical scheme. The main components of fuzzy inference system were created by using aggregate approach. These aggregates implement a fuzzy inference system while interacting with each other. This allows to specify fuzzy control system and to realize the development of the simulators and models for verification. Based on the behaviour equivalence, a method for transforming aggregate models into timed automata is presented for the purpose of verifying real time system. The timed automata and temporal logic formulas are used as inputs of UPPAAL model checker for verifying fuzzy control system. The proposed method for modelling and verification of fuzzy control system by using aggregate formalism was applied for analysing traffic signal control and drug delivery systems. Formal aggregate models of traffic signal and drug delivery control systems were used for creating simulation models for performance analysis. The proposed method for verification of the real time aggregate models was used to check safety, liveness and reachability properties of traffic signal and drug delivery control systems.Vytauto Didžiojo universiteta