cmUML - A UML based Framework for Formal Specification of Concurrent, Reactive Systems

Complex software systems possess concurrent and reactive behaviors requiring precise specifications prior to development. Lamport's transition axiom method is a formal specification method which combines axiomatic and operational approaches. On the other hand Unified Modeling Language (UML), a de facto industry standard visual language, lacks suitable constructs and semantics regarding concurrency aspects. Though UML includes action semantics, its higher level constructs and object semantics are inconsistent. Motivated by Lamport's approach, this paper proposes a UML based specification framework `cmUML' (`cm' for concurrent modules) for formal specification of concurrent, reactive systems without object level diagrams and OCL. The framework integrates higher level diagrams of UML and addresses various concurrency issues including exception handling. It combines UML-RT and UML/ SPT profile as the latter defines a core package for concurrency and causality. Further ...

• Type: Journal
• Year: 2008
• Where: JOT
• Authors: Jagadish Suryadevara, Lawrence Chung, R. K. Shyamasundar
• Keywords: Formal Specification, JOT 2008, Specification, Transition Axiom Method