Formalios specifikacijos – tai matematinis programinės ar techninės įrangos aprašymas, kurį galima naudoti sistemos realizacijai. Formalių specifikacijų naudojimas dar negarantuoja specifikacijos teisingumo. Tam naudojami formalaus verifikavimo metodai. Šiame dokumente aptariami formalių specifikacijų validavimo metodai. Du populiaraiausi formalių specifikacijų validavimo metodai yra pasiekiamų būsenų grafo analizė bei invarianto tikrinimas. Pasiekiamų būsenų grafo analizę sudaro pasiekiamų būsenų grafo generavimas ir analizė. Grafo analizės metu ieškoma aklaviečių, uždarų ciklų, nepasiekiamų būsenų, atliekamas būsenų koordinačių apribojimų tikrinimas bei invarianto tikrinimas. Tradiciniai pasiekiamų būsenų grafo sudarymo algoritmai grafo sudarymui naudoja sistemos būsenų eilę. Kiekviena išanalizuota būsena įrašoma į pasiekiamų būsenų grafą. Dokumente aptariamas lygiagretaus programavimo naudojimas būsenų grafo generavimui, kuris analizuoja ir generuoja sistemos būsenas naudodamas lygiagrečias gijas. Eksperimentų su vienkanale aptarnavimo sistema metu nustatyta, kad lygiagretaus algoritmo naudojimas šio uždavinio metu leidžia pagerinti sistemos veikimą iki 35%, priklausomai nuo būsenų skaičiaus. / Arguably the most important task in creation of software is user requirement specification. Accurate requirement specification allows avoidance of errors in late stages of software development. This is extremely important in critical systems, where even vague error can cause great financial losses or even human victims. One of the methods used for precise user requirement specification is use of formal specifications.
Formal specification is a mathematical method for describing of software or hardware, which might be suitable for system realization. Nevertheless, the construction of formal specifications does not guarantee the correctness of specification. For this reason formal specification validation is necessary.
In this paper methods of formal specification validation are discussed. Two most popular methods of formal specification validation are reachable state graph analysis and invariant checking. Reachable state graph analysis consists of graph generation and graph analysis. Graphs can be analyzed for dead-ends, closed loops, state reach ability checking, coordinate restriction checking or invariant checking. Traditional reachable graph generation algorithm uses unanalyzed states queue to produce reachable state graph. Each step single state is analyzed and depending on results new vertex or edge is added to state graph.
An improvement to the algorithm to consider is usage of parallel programming to process multiple states simultaneously. This allows increasing the... [to full text]
| Identifer | oai:union.ndltd.org:LABT_ETD/oai:elaba.lt:LT-eLABa-0001:E.02~2008~D_20080811_151721-05181 |
| Date | 11 August 2008 |
| Creators | Krivoūsas, Tomas |
| Contributors | Stulpinas, Raimundas, Motiejūnas, Kęstutis, Bareiša, Eduardas, Butleris, Rimantas, Kazanavičius, Egidijus, Tomkevičius, Arūnas, Šeinauskas, Rimantas, Štuikys, Vytautas, Blažauskas, Tomas, Pranevičius, Henrikas, Kaunas University of Technology |
| Publisher | Lithuanian Academic Libraries Network (LABT), Kaunas University of Technology |
| Source Sets | Lithuanian ETD submission system |
| Language | Lithuanian |
| Detected Language | English |
| Type | Master thesis |
| Format | application/pdf |
| Source | http://vddb.library.lt/obj/LT-eLABa-0001:E.02~2008~D_20080811_151721-05181 |
| Rights | Unrestricted |
Page generated in 0.0026 seconds