by Martin Hirsch, Holger Giese
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.
Reference:
Towards the Incremental Model Checking of Complex RealTime UML Models (Martin Hirsch, Holger Giese), In Proc. of the first International Fujaba Days 2003, Kassel, Germany (Holger Giese, Albert Zündorf, eds.), University of Paderborn, volume tr-ri-04-247, 2003.
Bibtex Entry:
@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ü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.}
}