Formalni model specifikacije pokretnih telekomunikacijskih agenata : magistarski rad - Bagić, Marina; Kunštić, Marijan (Zagreb : M. Bagić ; Fakultet elektrotehnike i računarstva, 2004)
Rad prikazuje razvoj formalne infrastrukture za specifikaciju višeagentskih sustava počevši od matematičkog aparata vektorskog prostora i kauzalnih mapa do konkretnih izvedbi dijagrama postojećih specifikacijskih jezika, konkretno Agent UML-a i obojenih Petrijevih mreža. Ističe važnost dobro definirane formalne specifikacije i dizajna koji podupiru rane faze razvojnog ciklusa softvera. Takvi formalizmi trebali bi poboljšati kvalitetu razvoja sustava prije njegove implementacijske faze verifikacijom i validacijom sustava. Petrijeve mreže pružaju mogućnosti konstrukcije sustava, te njegove simulacije, funkcionalne analize i analize performansi. Višeagentski sustavi podupiru autonomne, (re)aktivne i interno motivirane agente. Primjer takva sustava u radu je procesiranje poziva koji se bez gubitka informacija može generalizirati na proizvoljan drugi model upravljanja mrežom. Rezultati ovoga rada pokazuju da se mnogi aspekti AUML jezika mogu proširiti Petrijevim mrežama za formalnu definiciju ponašanja modeliranog sustava. AUML jezik proširen konceptom Petrijevih mreža može se efikasno koristiti za verifikaciju i validaciju specifičnih softverskih rješenje zahvaljujući karakteristikama Petrijevih mreža.
Ključne riječi:
• formalna specifikacija • verifikacija • validacija • formalizmi • Unified Modeling Language • Agent Unified Modeling Language • prošireni AUML • pokretni agent • agent u formalizmu Petrijeve mreže • obojena Petrijeva mreža • CPN Tools • procesiranje poziva
Software design is the technical kernel of software engineering, and to develop critical and complex software systems requires a complete, consistent and unambiguous specification. This observation has motivated initial work of using formal methods in concurrent object-oriented design, and further derived modelbased approach for development of agent-oriented software systems. This thesis has been focused on multi-agent system analysis due to wide application of agent technologies in distributed artificial intelligence. Agent-oriented models support autonomous, reactive and internally-motivated agents. Although formal methods have been widely used in specifying and verifying complex software systems, to bridge the gap between formal models and implemented systems is still a big challenge. Formal methods have been frequently adopted in the requirements analysis phase to specify a system and its desired properties, e.g. behavioural properties. This is not only because of the infancy of the techniques and the apparent difficulty of the notations used, but also due to a lack of support for modularization in most of the formal approaches. This thesis pointed out the importance of well-defined formal mechanism to support an early stage of software system development. Such mechanism should improve and prevent developing system from mistakes to appear in its implementation phase. Also, used method has achieved a formal mode that makes it possible to both verify and validate the system before its implementation. Due to this benefit the results on system behaviour simulation give an insight into possible system weaknesses and disabilities such as bottlenecks, dead states or other insufficiencies. Petri nets-based approach has been applied for system specification due to their benefits in system simulation and analysis abilities. CPN tools support the construction, simulation, functional and performance analysis of Coloured Petri Net models. Results of this thesis emphasis that many aspects of Agent Unified Modelling Language should be extended by Coloured Petri Nets to formally define system behaviour. Extended AUML efficiently verifies and validates specific software solutions due to Coloured Petri Net benefits.
Keywords:
• Formal Specification • Verification • Validation • Unified Modeling Language • Agent Unified Modeling Language • Extended AUML • Mobile Agent • Agent within Petri Net Formalism • Coloured Petri Net • CPN Tools • Call Processing
Bibliografija str. 96-98.