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

Research output: Book/Journal/Report › Commissioned report › Professional

17 Downloads (Pure)

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.

Original language	English
Publisher	Turku Center of Computer Science
ISBN (Print)	978-952-12-3473-6
Publication status	Published - 2016
MoE publication type	D4 Published development or research report or study

Keywords

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

Access to Document

tIqTsTrVaPo16a.fullFinal published version, 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
Project: Industry/Business Finland

Cite this

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

Abstract

Keywords

Access to Document

Fingerprint

Projects

N4S: Need for Speed

Cite this