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

Informationsteknologi

Forskningsoutput: Bok/tidskrift/rapport › Beställd rapport › Professionell

36 Nedladdningar (Pure)

Sammanfattning

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.

Originalspråk	Engelska
Förlag	Turku Center of Computer Science
ISBN (tryckt)	978-952-12-3473-6
Status	Publicerad - 2016
MoE-publikationstyp	D4 Publicerad utvecklings- eller forskningsrapport eller studie

Nyckelord

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

Åtkomst av dokument

tIqTsTrVaPo16a.fullSlutlig publicerad version, 2,41 MB

N4S: Need for Speed
Porres Paltor, I. (Ansvarig forskare), Nybom, K. (CoI), Truscan, D. (CoI), Ashraf, A. (CoI), Troubitsyna, E. (CoI), Byholm, B. (CoI), Rauf, I. M. (CoI) & Ahmad, T. (CoI)
01/01/14 → 31/12/16
Projekt: Företag/Business Finland

Citera det här

@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.

Sammanfattning

Nyckelord

Åtkomst av dokument

Fingeravtryck

Projekt

N4S: Need for Speed

Citera det här