Using a process algebra interface for verification and validation of UML statecharts |
| |
Affiliation: | Université de la Polynésie Française, Laboratoire GePaSud, Campus d''Outumaoro, Punaauia - B.P. 6570, Faa''a, Tahiti 98702, French Polynesia |
| |
Abstract: | UML diagrams are the conventional methods for visual modeling systems. Among them, the Statechart diagrams are used to show the runtime behavior of a system, but the correctness of such diagrams is the primary concern of the designers because of concurrency issues like livelock, inaccessible states, and non-deterministic states. Process algebra methods have the capabilities that are suitable for verification and validation of Statecharts. To this end, in this paper, process algebra language LOTOS (Language Of Temporal Ordering Specification) is used as the target language, and a method is presented to map UML Statecharts to the LOTOS processes, called USLP. Then the correctness of the proposed mappings is proved by demonstrating the isomorphism relation between the Labeled Transition System (LTS) of a Statechart and the LTS of its transformed LOTOS specification. Next, tools CADP (Construction and Analysis of Distributed Processes) is used for verification and validation of the mapped LOTOS models, and the CSP process algebra and its tools, FDR are used to verify the properties could not be verified by the LOTOS and its toolset. The experimental results show our approach can: (1) verify some properties (the issues) that are not verified by other approaches and (2) reduce the space that should be searched to verify the properties. |
| |
Keywords: | UML Statechart Formal specification Verification Validation LOTOS CSP |
本文献已被 ScienceDirect 等数据库收录! |
|