Verification of Non-functional Properties of a Composable Architecture with Petrinets

Issue title: Concurrency Specification and Programming Workshop (CS&P'2001)

Article type: Research Article

Authors: Richling, Jan | Popova-Zeugmann, Louchka | Werner, Matthias

Affiliations: Humboldt-Universität zu Berlin, Institut für Informatik, Rudower Chaussee 25, 12489 Berlin, Germany

Abstract: 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 first 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.

Keywords: real time, composability, Petrinets, duration nets, π-PN

Journal: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 185-200, 2002