Verification of Non-functional Properties of a Composable Architecture with Petrinets
Jan Richling, Louchka Popova-Zeugmann, Matthias Werner · 2002
In this paper, we introduce our concept of composability and present the MSS architecture as an example for a composable architecture. MSS claims to be composable with respect to timing properties. We discuss, how to model and prove properties in such an architecture with time-extended Petrinets. As a result, the rst step of a proof of composability is presented as well as a new kind of Petrinet, which is more suitable for modeling architectures like MSS.