The Crisis Management System – A Case Study in Aspect-Oriented Modeling Using UPPAAL.

Junaid Iqbal; Leonidas Tsiopoulos; Dragos Truscan; Vain Jüri; Ivan Porres Paltor

The Crisis Management System – A Case Study in Aspect-Oriented Modeling Using UPPAAL.

Junaid Iqbal, Leonidas Tsiopoulos, Dragos Truscan, Vain Jüri, Ivan Porres Paltor

Information Technology

Tutkimustuotos: Kirja/lehti/raportti › Tutkimusraportti › Ammatillinen

6 Lataukset (Pure)

Abstrakti

This technical report exemplifies the modelling of a Crisis Management System using an approach which combines aspect-oriented modelling and UPPAAL timed automata. We show that by taking advantage of aspect non-interference, we can enable compositional verification and testing. We provide examples of verification queries and test traces and benchmark the complexity of the verification and test generation activities. The results show that our approach brings clear benefits with respect to compositional verification and testing, compared to traditional modelling in UPPAAL.

Alkuperäiskieli	Englanti
Kustantaja	Turku Center of Computer Science
ISBN (painettu)	978-952-12-3473-6
Tila	Julkaistu - 2016
OKM-julkaisutyyppi	D4 Julkaistut kehitykset tai tutkimusraportit tai tutkimukset

Keywords

Compositional testing
Aspect weaving
UPPAAL Timed Automata
Aspect-oriented Modelling
Compositional verification

Pääsy asiakirjaan

tIqTsTrVaPo16a.fullLopullinen julkaistu versio, 2,41 MB

N4S: Need for Speed
Porres Paltor, I., Nybom, K., Truscan, D., Ashraf, A., Troubitsyna, E., Byholm, B., Rauf, I. M. & Ahmad, T.
01/01/14 → 31/12/16
Projekti: Industry/Business Finland

Viittausmuodot

@book{07f6c469e6284fe4b2e91c60bf676060,

title = "The Crisis Management System – A Case Study in Aspect-Oriented Modeling Using UPPAAL.",

abstract = "This technical report exemplifies the modelling of a Crisis Management System using an approach which combines aspect-oriented modelling and UPPAAL timed automata. We show that by taking advantage of aspect non-interference, we can enable compositional verification and testing. We provide examples of verification queries and test traces and benchmark the complexity of the verification and test generation activities. The results show that our approach brings clear benefits with respect to compositional verification and testing, compared to traditional modelling in UPPAAL.",

keywords = "Compositional testing, Aspect weaving, UPPAAL Timed Automata, Aspect-oriented Modelling, Compositional verification, Compositional testing, Aspect weaving, UPPAAL Timed Automata, Aspect-oriented Modelling, Compositional verification, Compositional testing, Aspect weaving, UPPAAL Timed Automata, Aspect-oriented Modelling, Compositional verification",

author = "Junaid Iqbal and Leonidas Tsiopoulos and Dragos Truscan and Vain J{\"u}ri and {Porres Paltor}, Ivan",

year = "2016",

language = "English",

isbn = "978-952-12-3473-6",

publisher = "Turku Center of Computer Science",

}

TY - BOOK

T1 - The Crisis Management System – A Case Study in Aspect-Oriented Modeling Using UPPAAL.

AU - Iqbal, Junaid

AU - Tsiopoulos, Leonidas

AU - Truscan, Dragos

AU - Jüri, Vain

AU - Porres Paltor, Ivan

PY - 2016

Y1 - 2016

N2 - This technical report exemplifies the modelling of a Crisis Management System using an approach which combines aspect-oriented modelling and UPPAAL timed automata. We show that by taking advantage of aspect non-interference, we can enable compositional verification and testing. We provide examples of verification queries and test traces and benchmark the complexity of the verification and test generation activities. The results show that our approach brings clear benefits with respect to compositional verification and testing, compared to traditional modelling in UPPAAL.

AB - This technical report exemplifies the modelling of a Crisis Management System using an approach which combines aspect-oriented modelling and UPPAAL timed automata. We show that by taking advantage of aspect non-interference, we can enable compositional verification and testing. We provide examples of verification queries and test traces and benchmark the complexity of the verification and test generation activities. The results show that our approach brings clear benefits with respect to compositional verification and testing, compared to traditional modelling in UPPAAL.

KW - Compositional testing

KW - Aspect weaving

KW - UPPAAL Timed Automata

KW - Aspect-oriented Modelling

KW - Compositional verification

KW - Compositional testing

KW - Aspect weaving

KW - UPPAAL Timed Automata

KW - Aspect-oriented Modelling

KW - Compositional verification

KW - Compositional testing

KW - Aspect weaving

KW - UPPAAL Timed Automata

KW - Aspect-oriented Modelling

KW - Compositional verification

M3 - Commissioned report

SN - 978-952-12-3473-6

BT - The Crisis Management System – A Case Study in Aspect-Oriented Modeling Using UPPAAL.

PB - Turku Center of Computer Science

ER -

The Crisis Management System – A Case Study in Aspect-Oriented Modeling Using UPPAAL.

Abstrakti

Keywords

Pääsy asiakirjaan

Sormenjälki

Projektit

N4S: Need for Speed

Viittausmuodot