Reference:
Martin Hirsch and Holger Giese, "Towards the Incremental Model Checking of Complex RealTime UML Models", in Holger Giese, Albert Zündorf, Eds., Proc. of the first International Fujaba Days 2003, Kassel, Germany, vol. tr-ri-04-247 of Technical Report, pp. 9–12, University of Paderborn, October 2003.
Abstract:
Today, the verification of complex distributed embedded real-time systems employing model checking is largely limited by the state explosion problem. We first report on the current tool support for an approach which addresses this problem by means of a compositional model checking approach for a pattern and component based UML 2.0 designs. However, the current checking covers only an abstraction of the employed Realtime Statechart semantics (cf. [4, 9]), and the compositional approach only works for properties which refer either to a single pattern or a single component. We then present plans for an improved tool support which supports the full Realtime Statechart semantics, enables the compositional checking of non-local properties, and a model checker integration which triggers required checks after a model update automatically in the background.
Links:
@InProceedings{HG03_ag,
AUTHOR = {Hirsch, Martin and Giese, Holger},
TITLE = {{Towards the Incremental Model Checking of Complex RealTime UML Models}},
YEAR = {2003},
MONTH = {October},
BOOKTITLE = {Proc. of the first International Fujaba Days 2003, Kassel, Germany},
VOLUME = {tr-ri-04-247},
PAGES = {9--12},
EDITOR = {Giese, Holger and Z\"{u}ndorf, Albert},
SERIES = {Technical Report},
PUBLISHER = {University of Paderborn},
URL = {http://www.upb.de/cs/ag-schaefer/Veroeffentlichungen/Quellen/Papers/2003/FD03-HG.pdf},
PDF = {FD03-HG.pdf},
ABSTRACT = {Today, the verification of complex distributed embedded real-time systems employing model checking is largely limited by the state explosion problem. We first report on the current tool support for an approach which addresses this problem by means of a compositional model checking approach for a pattern and component based UML 2.0 designs. However, the current checking covers only an abstraction of the employed Realtime Statechart semantics (cf. [4, 9]), and the compositional approach only works for properties which refer either to a single pattern or a single component. We then present plans for an improved tool support which supports the full Realtime Statechart semantics, enables the compositional checking of non-local properties, and a model checker integration which triggers required checks after a model update automatically in the background.}
}Copyright notice: This material is presented to ensure timely dissemination of
scholarly and technical work. Copyright and all rights therein are retained by
authors or by other copyright holders. All persons copying this information are
expected to adhere to the terms and constraints invoked by each author's copyright.
In most cases, these works may not be reposted without the explicit permission of
the copyright holder.
Powered by
bibtexbrowser