Argos Tool for Analysing UML Descriptions

Organisation:	Graz University of Technology Austrian Institute of Technology (AUSTRIA)
Functionality:	Model-based testing and analysis of UML descriptions.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2010-2012
Description:	The Unified Modeling language (UML) is widely used in industry for specifying software models, but it lacks the rigour of a formal method or process algebra. An automated method for transforming a specification written in a well-defined subset of UML into a labeled transition system (LTS) means that the specification can be validated by tools such as CADP, so that errors can be corrected at the earliest stages of development of a system, reducing the cost of correction. The tool chain consists of two applications, with a third application for test case generation. The first application converts the UML specification into the object-oriented action system (OOAS) code. The second application, Argos, then converts the OOAS into an an implicit LTS that can be used as input to the CADP model checking tools. Argos can also create an action system that serves as input to the Ulysses test-case generator. As an example, a simple car alarm system is used to illustrate the process, from specification in UML to generation of the LTS for analysis with CADP. A more pragmatic approach for the syntactic and semantic integration of model-based testing and analysis tools is proposed in [Aichernig-Lorber-Tiran-12]. The approach relies upon the exchange of test cases generated from the models instead of exchanging the models themselves. The advantage is that test cases have a much simpler syntax and semantics, and hence, the mapping between different tools is easier to implement and to maintain. With a formal testing approach with adequate testing criteria a set of test cases can be viewed as partial models that can be formally analysed. The Ulysses test case generator in integrated with the CADP toolbox by means of test case exchange. Test cases are generated in Ulysses and properties are verified in CADP. Also, test cases are generated in CADP and mutation analysis is carried out in Ulysses. More precisely, the test cases generated by Ulysses are grouped into a single model (by merging their initial states) represented in the BCG format of CADP. This model is then determinized and minimized using the REDUCTOR tool. Finally, some safety properties are verified on the resulting test model using EVALUATOR, with two objectives: to check that the generated test cases are consistent with the requirements expressed as temporal properties (quality control of test cases), and to detect possible faults in the models by detecting faults in the test cases. Conversely, the test cases generated by the TGV tool can be imported into Ulysses, which can then perform a mutation analysis using a set of 76 mutants. A mutation analysis shows which of the mutants were killed by a set of given test cases.
Conclusions:	Argos provides a reliable method for translating a UML specification to to an LTS that can be verified, though for a subset of UML that is not standard. Future work on more complex models may extend the subset of UML supported. Given the popularity of UML in industry and the lack of experience in model checking, mixed approaches such as this are likely to become increasingly popular as development teams see the benefits of applying formal methods but lack the necessary expertise to define specifications using process algebras. As regards the use of CADP, it is observed in [Krenn-Schlick-Aichernig-10] that: By giving the action systems abstract trace semantics and generating labeled transition systems for them, we can leverage existing tools, such as the wellknown CADP toolbox: checking of model-inclusion, absence of particular properties, and test-case generation becomes the problem of invoking the right CADP tool.
Publications:	[Krenn-Schlick-Aichernig-10] Willibald Krenn, Rupert Schlick, and Bernhard K. Aichernig. "Mapping UML to Labeled Transition Systems for Test-Case Generation". Proceedings of the 8th International Symposium on Formal Methods for Components and Objects FMCO'09, Lecture Notes in Computer Science vol. 6286, pages 186-207. Springer Verlag, 2010. Available on-line at: http://www.springerlink.com/content/ax58tw6h025w4r1j/ or from the CADP Web site in PDF or PostScript [Aichernig-Lorber-Tiran-12] Bernhard K. Aichernig, Florian Lorber, and Stefan Tiran. "Integrating Model-Based Testing and Analysis Tools via Test Case Exchange". Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering TASE'2012 (Beijing, China), pages 119-126. IEEE Computer Society, July 2012. Available on-line at: http://www.ist.tugraz.at/aichernig/publications/papers/tase12.pdf or from the CADP Web site in PDF or PostScript
Contact:	Bernhard K. Aichernig Institute for Software Technology Graz University of Technology Inffeldgasse 16 b 8010 Graz AUSTRIA Tel: +43 316 873 5717 Fax: +43 316 873-5706 Email: aichernig@ist.tugraz.at
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page