Verification of UML-based real-time system designs by means of cTLA

Günter Graw, Peter Herrmann, Heiko Krumm

Universität Dortmund, FB Informatik, LS IV, D-44221 Dortmund, Germany
E-Mail: {graw| herrmann| krumm}@ls4.cs.tu-dortmund.de

Abstract

The Unified Modeling Language UML is well-suited for the design of real-time systems. In particular, the design of dynamic system behaviors is supported by interaction diagrams and statecharts. Real-time aspects of behaviors can be described by time constraints. The semantics of the UML, however, is non-formal. In order to enable formal design verification, we therefore propose to complement the UML based design by additional formal models which refine UML diagrams to precise formal models. We apply the formal specification technique cTLA which is based on L. Lamport's Temporal Logic of Actions TLA. In particular cTLA supports modular definitions of process types and the composition of systems from coupled process instances. Since process composition has superposition character, each process system has all of the relevant properties of its constituting processes. Therefore mostly small subsystems are sufficient for the verification of system properties and it is not necessary to use complete and complex formal system models. We present this approach by means of an example and also exemplify the formal verification of its hard real-time properties.

Published in

Proceedings of the 3rd IEEE International Symposium on Object-oriented Real-time distributed Computing (ISORC2K), pages 86-95, Newport Beach, IEEE Computer Society Press, 2000.

Obtaining the paper

Due to the copyright agreement between the publisher and the authors we are not allowed to make the paper available online. If you have problems to obtain it, please call us.