Skapa referens, olika format (klipp och klistra)
Harvard
Carlsson, M. och Johansson, L. (2009) Formal Verification of UML-RT Capsules using Model Checking. Göteborg : Chalmers University of Technology
BibTeX
@mastersthesis{
Carlsson2009,
author={Carlsson, Mats G I and Johansson, Lars G},
title={Formal Verification of UML-RT Capsules using Model Checking},
abstract={Formal verification methods have successfully been used to ensure correctness
of both hardware and software systems. In contrast to testing methods, that
can demonstrate the presence of faults in a system, formal methods can prove
their absence.
A department of the telecommunications company Ericsson AB in Gothenburg,
Sweden, uses the UML-RT language to model software used in WCDMA
radio base stations. These concurrent and reactive systems can be modeled in
the Eclipse-based RSARTE environment.
Previous work underlines a need of narrowing the gap between software
development tools used in industry and formal verification tools. This thesis
examines the feasibility of using model checking to verify properties of UMLRT
capsules. We present a prototype tool for generating verification models
in the Promela language for the model checker Spin. The tool is implemented
as a model-to-text transformation using the JET tool and is integrated into
RSARTE.
The result of the work establishes that it, for a subset of constructs in
UML-RT, is possible to automate generation of verification models that can be
used to demonstrate properties of the original UML-RT capsules. We demonstrate
this with example models created in RSARTE.},
publisher={Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola},
place={Göteborg},
year={2009},
keywords={formal verification, model checking, model-to-text, Promela, RSARTE, Spin, UML-RT},
note={100},
}
RefWorks
RT Generic
SR Electronic
ID 117319
A1 Carlsson, Mats G I
A1 Johansson, Lars G
T1 Formal Verification of UML-RT Capsules using Model Checking
YR 2009
AB Formal verification methods have successfully been used to ensure correctness
of both hardware and software systems. In contrast to testing methods, that
can demonstrate the presence of faults in a system, formal methods can prove
their absence.
A department of the telecommunications company Ericsson AB in Gothenburg,
Sweden, uses the UML-RT language to model software used in WCDMA
radio base stations. These concurrent and reactive systems can be modeled in
the Eclipse-based RSARTE environment.
Previous work underlines a need of narrowing the gap between software
development tools used in industry and formal verification tools. This thesis
examines the feasibility of using model checking to verify properties of UMLRT
capsules. We present a prototype tool for generating verification models
in the Promela language for the model checker Spin. The tool is implemented
as a model-to-text transformation using the JET tool and is integrated into
RSARTE.
The result of the work establishes that it, for a subset of constructs in
UML-RT, is possible to automate generation of verification models that can be
used to demonstrate properties of the original UML-RT capsules. We demonstrate
this with example models created in RSARTE.
PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,
LA eng
LK http://publications.lib.chalmers.se/records/fulltext/117319.pdf
OL 30
