Akcijska logika dreves izvajanj z operatorjem unless : doktorska disertacija

Meolic, Robert

| | SLO | ENG | Piškotki in zasebnost

Izpis gradiva

Naslov:	Akcijska logika dreves izvajanj z operatorjem unless : doktorska disertacija
Avtorji:	ID Meolic, Robert (Avtor) ID Kapus, Tatjana (Mentor) Več o mentorju...
Datoteke:	phd-meolic-si.pdf (1,04 MB) MD5: 90186C455F6E94FE3128B7F64EB54A91 PID: 20.500.12556/dkum/94e6a967-06d9-4c47-99e9-ffa6005ac72f
Jezik:	Slovenski jezik
Vrsta gradiva:	Delo ni kategorizirano
Tipologija:	2.08 - Doktorska disertacija
Organizacija:	FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
Opis:	Doktorska disertacija definira in raziskuje akcijsko logiko dreves izvajanj z operatorjem unless (ACTLW). ACTLW je izjavna temporalna logika razvejanega časa. Izhaja iz logike ACTL, ki je bila vpeljana leta 1990 in je ena od uveljavljenih temporalnih logik za izražanje lastnosti modelov, ki temeljijo na dogodkih. ACTLW je fleksibilnejša od ACTL, saj ne vsiljuje uporabe notranjega dogodka T pri izražanju lastnosti. ACTLW je tudi nekoliko izraznejša od ACTL, saj vsebuje temporalni operator unless (W), katerega pomena v ACTL ni možno v celoti izraziti. Nasprotno pa lahko vse formule ACTL izrazimo z uporabo operatorjev ACTLW. ACTLW omogoča učinkovito izvedbo preverjanja modelov s podobnimi algoritmi kot pri preverjanju modela s CTL, kar je pomembna izboljšava glede na logiko ACTL. Doktorska disertacija podaja definicijo logike ACTLW, izpeljave vseh standardnih temporalnih operatorjev in algoritme za globalno preverjanje modela z ACTLW s simboličnim računanjem. Predstavljeni so tudi algoritmi za tvorjenje diagnostike pri ACTLW, za tvorjenje lineamih prič in protiprimerov pri ACTLW ter za tvorjenje avtomatov prič in proti primerov pri ACTLW. Doktorska disertacija je v celoto zaokrožena z vzorci formul ACTLW in dvema večjima praktičnima primeroma: verifikacijo več različnih algoritmov za medsebojno izključevanje in verifikacijo dveh asinhronih vezij za porazdeljeno medsebojno izključevanje.
Ključne besede:	formalne metode verifikacije sistemov, preverjanje modela, temporalna logika, doktorske disertacije, CTL, ACTL, ACTLW, diagnostika, problem medsebojnega izključevanja
PID:	20.500.12556/DKUM-67095
UDK:	004.23(043.3)
COBISS.SI-ID:	9981718
NUK URN:	URN:SI:UM:DK:OLOFPXQN
Datum objave v DKUM:	04.08.2017
Število ogledov:	1468
Število prenosov:	105
Metapodatki:
Področja:	Ostalo
:	Kopiraj citat

Skupna ocena:	(0 glasov)
Vaša ocena:	Ocenjevanje je dovoljeno samo prijavljenim uporabnikom.
Objavi na:
AddThis uporablja piškotke, za katere potrebujemo vaše privoljenje. Uredi privoljenje...

Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše podrobnosti ali sproži prenos.

Licence

Licenca:	CC BY 4.0, Creative Commons Priznanje avtorstva 4.0 Mednarodna

Povezava:	http://creativecommons.org/licenses/by/4.0/deed.sl
Opis:	To je standardna licenca Creative Commons, ki daje uporabnikom največ možnosti za nadaljnjo uporabo dela, pri čemer morajo navesti avtorja.
Začetek licenciranja:	02.08.2017

Sekundarni jezik

Jezik:	Angleški jezik
Naslov:	Action computation tree logic with unless operator
Opis:	This thesis defines and studies action computation tree logic with unless operator (ACTLW). ACTLW is a propositional branching-time temporallogic. It is derived from logic ACTL, which was introduced in 1990 and which is one of established temporallogics for expressing properties of action-based models. ACTLW is more flexible than ACTL, because it does not impose the usage of silent action T in expressing of the properties. ACTLW has also a slightly greater expressive power than ACTL, because it contains temporal operator unless (W), whose meaning cannot be fully covered in ACTL. As opposite, all ACTL formulae can be expressed using ACTLW operators. ACTLW enables efficient implementation of model checking by using similar algorithms to those used for CTL model checking, which is a significant advantage in comparison to logic ACTL. The thesis gives a definition of logic ACTLW, derivations of all standard temporal operators, and algorithms for global ACTLW model checking using symbolic methods. Moreover, algorithms for generation of diagnostics for ACTLW, for generation of linear witnesses and counterexamples for ACTLW, and for generation of witness and counterexample automata for ACTLW are presented. The thesis is accomplished with patterns of ACTLW formulae and two larger practical examples: a verification of several different mutual-exclusion algorithms and a verification of two asynchronous distributed mutual-exclusion circuits.
Ključne besede:	formal methods of system verification, model checking, temporal logic, CTL, ACTL, ACTLW, diagnostics

Komentarji

Dodaj komentar

Za komentiranje se morate prijaviti.

Komentarji (0)

0 - 0 / 0

Ni komentarjev!

Nazaj