Sciweavers

ISORC
2000
IEEE

Verification of UML-Based Real-Time System Designs by Means of cTLA

14 years 1 months ago
Verification of UML-Based Real-Time System Designs by Means of cTLA
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 ...
Günter Graw, Peter Herrmann, Heiko Krumm
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where ISORC
Authors Günter Graw, Peter Herrmann, Heiko Krumm
Comments (0)