J. Suryadevara and R.K. Shyamasundar (India)
UML, Concurrency, Parallelism, Abstract Specification, Safety and Liveness
SPECIFICATION OF CONCURRENT COMPONENTS JAGADISH SURYADEVARA Computer Science Group, Birla Institue of Technology & Science (BITS), Pilani, INDIA – 333 0031 Email: [email protected] R.K. SHYAMASUNDAR School of Technology & Computer Science, Tata Institute of Fundamental Research (TIFR), Mumbai, INDIA – 400 005 Email: [email protected] ABSTRACT Unified Modeling Language (UML) has become a de facto industry standard graphical language for design specification of object oriented systems. But, due to lack of formal semantics UML models are not suitable for rigorous formal analysis. This paper defines a UML subset language (cmUML) with formal semantics for precise and abstract specification of concurrent components independent of implementation issues. The approach provides modular specification and verification of larger systems. An integrated multi-view operational semantics of cmUML is defined using symbolic transition systems. This highly expressive language provides constructs to specify explicit parallelism, conditional synchronization, mutual exclusion, safety, and liveness notions as well as the behavior of the interacting environment.
Important Links:
Go Back
